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)
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
1 participant
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.
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).