Skip to content

Commit 8485dff

Browse files
kiranandcodekiranandcode
committed
Flesh out @[python] DSL, marshalling, Python-in-Lean bridge, kernel API
Lean → Python: - @[python "name"] now records full TypeRepr metadata in a persistent env extension (LeanPy/Registry.lean, LeanPy/Attr.lean). - derive_python TypeName extracts inductive constructor info. - #export_python_registry "<prefix>" emits two @[export]'d functions returning JSON metadata that the Python loader parses at startup. Python ↔ Lean ABI: - lean_py/marshal.py implements full marshalling for Bool, Int, Nat, String, Float, UInt*, Char, Array, List, Option, Prod, IO, named inductives (incl. enum-only unboxed ABI) and structures. - LeanLibrary auto-generates a Python callable per @[python] function and a wrapper class per derive_python type. Python in Lean: - LeanPy/Python.lean exposes Py opaque type + monadic API (init, eval, exec, import_, getAttr/setAttr, getItem/setItem, call/callKw, repr, numeric ops, of/to conversions). - LeanPy/native/python_bridge.c is the C implementation: a lean_external_class over PyObject* with a finaliser, lazy dlopen of libpython, and proper GIL handling. Kernel facade (Pantograph-equivalent subset): - LeanPy/Kernel.lean: loadEnv, declCount/exists/type, prettyPrint, inferType, whnf — exposed via @[python]. Build / loading: - Lakefile switched to .lean format, adds an extern_lib that compiles the Python C bridge into leanpy_native. - LeanLibrary auto-rewrites @rpath references via install_name_tool on macOS so dylibs load without DYLD_LIBRARY_PATH. - Python side uses ctypes.PyDLL (not CDLL) so the GIL stays held when Lean code calls back into the Python C API. - C-side leanpy_* helpers expose the static-inline lean.h primitives (alloc_ctor, alloc_array, inc/dec, box*, int*) that ctypes can't reach directly. Tests (37, all passing): - test_ffi: dynamic ctypes binding. - test_library: load + initialise. - test_marshal: round-trips for every TypeRepr kind. - test_python_in_lean: end-to-end Lean→Python→Lean via the bridge. - test_sympy_demo, test_lean_side_*: SymPy / NumPy via Lean. - test_kernel: parse, infer type, pretty-print, whnf via Init env. - test_memory: stress + Py refcount sentinels for leak detection. Memory + CI: - tests/leaks_check.sh runs the suite under macOS leaks(1) or Linux valgrind with python.supp suppressions. - .github/workflows/ci.yml matrix expanded to test multiple Lean toolchains plus dedicated leaks/valgrind jobs.
1 parent 79c609a commit 8485dff

29 files changed

Lines changed: 3572 additions & 132 deletions

‎.github/workflows/ci.yml‎

Lines changed: 96 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,41 +2,67 @@ name: CI
22
on: [push, pull_request]
33

44
jobs:
5+
# Run the full test suite on Linux + macOS, against multiple Lean
6+
# toolchain versions. The repo's `lean-toolchain` file pins one but we
7+
# additionally test the latest stable + nightly to catch regressions.
58
test:
69
strategy:
10+
fail-fast: false
711
matrix:
812
os: [ubuntu-latest, macos-latest]
13+
toolchain:
14+
- "default" # whatever lean-toolchain pins
15+
- "leanprover/lean4:v4.25.0"
16+
- "leanprover/lean4:nightly"
917
runs-on: ${{ matrix.os }}
1018
steps:
1119
- uses: actions/checkout@v4
1220

1321
- name: Install elan
1422
run: |
15-
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
23+
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
24+
-sSf | sh -s -- -y --default-toolchain none
1625
echo "$HOME/.elan/bin" >> $GITHUB_PATH
1726
27+
- name: Pick Lean toolchain
28+
id: toolchain
29+
shell: bash
30+
run: |
31+
if [ "${{ matrix.toolchain }}" = "default" ]; then
32+
echo "name=$(cat lean-toolchain)" >> "$GITHUB_OUTPUT"
33+
else
34+
echo "name=${{ matrix.toolchain }}" >> "$GITHUB_OUTPUT"
35+
echo "${{ matrix.toolchain }}" > lean-toolchain
36+
echo "${{ matrix.toolchain }}" > examples/lean/lean-toolchain
37+
fi
38+
1839
- name: Install Lean toolchain
40+
shell: bash
1941
run: |
20-
elan toolchain install $(cat lean-toolchain)
21-
elan default $(cat lean-toolchain)
42+
elan toolchain install ${{ steps.toolchain.outputs.name }}
43+
elan default ${{ steps.toolchain.outputs.name }}
2244
2345
- name: Install uv
2446
uses: astral-sh/setup-uv@v5
2547

2648
- name: Set up Python
2749
run: uv python install 3.12
2850

29-
- name: Install dependencies
51+
- name: Install Python dependencies
3052
run: uv sync --dev
3153

54+
- name: Install demo dependencies (sympy, numpy)
55+
run: uv pip install sympy numpy
56+
3257
- name: Build root Lake project
3358
run: lake build
3459

35-
- name: Build examples
60+
- name: Build PyleanExample
3661
run: lake build
3762
working-directory: examples/lean
3863

39-
- name: Set library path
64+
- name: Set library path (for downstream commands)
65+
shell: bash
4066
run: |
4167
LEAN_SYSROOT=$(lean --print-prefix)
4268
if [ "$RUNNER_OS" == "Linux" ]; then
@@ -47,3 +73,67 @@ jobs:
4773
4874
- name: Run tests
4975
run: uv run pytest tests -v
76+
77+
# macOS-only: run the test suite under `leaks` to check for missing
78+
# ref-count drops. This is slower so kept on a separate job.
79+
memory-macos:
80+
runs-on: macos-latest
81+
needs: test
82+
continue-on-error: true # leaks(1) reports of system frameworks are noisy
83+
steps:
84+
- uses: actions/checkout@v4
85+
- name: Install elan
86+
run: |
87+
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
88+
-sSf | sh -s -- -y --default-toolchain none
89+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
90+
- name: Install Lean toolchain
91+
run: |
92+
elan toolchain install $(cat lean-toolchain)
93+
elan default $(cat lean-toolchain)
94+
- name: Install uv + deps
95+
uses: astral-sh/setup-uv@v5
96+
- run: uv python install 3.12
97+
- run: uv sync --dev
98+
- run: uv pip install sympy numpy
99+
- name: Build
100+
run: |
101+
lake build
102+
(cd examples/lean && lake build)
103+
- name: leaks(1) check
104+
run: tests/leaks_check.sh
105+
106+
# Linux-only: run the test suite under valgrind for stronger coverage
107+
# of definite leaks.
108+
memory-linux:
109+
runs-on: ubuntu-latest
110+
needs: test
111+
continue-on-error: true # valgrind under Python interpreter is noisy
112+
steps:
113+
- uses: actions/checkout@v4
114+
- name: Install elan
115+
run: |
116+
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
117+
-sSf | sh -s -- -y --default-toolchain none
118+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
119+
- name: Install Lean toolchain
120+
run: |
121+
elan toolchain install $(cat lean-toolchain)
122+
elan default $(cat lean-toolchain)
123+
- name: Install valgrind
124+
run: |
125+
sudo apt-get update
126+
sudo apt-get install -y valgrind
127+
- name: Install uv + deps
128+
uses: astral-sh/setup-uv@v5
129+
- run: uv python install 3.12
130+
- run: uv sync --dev
131+
- run: uv pip install sympy numpy
132+
- name: Build
133+
run: |
134+
lake build
135+
(cd examples/lean && lake build)
136+
- name: valgrind check
137+
run: tests/leaks_check.sh
138+
env:
139+
PYTHONMALLOC: malloc

‎.gitignore‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,6 @@ dist/
77
refs/
88
**/__pycache__/
99
.venv/
10-
.cache/
10+
.cache/
11+
_examples/
12+
.pytest_cache/

‎LeanPy.lean‎

Lines changed: 15 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1,38 +1,16 @@
1-
-- This module serves as the root of the `Lean.Py` library.
2-
-- Import modules here that should be built as part of the library.
3-
import Lean.Elab
4-
import Std.Data.HashMap
5-
6-
open Lean Meta Elab
7-
8-
syntax (name := pythonAttr) "python" str : attr
9-
initialize pythonBindsRegistry :
10-
SimplePersistentEnvExtension (Name × String) (List (Name × String)) ←
11-
registerSimplePersistentEnvExtension {
12-
name := `pythonRegistryExt
13-
addEntryFn := (·.cons)
14-
addImportedFn := fun arr => arr.toList.flatMap (·.toList)
15-
toArrayFn := fun es => es.toArray
16-
}
17-
18-
initialize registerBuiltinAttribute {
19-
name := `pythonAttr
20-
descr := "Marks a Lean function to be exposed to Python."
21-
add := fun declName stx kind => do
22-
match stx with
23-
| `(attr| python $ext_name:str) =>
24-
let env <- getEnv
25-
let .some decl := env.find? declName
26-
| throwError s!"[python] could not find decl {declName}"
27-
let ext_name := ext_name.getString
28-
-- @[export "name"]
29-
modifyEnv fun env =>
30-
exportAttr.setParam env declName (.anonymous |>.str ext_name)
31-
|>.toOption.getD env
32-
-- register
33-
modifyEnv fun env =>
34-
pythonBindsRegistry.addEntry env (declName, ext_name)
35-
| _ =>
36-
throwErrorAt stx s!"unexpected syntax for python attribute"
37-
}
1+
/-
2+
LeanPy: effortless Python ↔ Lean bindings.
383
4+
This top-level module re-exports the public surface of the library:
5+
* `LeanPy.Registry` — persistent registry of types/functions exposed to Python
6+
* `LeanPy.TypeRepr` — Lean-side description of types (passed to Python as JSON)
7+
* `LeanPy.Attr` — the `@[python]` attribute and `derive_python` command
8+
* `LeanPy.Export` — runtime export of the registry (queried by Python at startup)
9+
* `LeanPy.Python` — Python-in-Lean: opaque `Py` external class + monadic operations
10+
-/
11+
import LeanPy.Registry
12+
import LeanPy.TypeRepr
13+
import LeanPy.Attr
14+
import LeanPy.Export
15+
import LeanPy.Python
16+
import LeanPy.Kernel

‎LeanPy/Attr.lean‎

Lines changed: 181 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,181 @@
1+
/-
2+
The `@[python "<name>"]` attribute and the `derive_python` command.
3+
4+
`@[python "py_foo"]` does three things:
5+
1. Sets `@[export "py_foo"]` so the C symbol is emitted.
6+
2. Reads the declaration's type, walks parameters, and converts each
7+
parameter and result type into a `TypeRepr` value.
8+
3. Adds a `FuncInfo` entry to the persistent registry.
9+
10+
`derive_python TypeName` walks an inductive declaration and adds a
11+
`TypeInfo` entry to the persistent registry. No accessor functions
12+
are generated — the Python side decodes the constructor tag and
13+
field offsets directly via the C ABI.
14+
-/
15+
import Lean
16+
import LeanPy.Registry
17+
import LeanPy.TypeRepr
18+
19+
open Lean Meta Elab Command
20+
21+
namespace LeanPy
22+
23+
/-- Convert a Lean type expression into a `TypeRepr`.
24+
25+
Recognises a fixed set of well-known types and falls through to
26+
`.named` (for registered user types) or `.opaque` (for anything else).
27+
The walk is purely structural and does not unfold definitions. -/
28+
partial def typeToRepr (env : Environment) (e : Expr) : TypeRepr :=
29+
let e := e.headBeta.cleanupAnnotations
30+
match e with
31+
| .const n _ =>
32+
match n with
33+
| ``Nat => .nat
34+
| ``Int => .int
35+
| ``Bool => .bool
36+
| ``String => .string
37+
| ``Float => .float
38+
| ``Float32 => .float32
39+
| ``Char => .char
40+
| ``Unit => .unit
41+
| ``PUnit => .unit
42+
| ``UInt8 => .uint 8
43+
| ``UInt16 => .uint 16
44+
| ``UInt32 => .uint 32
45+
| ``UInt64 => .uint 64
46+
| ``USize => .uint 64
47+
| ``Int8 => .sint 8
48+
| ``Int16 => .sint 16
49+
| ``Int32 => .sint 32
50+
| ``Int64 => .sint 64
51+
| _ =>
52+
if (Registry.findType? env n).isSome then .named n
53+
else .opaque n
54+
| .app .. =>
55+
let fn := e.getAppFn
56+
let args := e.getAppArgs
57+
match fn with
58+
| .const n _ =>
59+
match n with
60+
| ``Array => if h : args.size > 0 then .array (typeToRepr env args[0]) else .opaque n
61+
| ``List => if h : args.size > 0 then .list (typeToRepr env args[0]) else .opaque n
62+
| ``Option => if h : args.size > 0 then .option (typeToRepr env args[0]) else .opaque n
63+
| ``Prod => if h : args.size > 1 then .prod (typeToRepr env args[0]) (typeToRepr env args[1]) else .opaque n
64+
| ``Sum => if h : args.size > 1 then .sum (typeToRepr env args[0]) (typeToRepr env args[1]) else .opaque n
65+
| ``IO => if h : args.size > 0 then .io (typeToRepr env args[0]) else .opaque n
66+
| ``EIO => if h : args.size > 1 then .except (typeToRepr env args[0]) (typeToRepr env args[1]) else .opaque n
67+
| ``Except => if h : args.size > 1 then .except (typeToRepr env args[0]) (typeToRepr env args[1]) else .opaque n
68+
| _ =>
69+
if (Registry.findType? env n).isSome then .named n
70+
else .opaque n
71+
| _ => .opaque .anonymous
72+
| _ => .opaque .anonymous
73+
74+
/-- Walk a function type, yielding `(paramTypes, returnType)`. Drops type-class
75+
parameters and instance arguments (these are not transmitted to Python). -/
76+
partial def collectFunSig (env : Environment) (type : Expr) : Array TypeRepr × TypeRepr :=
77+
let rec go (params : Array TypeRepr) : Expr → Array TypeRepr × TypeRepr
78+
| .forallE _ d b _ =>
79+
-- Skip instance / type-class style binders heuristically: arrow into
80+
-- something that returns a type, treat as opaque param to keep arity.
81+
let dRepr := typeToRepr env d
82+
go (params.push dRepr) b
83+
| t => (params, typeToRepr env t)
84+
go #[] type
85+
86+
/-- The underlying registration logic, shared by the attribute and the
87+
`derive_python` command. Marked `setExportName := false` to skip rewiring
88+
the `export` attribute when only adding metadata. -/
89+
def doRegisterPython
90+
(declName : Name) (extName : String) (setExportName : Bool := true) :
91+
AttrM Unit := do
92+
let env ← getEnv
93+
let some info := env.find? declName
94+
| throwError s!"[python] could not find decl {declName}"
95+
let (params, ret) := collectFunSig env info.type
96+
let funcInfo : FuncInfo := {
97+
declName, exportName := extName, params, returnType := ret
98+
}
99+
if setExportName then
100+
modifyEnv fun env =>
101+
exportAttr.setParam env declName (.anonymous |>.str extName)
102+
|>.toOption.getD env
103+
modifyEnv (Registry.addFunc · funcInfo)
104+
105+
/-- The `@[python "name"]` attribute. Equivalent to `@[export "name"]`
106+
plus an entry in the persistent function registry. -/
107+
syntax (name := pythonAttr) "python" str : attr
108+
109+
initialize registerBuiltinAttribute {
110+
name := `pythonAttr
111+
descr := "Marks a Lean function to be exposed to Python."
112+
applicationTime := AttributeApplicationTime.afterCompilation
113+
add := fun declName stx _kind => do
114+
match stx with
115+
| `(attr| python $extName:str) =>
116+
doRegisterPython declName extName.getString
117+
| _ =>
118+
throwErrorAt stx "unexpected syntax for @[python]"
119+
}
120+
121+
/-! ### `derive_python` command
122+
123+
`derive_python TypeName` reads the declaration of `TypeName` from the
124+
environment, builds a `TypeInfo`, and stores it in the type registry. No
125+
new declarations are generated — the Python side uses the type info
126+
directly to read constructors / fields out of the runtime object.
127+
-/
128+
129+
/-- Build a `TypeInfo` for a Lean inductive type. -/
130+
def buildTypeInfo (env : Environment) (n : Name) : MetaM TypeInfo := do
131+
let some (.inductInfo iinfo) := env.find? n
132+
| throwError s!"derive_python: {n} is not an inductive type"
133+
let isStructure := isStructure env n
134+
let mut ctors : Array CtorInfo := #[]
135+
let mut isEnum := true
136+
for (cname, idx) in iinfo.ctors.zipIdx do
137+
let some (.ctorInfo ci) := env.find? cname
138+
| throwError s!"derive_python: cannot find constructor {cname}"
139+
-- Walk the constructor type, dropping the inductive's parameters
140+
-- and treating remaining `forallE` binders as fields.
141+
let ctorType := ci.type
142+
-- Skip the leading parameters of the inductive.
143+
let rec skipParams : Nat → Expr → Expr
144+
| 0, e => e
145+
| n+1, .forallE _ _ b _ => skipParams n b
146+
| _+1, e => e
147+
let body := skipParams iinfo.numParams ctorType
148+
let mut fields : Array TypeRepr := #[]
149+
let mut t := body
150+
while t.isForall do
151+
let .forallE _ dom rest _ := t | break
152+
fields := fields.push (typeToRepr env dom)
153+
t := rest
154+
if !fields.isEmpty then isEnum := false
155+
let cname' := cname.componentsRev.head?.map toString |>.getD (toString cname)
156+
ctors := ctors.push { name := cname', tag := idx, fields }
157+
return { name := n, isStructure, isEnum, ctors }
158+
159+
/-- Add a type to the registry, throwing if already present. -/
160+
def doRegisterType (n : Name) : CommandElabM Unit := do
161+
let env ← getEnv
162+
if (Registry.findType? env n).isSome then return ()
163+
let info ← liftTermElabM <| Lean.Meta.MetaM.run' (buildTypeInfo env n)
164+
modifyEnv (Registry.addType · info)
165+
166+
/-- The `derive_python` command. -/
167+
syntax (name := derivePython) "derive_python" ident,+ : command
168+
169+
@[command_elab derivePython]
170+
def elabDerivePython : Command.CommandElab := fun stx =>
171+
match stx with
172+
| `(derive_python $names,*) => do
173+
for n in names.getElems do
174+
let resolved ← liftCoreM <| Lean.realizeGlobalConstNoOverloadCore n.getId
175+
doRegisterType resolved
176+
| _ => throwUnsupportedSyntax
177+
178+
/-- Convenience: register a type (used internally and by user code). -/
179+
def deriveType (n : Name) : CommandElabM Unit := doRegisterType n
180+
181+
end LeanPy

0 commit comments

Comments
 (0)