Initialise Lean's task manager once per process. `Lean.importModules` (and any kernel operation that allocates a `Task`) asserts on `g_task_manager` being non-null. The Lean executable runtime does this for you in `lean_main`; when we host Lean inside Python we need
(self)
| 432 | self._ensure_task_manager() |
| 433 | self._initialize_lean_module() |
| 434 | |
| 435 | self.registry = self._load_registry() |
| 436 | |
| 437 | self.marshaller = Marshaller(self.registry) |
| 438 | self._funcs: dict[str, Callable] = {} |
| 439 | self._types: dict[str, _InductiveType] = {} |
| 440 | |
| 441 | for ti in self.registry.types: |
| 442 | wrapper = ( |
| 443 | _StructureType(ti, self.marshaller) |
| 444 | if len(ti.ctors) == 1 |
| 445 | else _InductiveType(ti, self.marshaller) |
| 446 | ) |
| 447 | short = ti.name.split(".")[-1] |
| 448 | self._types[short] = wrapper |
| 449 | setattr(self, short, wrapper) |
| 450 | |
| 451 | for fi in self.registry.funcs: |
| 452 | wrap = _build_callable(self.lib, fi, self.marshaller) |
| 453 | short = fi.declName.split(".")[-1] |
| 454 | self._funcs[short] = wrap |
| 455 | self._funcs[fi.exportName] = wrap |
| 456 | if not hasattr(self, short): |
| 457 | setattr(self, short, wrap) |
| 458 | if not hasattr(self, fi.exportName): |
| 459 | setattr(self, fi.exportName, wrap) |
| 460 | |
| 461 | # -- internal --------------------------------------------------------- |
| 462 |