Locate lean.h via the active Lean toolchain. Strategy: 1. Ask `lean --print-prefix` for the toolchain sysroot, look for ` /include/lean/lean.h`. This is the canonical location and works regardless of whether elan, lakefile, or a manual install picked the
()
| 66 | # ============================================================================ |
| 67 | |
| 68 | |
| 69 | def find_lean_header() -> Path: |
| 70 | """Locate lean.h via the active Lean toolchain. |
| 71 | |
| 72 | Strategy: |
| 73 | 1. Ask `lean --print-prefix` for the toolchain sysroot, look for |
| 74 | `<prefix>/include/lean/lean.h`. This is the canonical location |
| 75 | and works regardless of whether elan, lakefile, or a manual |
| 76 | install picked the toolchain. |
| 77 | 2. Fall back to constructing the elan path from the project's |
| 78 | `lean-toolchain` file, for callers who don't have `lean` on PATH. |
| 79 | |
| 80 | A ``LEANPY_BUNDLE_DIR`` bundle ships its own ``lean.h`` so a |
| 81 | wheel-installed library can build its ctypes bindings without a toolchain. |
| 82 | """ |
| 83 | bundle = os.environ.get("LEANPY_BUNDLE_DIR") |
| 84 | if bundle: |
| 85 | for cand in (Path(bundle) / "lean.h", Path(bundle) / "include" / "lean" / "lean.h"): |
| 86 | if cand.exists(): |
| 87 | return cand |
| 88 | |
| 89 | try: |
| 90 | prefix = subprocess.check_output(["lean", "--print-prefix"], text=True).strip() |
| 91 | header = Path(prefix) / "include" / "lean" / "lean.h" |
| 92 | if header.exists(): |
| 93 | return header |
| 94 | except (FileNotFoundError, subprocess.CalledProcessError): |
| 95 | pass |
| 96 | |
| 97 | toolchain_file = Path(__file__).parent.parent / "lean-toolchain" |
| 98 | if toolchain_file.exists(): |
| 99 | toolchain = toolchain_file.read_text().strip() |
| 100 | toolchain_dir = toolchain.replace("/", "--").replace(":", "---") |
| 101 | header = ( |
| 102 | Path.home() / ".elan" / "toolchains" / toolchain_dir / "include" / "lean" / "lean.h" |