MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / __init__

Method __init__

lean_py/library.py:385–428  ·  view source on GitHub ↗
(self, dylib_path: str | os.PathLike, library_name: str)

Source from the content-addressed store, hash-verified

383 found = _find(library_name)
384 if found is None:
385 raise FileNotFoundError(
386 f"lib{library_name}{ext} not found under {build_root}; "
387 f"check the library name or run `lake build`. {_diagnostic()}"
388 )
389 return cls(found, library_name)
390
391 # Auto-detect: pick the unique shared lib (excluding .hash/.trace/.rsp).
392 shared = []
393 if build_root.is_dir():
394 shared = [
395 p
396 for p in build_root.rglob(f"lib*{ext}")
397 if p.suffix == ext and not p.name.endswith((".hash", ".trace", ".rsp"))
398 ]
399 if not shared:
400 raise FileNotFoundError(
401 f"no shared library found under {build_root}; run `lake build`. {_diagnostic()}"
402 )
403 if len(shared) > 1:
404 names = ", ".join(p.stem.removeprefix("lib") for p in shared)
405 raise RuntimeError(
406 f"multiple shared libraries under {build_root} ({names}); pass "
407 f"library_name to disambiguate"
408 )
409 # The library_name we report should be the second half of
410 # `lib<pkg>_<name>` if that pattern is in play; otherwise the
411 # whole post-`lib` stem.
412 stem = shared[0].stem.removeprefix("lib")
413 name = stem.split("_", 1)[1] if "_" in stem else stem
414 return cls(shared[0], name)
415
416 def __init__(self, dylib_path: str | os.PathLike, library_name: str):
417 self.path = Path(dylib_path)
418 self.name = library_name
419 self.ffi = get_lean_ffi()
420 # Ensure the dylib can resolve its @rpath references to Lean's runtime.
421 _ensure_rpath(self.path)
422 # Use `PyDLL` so that ctypes does NOT release the GIL when calling
423 # into Lean. This matters for `LeanPy.Python.*` functions which
424 # call back into the Python C API: those calls require the GIL
425 # to be held by the calling thread.
426 self.lib = ctypes.PyDLL(str(self.path), mode=ctypes.RTLD_GLOBAL)
427
428 # Make this dylib's `leanpy_*` C-bridge symbols visible to the
429 # FFI helper-lookup chain (used by ref-count and allocation ops).
430 self.ffi.register_handle(self.lib)
431

Callers 1

__init__Method · 0.45

Calls 9

_ensure_task_managerMethod · 0.95
_load_registryMethod · 0.95
MarshallerClass · 0.90
get_lean_ffiFunction · 0.85
_ensure_rpathFunction · 0.85
_StructureTypeClass · 0.85
_InductiveTypeClass · 0.85
_build_callableFunction · 0.85

Tested by

no test coverage detected