Function get_header_model

lean_py/_parse.py:338–369

Parse lean.h and return the HeaderModel, using a disk cache for speed.

()

                    model.exported_functions.append(func)

    return model


# ============================================================================
# Public API
# ============================================================================

_CACHE_DIR = Path(__file__).parent.parent / ".cache"


def get_header_model() -> HeaderModel:
    """Parse lean.h and return the HeaderModel, using a disk cache for speed."""
    header_path = find_lean_header()
    header_hash = hashlib.md5(header_path.read_bytes()).hexdigest()

    cache_file = _CACHE_DIR / f"lean_h_{header_hash}.pickle"
    if cache_file.exists():
        try:
            return pickle.loads(cache_file.read_bytes())
        except Exception:
            pass

    # Parse fresh
    preprocessed = _preprocess(header_path)
    parser = pycparser.CParser()
    with open(preprocessed) as f:
        source = f.read()
    try:
        ast = parser.parse(source, filename=str(preprocessed))
    except ParseError as e:
        raise RuntimeError(f"Failed to parse lean.h: {e}") from e
    finally:
        preprocessed.unlink(missing_ok=True)

    defines = extract_defines(header_path)