Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore: bump to v1.15.0-rc1 #970

Draft
wants to merge 15 commits into
base: main
Choose a base branch
from
Draft

chore: bump to v1.15.0-rc1 #970

wants to merge 15 commits into from

Conversation

pitmonticone
Copy link
Collaborator

@pitmonticone pitmonticone commented Dec 2, 2024 •
edited by github-actions bot
Loading

null

Closes #977

@kim-em
Copy link

kim-em commented Dec 2, 2024

https://github.com/teorth/equational_theories/pull/970/files#diff-409cb2b8a4104e6f92772ad832e1551e548fb7ffcb5d3d45c600a9b603f5338cR348-R349 can be replaced with

    · simp at can
      obtain ⟨rfl, rfl⟩ := can
      simp [this]
      ext n h₁ h₂
      · simp
      · simp [List.getElem_append] at h₁ ⊢
        omega

@pitmonticone @kim-em
Update LawsComplete.lean
5e9ba26 
Co-Authored-By: Kim Morrison <kim@tqft.net>
@pitmonticone
Copy link
Collaborator Author

Thank you @kim-em, done.

@pitmonticone pitmonticone marked this pull request as ready for review December 2, 2024 16:45
@vlad902
Copy link
Contributor

vlad902 commented Dec 3, 2024

For posterity: I believe the CI failure here is lean4#5548, and that a fix may be adding a ulimit -s 16000 to expand the stack space given that issue.

@pitmonticone
Copy link
Collaborator Author

Done. Let's see...

@teorth teorth removed the awaiting-CI label Dec 3, 2024
@pitmonticone pitmonticone mentioned this pull request Dec 4, 2024
Open
@pitmonticone pitmonticone marked this pull request as draft December 4, 2024 20:06
@pitmonticone
Copy link
Collaborator Author

It's likely that the current issue is related to the following:

I am waiting for the above PR to be merged, after which I will re-run the CI jobs.

@vlad902
Copy link
Contributor

vlad902 commented Dec 14, 2024

@pitmonticone The fix for that build failure is:

diff --git a/equational_theories/MemoFinOp.lean b/equational_theories/MemoFinOp.lean
index 22c326ad..dd74d59d 100644
--- a/equational_theories/MemoFinOp.lean
+++ b/equational_theories/MemoFinOp.lean
@@ -132 +132 @@ elab "finOpTable" str:str :term => do
-  discard <| withCurrHeartbeats <| Tactic.run mv.mvarId! do Lean.Elab.Tactic.evalTactic (← `(tactic| decide!))
+  discard <| withCurrHeartbeats <| Tactic.run mv.mvarId! do Lean.Elab.Tactic.evalTactic (← `(tactic| decide +kernel))

@pitmonticone
Copy link
Collaborator Author

Thanks. I'll do it later today.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Updates available but manual intervention required
4 participants
@pitmonticone @kim-em @vlad902 @teorth