Load a Lean library from a Lake project directory. Looks for ` /.lake/build/lib/lib . ` (or, when `library_name` is omitted, the single shared library produced by the project). Pass `build=True` to run `lake build` in `lake_dir` first.
(
cls,
lake_dir: str | os.PathLike,
library_name: str | None = None,
*,
build: bool = False,
)
| 279 | v = ctypes.cast(v, c_void_p).value if v is not None else 0 |
| 280 | elif w.ctype in (c_uint8, ctypes.c_uint16) and not isinstance(v, int): |
| 281 | # Enum/Bool: `to_lean` produces a boxed scalar pointer so it |
| 282 | # round-trips through nested struct fields, but a top-level |
| 283 | # uint8/uint16 parameter expects the raw tag. Unbox here. |
| 284 | v = _ffi.lean_unbox(v) |
| 285 | cargs.append(v) |
| 286 | if is_io: |
| 287 | cargs.append(c_void_p(1)) |
| 288 | result_raw = cfn(*cargs) |
| 289 | if return_is_pointer: |
| 290 | result_ptr = ctypes.cast(c_void_p(result_raw), LObjPtr) |
| 291 | return rwrap.from_lean(result_ptr) |
| 292 | return rwrap.from_lean(result_raw) |
| 293 | |
| 294 | _wrapper.__name__ = finfo.exportName |
| 295 | _wrapper.__qualname__ = f"LeanLibrary.{finfo.exportName}" |
| 296 | _wrapper.__doc__ = ( |
| 297 | f"Lean function `{finfo.declName}` exposed as `{finfo.exportName}`.\n" |
| 298 | f"Signature: ({', '.join(p.short() for p in finfo.params)}) -> {ret.short()}" |
| 299 | ) |
| 300 | return _wrapper |
| 301 | |
| 302 | |
| 303 | # ============================================================================ |
| 304 | # LeanLibrary |
| 305 | # ============================================================================ |
| 306 | |
| 307 | |
| 308 | class LeanLibrary: |
| 309 | """A loaded Lean library with `@[python]` bindings.""" |
| 310 | |
| 311 | @classmethod |
| 312 | def from_lake( |
| 313 | cls, |
| 314 | lake_dir: str | os.PathLike, |
| 315 | library_name: str | None = None, |
| 316 | *, |
| 317 | build: bool = False, |
| 318 | ) -> LeanLibrary: |
| 319 | """Load a Lean library from a Lake project directory. |
| 320 | |
| 321 | Looks for `<lake_dir>/.lake/build/lib/lib<library_name>.<ext>` |
| 322 | (or, when `library_name` is omitted, the single shared library |
| 323 | produced by the project). Pass `build=True` to run `lake build` |
| 324 | in `lake_dir` first. |
| 325 | """ |
| 326 | lake_path = Path(lake_dir).resolve() |
| 327 | if not lake_path.is_dir(): |
| 328 | raise FileNotFoundError(f"not a Lake project directory: {lake_path}") |
| 329 | if build: |
| 330 | run_command(["lake", "build"], cwd=lake_path) |
| 331 | |
| 332 | ext = shared_lib_extension() |
| 333 | build_root = lake_path / ".lake" / "build" |
| 334 | lib_dir = build_root / "lib" |
| 335 | |
| 336 | def _find(name: str) -> Path | None: |
| 337 | """Locate `lib<name>.<ext>` produced by `lake build`. |
| 338 |