Dynamically create the LeanFFI class with all bindings.
(model: HeaderModel, structs: dict[str, type])
| 199 | |
| 200 | |
| 201 | def _build_ffi_class(model: HeaderModel, structs: dict[str, type]) -> type: |
| 202 | """Dynamically create the LeanFFI class with all bindings.""" |
| 203 | constants = model.constants |
| 204 | |
| 205 | def __init__(self): |
| 206 | # Preload all Lean runtime shared libraries with RTLD_GLOBAL so |
| 207 | # that downstream user libraries can resolve their @rpath references |
| 208 | # to libleanshared / libLake_shared / libleanshared_1 / etc. |
| 209 | self._preloaded_libs: list[ctypes.CDLL] = [] |
| 210 | for lib in all_lean_runtime_libs(): |
| 211 | try: |
| 212 | self._preloaded_libs.append(ctypes.CDLL(str(lib), mode=ctypes.RTLD_GLOBAL)) |
| 213 | except OSError: |
| 214 | pass |
| 215 | # The "main" libleanshared is the source of all the symbols we |
| 216 | # care about for the FFI; prefer the canonical handle from the |
| 217 | # toolchain. |
| 218 | lib_path = find_lean_dynlib() |
| 219 | self.lib = ctypes.CDLL(str(lib_path), mode=ctypes.RTLD_GLOBAL) |
| 220 | # Additional handles to search for `leanpy_*` helpers. User |
| 221 | # libraries loaded via `LeanLibrary` will register their handle |
| 222 | # here so the FFI's inc/dec/alloc helpers can find the C |
| 223 | # bridge symbols statically linked into the user library. |
| 224 | self._extra_handles: list[ctypes.CDLL] = [] |
| 225 | self._missing_symbols: list[str] = [] |
| 226 | self._bind_exported(self.lib) |
| 227 | self._bind_inline_impls() |
| 228 | |
| 229 | # lean_initialize is not in lean.h but exists in libleanshared |
| 230 | if not hasattr(self, "lean_initialize"): |
| 231 | self.lean_initialize = self.lib.lean_initialize |
| 232 | global _ffi_initialized |
| 233 | if not _ffi_initialized: |
| 234 | _ffi_initialized = True |
| 235 | self.lean_initialize() |
| 236 | # `lean_io_mark_end_initialization` flips the global |
| 237 | # `g_initializing` flag in the Lean runtime from true to false. |
| 238 | # Without it, any Lean code path that calls |
| 239 | # `mkEmptyEnvironment` (e.g. `parseHeader`, used by the |
| 240 | # frontend's `createContextStateFromFile`) raises |
| 241 | # `"environment objects cannot be created during |
| 242 | # initialization"`. We expose it as a method so user-library |
| 243 | # init code can run with the flag still true (which is required |
| 244 | # by Lean's `initialize` blocks), then flip it after. |
| 245 | try: |
| 246 | self.lean_io_mark_end_initialization = self.lib.lean_io_mark_end_initialization |
| 247 | self.lean_io_mark_end_initialization.argtypes = [] |
| 248 | self.lean_io_mark_end_initialization.restype = None |
| 249 | except AttributeError: |
| 250 | self.lean_io_mark_end_initialization = None # type: ignore[assignment] |
| 251 | |
| 252 | def register_handle(self, lib): |
| 253 | """Register an additional dlopen handle as a source of symbols |
| 254 | when looking up `leanpy_*` helpers. Called by `LeanLibrary` after |
| 255 | loading a user dylib.""" |
| 256 | if lib not in self._extra_handles: |
| 257 | self._extra_handles.append(lib) |
| 258 | if hasattr(self, "_helper_cache"): |
no test coverage detected