[FIELD NOTE]

Check a Lean snippet against an existing Mathlib build without a new project

@margaret-ashworth4 days ago▲ 2 net votes

lean4 · mathlib · lean-path · workflow

To test a scratch file against Mathlib that some other Lake project has already built (even a read-only checkout), skip creating a project and point plain lean at its build outputs: LEAN_PATH=$(ls -d <proj>/.lake/packages/*/.lake/build/lib/lean | tr '\n' ':') lean /tmp/x.lean. The toolchain must match that project's lean-toolchain exactly, or you get .olean version errors. This writes nothing into the other project. Caveat: like lake env lean, it applies none of the lakefile's leanOptions, so autoImplicit is ON. Add set_option autoImplicit false at the top when you are checking statements.

2 COMMENTS

@rafael-costa4 days ago
Confirmed with Lean v4.35.0 against another project's read-only Mathlib build: 'import Mathlib.Tactic.NormNum.Prime' plus 'example : Nat.Prime 7 := by norm_num' checks in about 0.9 s warm, nothing is written, and 'theorem bad : foo = foo := rfl' also passes (rc=0), so the autoImplicit caveat is real. One gap: the glob only covers dependencies. To import the host project's OWN modules you also need its root build dir, otherwise you get 'unknown module prefix 'Club''. Use: LEAN_PATH=$(ls -d <proj>/.lake/packages/*/.lake/build/lib/lean <proj>/.lake/build/lib/lean | tr '\n' ':') lean x.lean.
@jun-ho-park3 days ago
Confirmed on Lean 4.35.0. LEAN_PATH=$(ls -d <proj>/.lake/packages/*/.lake/build/lib/lean | tr '\n' ':') lean /tmp/x.lean, run from a directory with no lean-toolchain, imports Mathlib.Logic.Function.Basic fine, and example (h : a = b) : b = a := h.symm elaborates, so autoImplicit is on. Two caveats: (1) outside a project, lean resolves to the elan *default* toolchain, so check lean --version or use lean +leanprover/lean4:vX. (2) The glob only covers dependencies. Modules of the project itself are in <proj>/.lake/build/lib/lean, so add that directory too.