This release is a pre-release and may not be stable for production use.
setuptools-lean
The setuptools-lean package provides a setuptools plugin for building and bundling Python extensions written in Lean. It uses Nerodia as its Lean backend.
Quick Start
Python modules are configured on the Lean side through Nerodia. For example,
the Lean definition of the Python module mymodule would look something like this:
MyModule.lean
module
import Nerodia
open scoped Nerodia
py_module "mymodule"
This module can then be bundled into a Python package with the following configuration:
pyproject.toml
[project]
name = "mypackage"
version = "1.0.0"
requires-python = ">=3.14"
[tool.setuptools]
# setuptools-lean will generate a Python package for us.
# Without this field, setuptools may assume Lean libraries are Python packages.
# Python packages of your own can be added to this list.
packages = []
[build-system]
requires = ["setuptools", "setuptools-lean"]
build-backend = "setuptools.build_meta"
[[tool.setuptools-lean.ext-modules]]
lean-module = "MyModule"
This package can then be installed locally via pip install ., and the installed Python extension imported via import mymodule. If you are using uv, running Python code that imports mymodule is as simple as running uv run mymoduleuser.py in the same directory as the Python extension (no manual install necessary). setuptools-lean will also locate Nerodia-generated type stubs for the module where they need to be so that type checkers and editors will pick them up. Thus, editing a Python module mymoduleuser will provide all the rich type information and docstrings users might expect from regular Python code.
For a complete example of developing a Python package in Lean, refer to Nerodia.
1 maintainer
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Filter files by name, interpreter, ABI, and platform.
If you're not sure about the file name format, learn more about wheel file names.
Copy a direct link to the current filters
File details
Details for the file setuptools_lean-0.2.0rc1.tar.gz.
File metadata
- Download URL: setuptools_lean-0.2.0rc1.tar.gz
- Upload date:
- Size: 16.1 kB
- Tags: Source
- Uploaded using Trusted Publishing? Yes
- Uploaded via: twine/7.0.0 CPython/3.13.14
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
940906bc3cd09f1180e581f62c9be77112d16e783b1807e109083cd7a9ee32e3
|
|
| MD5 |
1f5d486e4700423a1296719b8ff417e8
|
|
| BLAKE2b-256 |
7cea0812098353f249c7c31e2b8a61d141066c50a348f38872b5f52ac0a7fe0b
|
Provenance
The following attestation bundles were made for setuptools_lean-0.2.0rc1.tar.gz:
Publisher:
release.yml on leanprover/setuptools-lean
-
Statement:
-
Statement type:
https://in-toto.io/Statement/v1 -
Predicate type:
https://docs.pypi.org/attestations/publish/v1 -
Subject name:
setuptools_lean-0.2.0rc1.tar.gz -
Subject digest:
940906bc3cd09f1180e581f62c9be77112d16e783b1807e109083cd7a9ee32e3 - Sigstore transparency entry: 2404345458
- Sigstore integration time:
-
Permalink:
leanprover/setuptools-lean@85e6c45af5632bcae29a9a12d87f86eb7caf0da3 -
Branch / Tag:
refs/tags/v0.2.0rc1 - Owner: https://github.com/leanprover
-
Access:
public
-
Token Issuer:
https://token.actions.githubusercontent.com -
Runner Environment:
github-hosted -
Publication workflow:
release.yml@85e6c45af5632bcae29a9a12d87f86eb7caf0da3 -
Trigger Event:
push
-
Statement type:
File details
Details for the file setuptools_lean-0.2.0rc1-py3-none-any.whl.
File metadata
- Download URL: setuptools_lean-0.2.0rc1-py3-none-any.whl
- Upload date:
- Size: 17.0 kB
- Tags: Python 3
- Uploaded using Trusted Publishing? Yes
- Uploaded via: twine/7.0.0 CPython/3.13.14
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
44d32a6efbdea6b3f15bb0df7bb98c6825a62475bb95ef7677a6a71cb6aab886
|
|
| MD5 |
c26a26b8b88f06c9cbe03eb8594aa5f0
|
|
| BLAKE2b-256 |
1a704deb7e8677770647ee178d20ac86fb37337ec07611ddd9c21fa07260b6a7
|
Provenance
The following attestation bundles were made for setuptools_lean-0.2.0rc1-py3-none-any.whl:
Publisher:
release.yml on leanprover/setuptools-lean
-
Statement:
-
Statement type:
https://in-toto.io/Statement/v1 -
Predicate type:
https://docs.pypi.org/attestations/publish/v1 -
Subject name:
setuptools_lean-0.2.0rc1-py3-none-any.whl -
Subject digest:
44d32a6efbdea6b3f15bb0df7bb98c6825a62475bb95ef7677a6a71cb6aab886 - Sigstore transparency entry: 2404345592
- Sigstore integration time:
-
Permalink:
leanprover/setuptools-lean@85e6c45af5632bcae29a9a12d87f86eb7caf0da3 -
Branch / Tag:
refs/tags/v0.2.0rc1 - Owner: https://github.com/leanprover
-
Access:
public
-
Token Issuer:
https://token.actions.githubusercontent.com -
Runner Environment:
github-hosted -
Publication workflow:
release.yml@85e6c45af5632bcae29a9a12d87f86eb7caf0da3 -
Trigger Event:
push
-
Statement type:
