Conversation
Bump the Lean toolchain and mathlib to v4.33.0-rc2 and adapt the backend and tests to the new toolchain. Toolchain: - backends/lean and tests/lean lean-toolchain -> v4.33.0-rc2 - mathlib tag -> v4.33.0-rc2 in lakefile.lean; regenerate both manifests API breakage: - BvEnumToBitVec / BvTac: BVDecide frontend moved from Lean.Elab.Tactic.BVDecide.Frontend.* to Lean.Meta.Tactic.BVDecide.* - Simp: 4.33 no longer inserts the Array->Option coercion; make it explicit - ReduceZMod: mathlib Monoid.toPow -> NPow.toPow / Monoid.toNPow Proof / tactic repair: - Make Pre reducible (like Post) so and_imp/exists_imp flatten conjunction/existential post-conditions again in step/let* (4.33's simp only rewrites when the conclusion is recognised as Prop) - Fix grind/simp failures on spec (ok ...) goals via spec_ok, and the semireducible-wrapper getElem/setSlice! lemmas in Vec/Slice - FlatOrder.mk admissibility, StepStar TaskOrDone annotation, StepArraySpec declModifiers TSyntax category, Step do-block returning Unit - Update #guard_msgs for the reworded unusedVariables linter message Tests: - Work around leanprover/lean4#14521 (grind emits a kernel-invalid eq_false_of_decide term for BitVec equalities whose width is defeq but not syntactically 32): route the tutorial get_elem_tactic through scalar_tac, and spell out the one step* demo explicitly Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> (cherry picked from commit 744f829)
clementblaudeau
left a comment
clementblaudeau
left a comment
There was a problem hiding this comment.
I think the proof changes look fine, even though the grind regressions should be investigated. The main thing that could block upstreaming would be significant change in proof checking time of the lib itself.
Could also be split into several PRs.
There was a problem hiding this comment.
This could be upstreamed regardless of the lean version bump right ?
There was a problem hiding this comment.
Are those specific to the lean bump ? They seem like reasonable changes anyway
There was a problem hiding this comment.
Proof changes like those seem fine to me.
Comment on lines
-11
to
+12
| def Post α := (α -> Prop) | ||
| def Pre := Prop | ||
| @[reducible] def Post α := (α -> Prop) | ||
| @[reducible] def Pre := Prop |
Comment on lines
-744
to
745
| grind [spec, Std.lift] | ||
| simp only [Std.lift, spec_ok, ← h1] | ||
| exact h0 | ||
|
|
Comment on lines
1015
to
1031
| def tryApply (info : SpecInfo) (lifting : Option LiftingInfo) (args : Args) (isLet:Bool) (fExpr : Expr) (kind : String) (th : Option Expr) : | ||
| TacticM (Option Goals) := do | ||
| let res ← do | ||
| match th with | ||
| | none => | ||
| trace[Step] "Could not find a {kind}" | ||
| pure none | ||
| | some th => do | ||
| trace[Step] "Lookuped up {kind}: {th}" | ||
| -- Apply the theorem | ||
| let res ← do | ||
| try | ||
| let res ← stepWith info lifting args isLet fExpr th | ||
| pure (some res) | ||
| catch _ => pure none | ||
| try | ||
| let res ← stepWith info lifting args isLet fExpr th | ||
| pure (some res) | ||
| catch _ => pure none | ||
| match res with | ||
| | some res => pure (some res) | ||
| | none => pure none |
Comment on lines
+5
to
11
| -- Workaround for leanprover/lean4#14521: the default `get_elem_tactic` (`grind`) | ||
| -- emits kernel-invalid proofs when an index bound depends on `_ ≠ 0#uN` (the | ||
| -- BitVec width `numBits U32` is defeq but not syntactically `32`). `scalar_tac` | ||
| -- discharges these bounds correctly; `grind` stays as a fallback. | ||
| local macro_rules | ||
| | `(tactic| get_elem_tactic) => `(tactic| grind) | ||
| | `(tactic| get_elem_tactic) => `(tactic| first | scalar_tac | grind) | ||
|
|
Lean v4.33 newly enables the `dupNamespace`, `defProp`, and `ambiguousOpen` linters. They fire on generated Rust-path declaration names, intentional `Prop`-valued definitions, and `open Std` (now that `Lean.Std` also exists) -- none cleanly fixable in the generated / spec code -- so disable them in the lakefile to keep CI's `lake build --iofail` green after the toolchain bump. Also drop a few unused simp arguments and one unnecessary `<;>`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Bump the Lean toolchain and mathlib to v4.33.0-rc2 and adapt the backend and tests to the new toolchain.
Toolchain:
API breakage:
Proof / tactic repair:
Tests:
(cherry picked from commit 744f829)
Instructions
Thanks for opening a PR! We welcome external contributions but encourage contributors to
coordinate with us before, either by joining the Zulip or by opening issues with detailed
proposals. In particular, we ask contributors to engage with us before making deep
modifications of the code or implementing non trivial features, as these require in-depth
design discussions and careful reviews. This means for instance that proposals to extend
the translation should be discussed first. On the other hand, you should feel free to
directly submit PRs that fix an issue through a scoped, small fix, or that add theorems to
the standard library. In case of doubt, discuss with us.
Good practices:
functions with
#[verify::test]to generate tests at extraction time)AI assisted PRs:
Please indicate whether the PR was AI assisted, and by how much: did you use AI in a
limited way or did you completely vibe-code the PR? We welcome AI assisted PRs but need
this information to adjust our level of scrutinee during the review and evaluate whether
it is reasonable to ask for the contributor to completely modify their code. Also note
that we expect contributors to own and understand the code they submit: as we will
carefully review the PR line by line, we expect contributors to have done the same for AI
generated code (reviewing PRs takes time and we have limited resources).