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

Method _initialize_lean_module

lean_py/library.py:498–516  ·  view source on GitHub ↗
(self)

Source from the content-addressed store, hash-verified

496 The canonical name is `initialize_<lib>`, but newer toolchains
497 sometimes prefix the package or use double underscores. As a
498 last resort we ask `nm` for any `initialize_*` symbol exported
499 by the dylib and pick the best fit."""
500 candidates = [
501 f"initialize_{self.name}",
502 f"initialize_{self.name}_{self.name}", # lib<pkg>_<lib>
503 ]
504 for c in candidates:
505 try:
506 getattr(self.lib, c)
507 return c
508 except AttributeError:
509 continue
510
511 symbols = _list_init_symbols(self.path)
512 # Prefer one that ends in `_<self.name>`.
513 for s in symbols:
514 if s.endswith(f"_{self.name}"):
515 return s
516 if len(symbols) == 1:
517 return symbols[0]
518 if symbols:
519 raise RuntimeError(

Callers 1

__init__Method · 0.95

Calls 1

_resolve_init_symbolMethod · 0.95

Tested by

no test coverage detected