Dev environment

How to set up + use the bang-lang dev tooling. Most things "just work" after nix develop; this doc lists the levers and what each does.

Why Nix manages elan, NOT Lean itself

Mathlib's olean cache is keyed to the official Lean toolchain build (hash). If Nix builds Lean itself, the hash diverges and the cache misses — every build then recompiles Mathlib from source (multi-GB, hours).

Our flake.nix deliberately ships pkgs.elan only, not pkgs.lean. Elan reads lean-toolchain and fetches the official Lean release. Mathlib's Azure-hosted cache stays live; lake exe cache get populates oleans in seconds.

For hermetic reproducibility (e.g. CI), the second path is lean4-nix — slow Mathlib rebuild is fine there because CI doesn't iterate. Keep it out of the daily dev shell.

First-time setup

cd /srv/share/projects/lang-bang
nix develop          # opens Lean 4 dev shell (or auto-entered via direnv)
lake exe cache get   # one-time: pull Mathlib oleans from Azure (multi-GB)
just verify          # selfcheck + lake build + tools/audit.sh
bash tools/install-hooks.sh   # one-time: link git pre-commit hook

Direnv (.envrc uses use flake) auto-enters the dev shell on cd once direnv allow is run.

Production docs shell

The Vocs site deliberately uses a separate, opt-in shell so every Lean session does not carry Bun + Chromium. One command enters the flake-pinned site shell, installs the locked JavaScript graph, requires every Mermaid render, and builds the static site:

just site-build

This is the local equivalent of Site CI, Pages deployment, and the release-site gate. bun run dev remains an authoring loop with per-diagram fallback; just site-build is strict and fails if Chromium, mmdc, or any diagram fails.

Editor

.editorconfig keeps indent (2-space, Mathlib convention) consistent.

Make targets

Scripts (tools/)

Lean warning budget

Historical Lean warnings are tracked in docfacts/lean-warning-budget.json by module and stable category. just build runs lake build Bang bang once, covering the complete library and native runner while streaming compiler output unchanged, and then enforces the budget. Lake replays stored diagnostics, so cached and cold builds take the same path. A reduction passes immediately; an increased count, a new module, a new category, or an unrecognized warning shape fails. The budget is also bound to lean-toolchain plus the platform-independent Lean version, commit, and build flavor parsed from lean --version, so a toolchain change requires an explicit review and regeneration without making one host's target triple part of the baseline.

Located dependency diagnostics are deliberately excluded. Any warning: line without a source location is ambiguous—it cannot be attributed to the project or a dependency—so the gate conservatively rejects it on both check and update paths. There is no broad locationless exception: a real non-diagnostic notice that must coexist with the compiler stream needs a narrow reviewed classifier rule instead of silently bypassing the budget.

The target is zero warnings. After fixing warnings, shrink the committed ceiling with:

just warnings-update
git diff -- docfacts/lean-warning-budget.json
just warnings

warnings-update requires a successful build, refuses unknown warning shapes, writes sorted unique buckets deterministically, and replaces the file atomically. Do not use it merely to accept an increase: inspect and fix the regression unless the increase is an intentional, reviewed exception.

Iteration loop (recommended)

For Phase A part 2 / Phase B work:

# Edit Bang/Spec.lean or Bang/Meta/BinaryLR.lean or Bang/Eval.lean ...
 
bash tools/check.sh Bang/Spec.lean     # fast: just this file's errors
# repeat until clean
 
just audit                              # full gate before committing
bash tools/burndown.sh                  # see remaining sorrys/axioms
 
git add -A && git commit -m "..."       # pre-commit hook runs static guards

tools/check.sh Bang/Spec.lean is faster than just build because it type-checks just one file (still pulling its dependencies via the lake cache). Use this constantly while editing.

Audit + #print axioms

The real Phase B gate is Bang/Audit.lean. Run it directly:

nix develop --command lake env lean Bang/Audit.lean

Output: each headline theorem's transitive axiom dependencies. Phase B closes when each set ⊆ {propext, Classical.choice, Quot.sound}.

Currently (Phase A part 1) the burndown shows sorryAx plus the specific axioms each theorem touches (e.g. lr_fundamental depends on [sorryAx, Crel, HasCTy]). Each axiom is a Phase B target.

Loogle — Mathlib type-signature search

just loogle "?n + 0 = ?n"                       # hits the web service (loogle.lean-lang.org)
just loogle "Finset _ → Finset _ → Finset _"

Returns Mathlib lemmas matching the shape. Loogle is NOT a build dependency — agents should prefer the lean_loogle MCP tool (richer, no shell). The just loogle recipe queries the public web service; nothing is fetched or built locally.

RESOLVED (2026-06-26, task #19) — the loogle re-clone hazard is gone at the root. Previously loogle was a require in lakefile.toml (a dev-only tool, NEVER imported by Bang). In a fresh git worktree, lake exe cache get re-resolved it ("URL has changed; deleting and cloning again" → fatal: unable to read tree <sha> → exit 128), and loogle's untracked frontend-tests/*.py aborted lake's checkout — triggering a clobbering re-clone that corrupted the SHARED worktree object store. This flaked the pre-commit just verify, forced BANGLANG_SKIP_VERIFY_REASON commits (bypassing the build gate), and once trapped ~600 lines of green proof uncommitted. Fixed by removing loogle from the dependency graph entirely — removal doesn't fetch, so it can't trigger the hazard, and since Bang never imported loogle the build graph is unchanged. If a Bang module ever needs loogle as a library, re-add it pinned to a TAG (not master) — but it does not.

tools/eval.sh — submit Lean snippet, get elaborator output

echo '#check @Bang.Comp.handle' | bash tools/eval.sh
echo '#print Bang.HasCTy' | bash tools/eval.sh

Snippet runs with import Bang.Audit; open Bang prepended (Bang.Audit is the apex re-exporter — the former import Bang barrel was retired for the Bang.+ lake glob). Useful for exploration without editing a file. AI agents / scripts can shell out here for programmatic Lean access without an MCP bridge.

Tools to consider adding (deferred)

Stale-doc check

If something in this doc no longer matches reality (e.g. a make target was renamed), tools/check.sh and just verify are the ground truth. This doc is hand-maintained.