Repository navigation
Bump Lean toolchain v4.29.1 -> v4.34.1 - #14
Open
kiranandcode wants to merge 3 commits into
Open
kiranandcode wants to merge 3 commits into
kiranandcode wants to merge 3 commits into
Conversation
- GIL: acquire around every CPython-touching bridge entry via a cleanup-attribute WITH_GIL macro (releases on all return paths). - Remove dead lean_types.py + manual m_rc helpers; route library.py through lean_dec. Replace magic IO.Error tag constants with lean_is_string. Clear stale worktree/autosave/pyc; fix README count. - stubgen: generate .pyi from the registry (mypy-clean). - packaging: vendor the dylib closure + lean.h into a py3-none wheel that loads with no toolchain present. - registry: TypeRepr drives both the stub annotation and a runtime predicate (matches/check); opt-in set_argument_typechecking. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- lean-toolchain (root, tests/lean, examples/*) -> v4.34.1 - Regex v4.29.0 -> v4.34.0-rc1; Pantograph dev -> 92d4818 - Kernel.declAxioms: use public Lean.collectAxioms (CollectAxioms.collect is now private) - Kernel.envUnpickle/goalUnpickle: re-enable initializer execution, since withImporting now clears the flag after each import - Z3 datatypes: compileDecls the inductive before mkCtorIdx etc. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This branch has not been deployed
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.
Bumps lean.py to Lean v4.34.1, the latest stable release.
Dependencies
lean-toolchain→leanprover/lean4:v4.34.1in the root,tests/leanand all sixexamples/*/leanprojects (manifests refreshed).v4.29.0→v4.34.0-rc1(its newest tag; no stable v4.34 tag yet).dev→92d4818. Upstream targets Lean v4.33.1 but compiles cleanly on 4.34.1.Fixes for 4.34 breakage
The C bridge and Python bindings needed no changes. No public Python API changed.
Kernel.declAxioms:CollectAxioms.collectis now private, so this uses the publicLean.collectAxioms. Output is unchanged.Kernel.envUnpickle/goalUnpickle:withImportingnow clears the initializer-execution flag after each import, so unpickling (which re-imports) failed. Both now callenableInitializersExecutionfirst.Z3.leandatatypes: inductives must be compiled beforemkCtorIdxetc., socompileDecls #[tName]now runs afteraddDecl, matching Lean's own inductive elaborator.Verification (macOS, local)
lake build(root) andlake build TestLib:sharedpass; examples 01 and 02 build.pytest tests: 1325 passed, 0 skipped (with sympy and numpy installed).ruff format --check,ruff check,mypy lean_py/clean.tests/leaks_check.sh: 0 leaks.Not run locally: the Linux CI jobs (including valgrind), and builds of examples 03 to 06.
Known gap (not fixed here)
ManagedProjectpins batteries/aesop/mathlib to the exact toolchain tag. mathlib hasv4.34.1; batteries and aesop only havev4.34.0.🤖 Generated with Claude Code