Metadata-Version: 2.4
Name: setuptools-lean
Version: 0.2.0
Summary: Setuptools plugin for Lean/Nerodia Python extensions
Author-email: Mac Malone <mac@lean-fro.org>
License-Expression: Apache-2.0
Project-URL: Repository, https://github.com/leanprover/setuptools-lean
Keywords: distutils,setuptools,lean,nerodia
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Topic :: Software Development :: Build Tools
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Programming Language :: Python :: 3.14
Classifier: Operating System :: POSIX
Classifier: Operating System :: MacOS :: MacOS X
Classifier: Operating System :: Microsoft :: Windows
Requires-Python: >=3.14
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: setuptools>=82
Dynamic: license-file

# setuptools-lean

The `setuptools-lean` package provides a [setuptools](https://github.com/pypa/setuptools) plugin for building and bundling Python extensions written in Lean. It uses [Nerodia](https://github.com/leanprover/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**
```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**
```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](https://github.com/astral-sh/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](https://github.com/leanprover/nerodia).
