Method _resolve_init_symbol

lean_py/library.py:461–496

Resolve the module-initializer symbol, allowing for the Lake-naming variations Lean has gone through. The canonical name is `initialize_ `, but newer toolchains sometimes prefix the package or use double underscores. As a last resort we ask `nm` for any `initiali

(self)

                setattr(self, fi.exportName, wrap)

    # -- internal ---------------------------------------------------------

    _task_manager_initialized: bool = False

    def _ensure_task_manager(self) -> None:
        """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 to call it ourselves. Idempotent.
        """
        if LeanLibrary._task_manager_initialized:
            return
        # The symbol lives in libleanshared, not the user dylib.
        # Try the user dylib first (works on macOS with RTLD_GLOBAL),
        # then fall back to the FFI's lean shared lib handle.
        init = None
        for handle in (self.lib, self.ffi.lib):
            try:
                init = handle.lean_init_task_manager
                break
            except AttributeError:
                continue
        if init is None:
            return
        init.argtypes = []
        init.restype = None
        init()
        LeanLibrary._task_manager_initialized = True

    def _resolve_init_symbol(self) -> str:
        """Resolve the module-initializer symbol, allowing for the
        Lake-naming variations Lean has gone through.

        The canonical name is `initialize_<lib>`, but newer toolchains
        sometimes prefix the package or use double underscores. As a
        last resort we ask `nm` for any `initialize_*` symbol exported
        by the dylib and pick the best fit."""