| 523 | raise RuntimeError( |
| 524 | f"library does not export an `initialize_*` symbol for " |
| 525 | f"`{self.name}`; was it compiled with `@[python]` attributes " |
| 526 | f"and `precompileModules`/`shared`?" |
| 527 | ) |
| 528 | |
| 529 | def _initialize_lean_module(self) -> None: |
| 530 | init_name = self._resolve_init_symbol() |
| 531 | init_fn = getattr(self.lib, init_name) |
| 532 | init_fn.argtypes = [c_uint8, POINTER(LeanObject)] |
| 533 | init_fn.restype = POINTER(LeanObject) |
| 534 | |
| 535 | result = init_fn(1, ctypes.cast(c_void_p(1), POINTER(LeanObject))) |
| 536 | if result.contents.m_tag != 0: |
| 537 | self.ffi.io_result_show_error(result) |
| 538 | self.ffi.lean_dec(result) |
| 539 | raise RuntimeError(f"{init_name} failed") |
| 540 | self.ffi.lean_dec(result) |
| 541 | # The user library's `initialize_*` block has now run all its |
| 542 | # `initialize` declarations. Flip the runtime's global init |
| 543 | # flag so subsequent calls (e.g. frontend operations that |
| 544 | # invoke `mkEmptyEnvironment` via `parseHeader`) succeed. |
| 545 | # See `lean_py/_runtime.py` for more on why. |