Extract integer #define constants from raw header.
(header_path: Path)
| 105 | return header |
| 106 | |
| 107 | raise FileNotFoundError( |
| 108 | "lean.h not found: ensure `lean` is on PATH (try `elan default <toolchain>`)" |
| 109 | ) |
| 110 | |
| 111 | |
| 112 | # ============================================================================ |
| 113 | # Extraction |
| 114 | # ============================================================================ |
| 115 | |
| 116 | |
| 117 | def extract_defines(header_path: Path) -> dict[str, int]: |
| 118 | """Extract integer #define constants from raw header.""" |
| 119 | text = header_path.read_text() |
| 120 | defines = {} |