Library Loading

LeanLibrary is the entry point to lean-py. It loads a compiled Lean shared library, discovers its @[python]-annotated functions and derive_python types, and exposes them as ordinary Python callables.

Source: lean_py/library.py

Loading from a Lake project

The most common way to create a library is from a Lake project directory:

from lean_py import LeanLibrary

lib = LeanLibrary.from_lake("examples/01_basic/lean", "Basic", build=True)

from_lake does three things:

  1. Optionally runs lake build (when build=True).

  2. Locates the shared library under .lake/build/lib/.

  3. Returns a fully initialised LeanLibrary with all wrappers ready.

If the project produces a single shared library, the name can be omitted:

lib = LeanLibrary.from_lake("examples/01_basic/lean", build=True)

Loading from a path

You can also load a pre-built .dylib / .so directly:

lib = LeanLibrary("/path/to/libBasic.dylib", "Basic")

What happens at load time

When you create a LeanLibrary, the following steps execute in order:

  1. dylib is loaded via ctypes.PyDLL with RTLD_GLOBAL so that subsequently loaded libraries can see its symbols.

  2. macOS rpath fixup — on macOS, any @rpath/libFoo.dylib references in the dylib are rewritten to absolute paths under Lean’s lib/lean/ directory. This means you don’t need DYLD_LIBRARY_PATH.

  3. Lean task manager is initialised once per process (required by importModules and any kernel operation that allocates a Task).

  4. Module initialiser is called — the initialize_<LibName> symbol that Lean’s compiler generates. This runs all initialize blocks.

  5. JSON registry is read — the #export_python_registry "LibName" command in Lean emits two C functions (LibName_funcs_json and LibName_types_json) that return JSON describing every exported function and type. LeanLibrary calls these and parses the result into a LibraryRegistry.

  6. Wrappers are built for each function and type. Functions get a Python callable that handles marshalling; types get either an _InductiveType or _StructureType namespace.

Calling functions

Every @[python "name"] function becomes an attribute on the library:

>>> lib.increment(7)
8

>>> lib.greet("world")
'Hello, world!'

>>> lib.sumArray(list(range(1, 11)))
55

The wrapper automatically marshals Python values to Lean objects (and back) according to the type registry. IO-returning functions have their IO unwrapped transparently — if the Lean function throws, Python gets a LeanError.

Working with types

Types registered with derive_python appear as namespaces on the library.

Structures (single-constructor types) are callable:

>>> p = lib.Point(3, 4)
>>> p
Point.mk(3, 4)

>>> lib.normSq(p)
25

Inductives expose each constructor as an attribute:

>>> lib.Shape.circle(5)
Shape.circle(5)

>>> lib.perimeter(lib.Shape.rect(2, 3))
10

Both support Python 3.10+ structural pattern matching:

match shape:
    case lib.Shape.circle(r):
        print(f"circle with radius {r}")
    case lib.Shape.rect(w, h):
        print(f"{w}x{h} rectangle")

And isinstance checks work against constructor classes:

>>> isinstance(lib.Shape.circle(5), lib.Shape.circle)
True

API reference