buddend/lean-mathlib-compiler-v4291

lean-mathlib-compiler

Persistent Lean 4 + Mathlib compilation endpoint. Backs the lean skill's mode="mathlib" and mode="auto_mathlib" paths.

Endpoints

• —GET /health — returns {ok, lean_version, mathlib_pin}. Use to verify the Space is awake before paying compile-call latency.
• —POST /compile with {snippet: str} — compiles the snippet against the baked Mathlib, returns {stdout, exit_code, lean_version, mathlib_pin}.

Deploying

1. 1.Create the Space on huggingface.co:
2. 2.SDK: Docker
3. 3.Hardware: CPU upgrade (16 GB RAM minimum — basic 16 GB tier works for most snippets; bump if you import heavy Mathlib sections like Mathlib.NumberTheory.Cyclotomic.*).
4. 4.Visibility: private + token, or public (your call).

1. 1.Set repo secrets (Settings → Repository secrets):
2. 2.LEAN_SPACE_TOKEN (optional) — if set, all requests must send Authorization: Bearer <token> matching it. Recommended for private use.

1. 1.Set build args (Settings → Variables):
2. 2.MATHLIB_REV — Mathlib git rev. Default master. Pin to a commit for reproducibility. Tags like v4.15.0 also work.
3. 3.LEAN_TOOLCHAIN — optional sanity check. If set, build fails if the toolchain in Mathlib's lean-toolchain file doesn't match. Leave unset to accept whatever Mathlib pins.

1. 1.Push the files (Dockerfile, app.py, this README.md) to the Space repo. HF builds the image. First build is slow (~15-25 min, mostly lake exe cache get pulling oleans).

1. 1.Get the endpoint URL: https://<user>-<space-name>.hf.space. The /compile endpoint is at https://<user>-<space-name>.hf.space/compile.

1. 1.Configure the skill: in your environment,

   export LEAN_MATHLIB_ENDPOINT="https://<user>-<space-name>.hf.space/compile"
   export HF_TOKEN="<the LEAN_SPACE_TOKEN value if you set one>"

Or pass endpoint_url= / hf_token= explicitly to verify(..., mode="mathlib").

Bumping Mathlib

Change MATHLIB_REV build arg → factory-reboot the Space (Settings → Factory rebuild). ~15-25 min later, new Mathlib is live.

Sleep behaviour

HF Spaces on free CPU tier sleep after ~48h of inactivity. Cold-wake is ~30-60s. For active campaigns: either upgrade to a persistent tier (~$0.05/hr), or hit /health on a 12h cron from anywhere to keep warm.

The skill-side lean_mathlib.healthcheck() is the right tool for the warmup ping.

Resource ceilings

The free 16 GB CPU tier comfortably handles snippets that import a few specific Mathlib modules (Mathlib.Analysis.SpecialFunctions.*, Mathlib.NumberTheory.LSeries.*, etc.). A bare import Mathlib (everything) will spike memory significantly — prefer specific imports.

If you hit OOM kills, options in order of preference:

1. 1.Tighten imports in your snippet to specific submodules.
2. 2.Upgrade Space hardware to 32 GB.
3. 3.Build a slim Mathlib subset image (only the modules you need; ~5x faster builds, ~3x smaller image).

Auth

If LEAN_SPACE_TOKEN is unset, the Space is open. Anyone with the URL can compile against it. For solo use this is usually fine. For team use or anything publicly linked, set the token.

Troubleshooting

• —Build fails at `lake exe cache get`: Mathlib commit doesn't have a cached olean set yet (happens on bleeding-edge commits). Pick a slightly older commit, or run lake build (slow — multi-hour) by dropping the lake exe cache get line. Cache is the right path for any stable rev.
• —`/compile` returns exit_code=124: snippet timed out (default 120s). Either the snippet is genuinely heavy (e.g. unfolds a slow Mathlib def) or the Space is cold. Hit /health to wake, retry. Override via COMPILE_TIMEOUT env var on the Space.
• —`unknown identifier 'X'`: Mathlib lemma name has changed between versions. Check at the pinned commit on github.com/leanprover-community/mathlib4.