Skip to content

MEMORY.md

Latest commit

 

History

History
205 lines (170 loc) · 11.9 KB

MEMORY.md

File metadata and controls

205 lines (170 loc) · 11.9 KB
Raw

MEMORY

Durable facts and preferences for this repository. Load this file first in every session, before doing anything else. It is short on purpose. Anything transient belongs in JOURNAL.md; anything about how Lean is written here belongs in vault/Formalization Style.md.

Two kinds of thing live in this file, and they are kept apart deliberately.

  • Environment facts. Properties of this repository and of how Lean has to be run inside it. They are not preferences: code that ignores them either fails to compile or is unusably slow. They ship filled in and correct.
  • Who the user is, and how the user wants to work. This half ships as a template. Fill it in. It is what turns a generic assistant into a useful collaborator, and nothing else in the repository can supply it.

If anything here ever conflicts with what the user says now, the user wins: update the entry, date the change, and say what it supersedes.

TEMPLATE — who and what

Replace this whole section with three or four bullets about yourself, then delete this quoted block. A fresh session reads it before it reads anything else and calibrates everything on it: how much mathematics to explain and what to explain instead, whether to reach for ℕ or ℤ or ZMod n, how long a turn should be, when to stop and ask.

Worth stating explicitly, because the assistant cannot guess any of it:

  • Your mathematical background, and in particular what you are not here to learn. "I know the mathematics, I do not know Lean" produces very different explanations from the default, which assumes neither.
  • The area you are formalizing in.
  • Where you want to start from: ordinary mathematical prose, Lean statements you write yourself, a computation, a textbook you are working through.
  • Your own worst failure mode, if you know it. The example below is real, and it is the reason section 2 of CLAUDE.md exists at all.

Two illustrative bullets, in the format documented at the bottom of this file. Delete both once you have written your own.

  • 2026-08-06 — (EXAMPLE — delete) The user is a professional mathematician working in elementary number theory, not here to learn the mathematics but to learn Lean and Mathlib. Explanations should assume full mathematical fluency and spend every word on the formalization, none on the number theory.
  • 2026-08-06 — (EXAMPLE — delete) The user works from ordinary mathematical prose: a sentence of normal mathematics is typed, the assistant restates it precisely and formalizes it. The user does not write the Lean statement as the starting point. The stated pain point is not remembering Mathlib names, so every name is to be searched and verified, never recalled. (context: project setup)

Environment facts

These describe the repository as it ships. They are true now; if you change a pin or a platform assumption, edit the bullet and date the edit.

Toolchain and build

  • Lean v4.28.0, installed via elan and pinned by lean-toolchain.
  • Mathlib pinned in lakefile.toml to the git tag v4.28.0, deliberately matching the toolchain, so that lake exe cache get finds prebuilt oleans instead of compiling Mathlib from source for hours. lake-manifest.json is committed and records the exact revision.
  • Never start a Mathlib build from source. If the olean cache misses, stop and say so. The matched pin exists precisely to prevent that; lake exe cache get is the repair.
  • lakefile.toml sets autoImplicit = false and relaxedAutoImplicit = false. Every binder must be declared explicitly in every Lean file here, type variables included. A missing binder is a hard error, not a convenience.
  • Default target is NtLean. lake build is reserved for promotion (see CLAUDE.md §3); it is not part of the edit loop.

Verifying a repository, as opposed to verifying its files

"Every module compiles" and "the package builds" are different claims. Checking a .lean file with tools/leanserver.py elaborates it against an environment that is already built; it never reads lakefile.toml or lake-manifest.json. A package can therefore have every module clean and still be unusable by anyone who clones it.

This repository shipped that way. lakefile.toml declared name = "lean-interact", and a hyphen is not a valid Lean identifier, so Lake refused the manifest -- name: expected a 'Name', got '"lean-interact"' -- before doing any work at all. Fixed on 2026-08-08 by renaming the Lake package to lean_interact. The repository directory, the tmux session and the GitHub project keep the hyphenated name; only the package identifier had to change.

Standing rule: any change to lakefile.toml, lake-manifest.json or the module layout is verified with lake build, and anything intended for other people is verified once from a fresh clone. A per-module check does not substitute.

How Lean must be run — measured, not assumed

The numbers below were measured on the machine this harness was built on (16 GB of RAM against 5.4 GB of Mathlib oleans). Absolute values will differ on other hardware; the ratios, and the design decisions they force, will not.

  • Never write import Mathlib in a working file. It costs ~111 s per check. The cause is I/O rather than CPU: the oleans do not fit in the page cache, so every invocation re-reads them. Working files import NtLean.Preamble instead — a focused import surface costing ~24 s one-shot and ~0.25 s through the daemon.
  • To use a module the preamble lacks: add the import to NtLean/Preamble.lean, run lake build NtLean.Preamble, then python3 tools/leanserver.py restart. The daemon loads imports once at worker startup, so without the restart it will report unknown identifier for a lemma that is plainly there.
  • The live loop depends on tools/leanserver.py, a persistent lake env lean --server process that holds the elaborated environment in memory and pushes each edit as an LSP didChange. Warm edit-to-diagnostics is ~0.25 s. leanlib.lean_check_file uses it automatically and falls back to one-shot lake env lean when it is down; LEAN_INTERACT_NO_LSP=1 forces the fallback.
  • Lean runs one language-server worker per open document, so the first check of each file pays the import load (~40 s), once. tools/session.sh pre-warms Scratch/Current.lean for exactly this reason. A slow first check is expected; a slow second one is a bug.
  • When reading Lean's LSP output, the completion signal is $/lean/fileProgress reaching an empty processing list — not a version-matched publishDiagnostics. Lean emits an empty, correctly-versioned diagnostics message the moment it accepts a document, long before elaboration runs, so keying on the version silently reports broken files as clean.

Mathlib names

  • tools/mathlib_index.py indexes ~239,000 Mathlib declarations from source in ~10 s into SQLite FTS. tools/mlq.py searches that index by name, statement, namespace or informal concept.
  • tools/leanserver.py verify NAME... asks the compiler itself and prints the real elaborated types. Verifying 17 names takes ~0.6 s warm.
  • False-negative caveat. verify (and tools/mlq.py --verify) elaborates against NtLean.Preamble, so a genuine Mathlib name living in a module the preamble does not import is reported ABSENT. That is a false negative, not a discovery. Before recording any name in the vault, in book/, or in tools/concept_aliases.json, re-check with verify --full (tools/mlq.py --verify-full), which elaborates against all of Mathlib: slow (~2 min, separate process) but authoritative.
  • The standing invariant. Every Mathlib name cited anywhere in NtLean/, vault/ or book/ must either exist, or carry the marker (absent at Mathlib v4.28.0) on the same line. tools/check_names.py enforces this and exits non-zero otherwise; it also reports broken [[wikilinks]] in the vault. Run it before committing documentation and after any Mathlib bump.
  • Why the rule is absolute. While this repository was built, 353 Mathlib names were written from memory; 27 of them did not exist, and 18 module paths were stale. That is roughly a one-in-ten failure rate for recall. Verification is therefore not a best practice here, it is a precondition.

Platform and tooling

  • Runtime tooling is Python 3 standard library only. No pip installs, no third-party imports, not even a small one. python3 is taken from PATH.
  • Shell scripts are bash and must stay macOS/BSD compatible: no GNU-only flags, no readlink -f, no sed -i without a backup suffix. There is no fswatch, entr or watchexec in the dependency set — file watching is done by polling mtimes.
  • tmux is required by tools/session.sh (two panes: the live watcher, and the dashboard server). jupyter-book is required only to build book/. Nothing in the Lean loop needs either.
  • On macOS the VS Code code CLI is often not on PATH; tools/vscode-setup.sh handles the project-side configuration for the Lean 4 extension.
  • Three live views, all fed by .live/status.json: the terminal watcher (tools/live.py), the VS Code infoview (Lean 4 extension), and the browser dashboard (tools/dashboard.py, bound to 127.0.0.1). They are independent; run any subset.

Magma bridge — optional, and off by default

  • Magma is commercial and usually lives on a departmental server, so tools/magma_run.sh drives it over SSH. Configuration is config.example.sh → config.sh (gitignored), setting LEAN_MAGMA_HOST and LEAN_MAGMA_BIN.
  • With nothing configured the script prints an actionable message rather than failing obscurely. The Lean side of this project needs none of it.
  • Two things break naive invocations, and tools/magma_run.sh handles both: many installations put the binary on the PATH of a login shell only, hence ssh $LEAN_MAGMA_HOST 'bash -lc "..."'; and Magma prints a multi-line startup banner ending in a row of asterisks plus a session-log path, which must be stripped before the real output.

Preferences learned

Append-only. Never rewrite or delete a bullet in this section. If a preference changes, add a new dated bullet saying what it supersedes. The value of this section is that it can be trusted as an audit trail of how the user wants to work; that value disappears the first time something is quietly edited.

Format for each bullet:

- **YYYY-MM-DD** — <the preference, stated as a rule> (context: <where it came up>)
  [supersedes: <date of the bullet it replaces>, if any]

The Lean-writing half of this — naming, statement shape, tactic style, how things are phrased — is recorded in more detail in vault/Formalization Style.md. When a preference is about how Lean code looks, write the full version there and leave a one-line pointer here. When it is about how the user and the assistant work together, the full version lives here.

Two illustrative bullets. Delete both; this section should start empty.

  • 2026-08-06 — (EXAMPLE — delete) Teach as we go. After every formalization, give (a) the Mathlib lemmas used and why each one applies, and (b) exactly one alternative tactic worth knowing for that situation. One alternative, not a survey. (context: asked for explicitly at project start)
  • 2026-08-07 — (EXAMPLE — delete) Interactivity outranks thoroughness. A turn should take seconds: show the compiled Lean plus the short teaching note, then stop. Defer promotion into NtLean/, vault notes, journal bullets, index updates and commits, and flush them when the user pauses or asks. Offer choices rather than performing them; do not batch several results into one turn unless asked. When thoroughness and responsiveness conflict, responsiveness wins and the thorough part is deferred, not dropped. (context: correction after a turn that was complete but slow)