Harden the C bridge; add stub, wheel, and type-check tooling - #13
Merged
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>
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.
Cleans up the FFI layer and adds three tools borrowed from leanprover/nerodia.
FFI + cleanup. The C bridge now takes the GIL around every CPython-touching entry point, via a
cleanup-attribute macro that releases it on all return paths. Correctness no longer rests on loading through ctypesPyDLLalone; it holds for foreign threads and free-threaded builds too. Removedlean_types.pyand its manualm_rchelpers, which duplicated the refcount bug fixed earlier, and routedlibrary.pythroughlean_dec. Swapped the magic249/18tags informat_lean_io_errorforlean_is_string. Cleared a stale worktree, editor autosave files, and dead.pyc; corrected the README test count.Type stubs.
python -m lean_py.stubgen <project> <Lib>(orlib.write_stub()) generates a.pyifrom the registry, so editors and type-checkers see real signatures instead ofAny. mypy-clean on the 90-function TestLib surface.Self-contained wheels.
python -m lean_py.packaging build ...vendors the dylib closure pluslean.h, relocates them to@loader_path/$ORIGIN, and writes apy3-none-<platform>wheel with a loader. lean.py binds through ctypes, so no abi3 tag is needed. Two tests load the library with elan stripped from the environment.Unified types.
TypeRepryields both the stub annotation (which stubgen consumes) and a runtime predicate (matches/check), with opt-inset_argument_typechecking(True). One description drives static hints and value checks, adapting nerodia'sTyping = Py.Raw → Propto the registry design.1325 tests pass, none skipped, with sympy and numpy installed.
🤖 Generated with Claude Code