Scale Anthropic FLT compilation with memory-aware scheduling and DAG caches

Benchmarks/Compile/CompileAnthropicFLT.lean

@@ -0,0 +1 @@
+import FinalCheck

Benchmarks/Compile/README.md

@@ -4,7 +4,8 @@ Test libraries for the Ix compiler
 
 - [Init, Std, and Lean libraries](https://github.com/leanprover/lean4)
 - [Mathlib](https://github.com/leanprover-community/mathlib4)
-- [FLT project](https://github.com/ImperialCollegeLondon/FLT)
+- [Imperial College London FLT project](https://github.com/ImperialCollegeLondon/FLT)
+- [Anthropic FLT proof artifact](https://github.com/anthropics/fermats-last-theorem)
 - Every native TruthMines member, independently, through the generated
   `TruthMines/Members/<Qualifier>.lean` fidelity drivers
 - [Palomar.ix](https://github.com/argumentcomputer/Palomar.ix) as one aggregate
@@ -14,7 +15,100 @@ Test libraries for the Ix compiler
 
 First ensure the Lean version used to build Ix matches the `Benchmarks/Compile/lean-toolchain` version (check against `ix --version`). Then run
 
-`ix compile /path/to/Compile<Lib>.lean` # replace `<Lib>` with `Init`, `InitStd`, `Lean`, `Mathlib`, or `FLT`
+`ix compile /path/to/Compile<Lib>.lean` # replace `<Lib>` with `Init`, `InitStd`, `Lean`, `Mathlib`, `FLT`, or `AnthropicFLT`
+
+To retry only the Ix compiler using existing, up-to-date import artifacts:
+
+```sh
+lake exe ix compile Benchmarks/Compile/CompileAnthropicFLT.lean --no-build --verbose
+```
+
+Run this from the repository root. `--no-build` skips the target's Lake
+build/cache step, including checks for generated C files. The input source is
+still elaborated; missing imports fail, and stale imports are not rebuilt.
+The outer `lake exe` may still rebuild the Ix executable itself.
+
+For allocation-failure diagnostics, set `IX_MEMORY_DIAG=1` to log process
+RSS, virtual memory, swap, system memory availability, and mapping counts
+every five seconds during Ix compilation. `IX_LOG_IND_GROUPS=1` also logs
+each inductive-validation group's entry/exit; unmatched `BEGIN` lines show
+which groups were active if the process aborts. Both are opt-in and leave
+the compilation algorithm unchanged.
+
+Ix pins the [mimalloc Rust fork](https://github.com/argumentcomputer/mimalloc_rust)
+with mimalloc v3.5.1 in `Cargo.toml`. This fixes v3.3.x rejecting its own
+metadata for 16 GiB arenas and eventually exhausting `vm.max_map_count`
+despite available RAM and swap ([upstream issue #1309](https://github.com/microsoft/mimalloc/issues/1309)).
+
+Inductive-flag validation (setup stage 4) uses adaptive admission on Linux.
+The Rayon pool keeps its configured size, but validation starts with two
+active jobs and ramps up while memory is healthy. The controller samples
+`MemAvailable`, visible cgroup-v2 ancestor limits, swap growth, and memory
+stall pressure every 250 ms. It stops admissions and cancels excess attempts
+under pressure; those attempts return normally, drop their scratch data, and
+retry once alone after other work finishes. Completed validations are retained.
+When retained data leaves limited headroom, validation continues one job at a
+time while the safety reserve is available and the system is not reclaiming
+memory. Low headroom alone does not keep resetting the recovery delay.
+Expression walks preserve DAG sharing and check cancellation within the walk.
+
+This is a soft safety mechanism, not a hard allocation limit: an individual
+allocation, lazy import fetch, or destruction cannot be interrupted. A lone
+attempt that exhausts the safety reserve returns `resourceLimit`, not an
+invalid-proof error.
+Non-Linux hosts without telemetry retain ordinary parallel validation.
+
+`--verbose` reports `[validate_memory]` admission/pressure progress.
+`IX_LOG_IND_GROUPS=1` distinguishes `END`, `CANCEL`, and `ERROR` with stable
+group IDs. Optional controls:
+
+- `RAYON_NUM_THREADS`: the pool-size ceiling, not a fixed active-job count.
+- `IX_VALIDATE_MEMORY_GIB`: an additional process RSS-plus-swap soft budget
+  during validation; system/cgroup headroom still applies. Swap is not
+  counted as extra available RAM.
+- `IX_VALIDATE_ADAPTIVE=0`: disable admission control (cannot be combined
+  with an explicit memory budget). DAG-preserving walks remain enabled.
+
+The main dependency scheduler also uses adaptive admission on Linux. It
+starts with up to two active blocks and samples the same memory signals
+every 250 ms, plus a ten-second forecast of recent memory growth. It raises
+concurrency only after completed work and sufficient headroom, stops new
+admissions under pressure, and waits five seconds after recovery before
+resuming. Stable retained output can continue growing with one active block
+while the safety reserve remains available. Main-stage expression transforms
+also preserve DAG sharing instead of repeatedly copying shared subexpressions.
+
+Unlike validation, main-stage blocks publish shared metadata during their
+execution, so active blocks are **not cancelled or retried**: they finish and
+release their scratch before the slot is reused. This is a soft safeguard,
+not a hard memory cap; one large block can still exhaust memory. If no block
+is active and admission cannot resume for 30 seconds, compilation returns
+`resourceLimit`. The gate covers the main block scheduler, not graph setup,
+final serialization, or other work outside that scheduler. Without Linux
+telemetry, the scheduler retains fixed concurrency.
+
+`--verbose` reports `[compile_memory]` limits, active blocks, admissions,
+memory, and growth forecasts. Compilation progress shows recent completions,
+active blocks, and time since the last completion instead of a lifetime-average
+ETA or a `STALLED` label. Optional main-stage controls:
+
+- `IX_COMPILE_WORKERS`: the worker-count ceiling (bounded by available CPUs).
+- `IX_COMPILE_MEMORY_GIB`: an additional process RSS-plus-swap soft budget
+  during main compilation; system/cgroup headroom still applies.
+- `IX_COMPILE_ADAPTIVE=0`: use fixed admission (cannot be combined with
+  `IX_COMPILE_MEMORY_GIB`). DAG-preserving transforms remain enabled.
+
+The Anthropic artifact is also registered as the on-demand `AnthropicFLT`
+benchmark environment. After building its oleans, benchmark the Ix compiler
+and Rust kernel from the repository root with:
+
+```sh
+cd Benchmarks/Compile
+lake build +CompileAnthropicFLT:olean
+cd ../..
+ix bench run --backend compile --env AnthropicFLT
+ix bench run --backend ooc --env AnthropicFLT --ixe AnthropicFLT.ixe
+```
 
 For a TruthMines constituent, use the nested fidelity workspace, for example:
 
@@ -26,4 +120,8 @@ complete sweep with `lake exe truthmines validate`; use `--only Cli,Palomar`
 to select libraries.
 
 > [!NOTE]
-> Compiling Mathlib and FLT currently requires a multi-core CPU and >64 GB RAM.
+> Compiling Mathlib and the Imperial FLT project currently requires a
+> multi-core CPU and >64 GB RAM. Anthropic reports that building its FLT
+> artifact from scratch peaked at 153 GB RAM and used about 67 GB under
+> `.lake/`, plus roughly 220 GB of generated C files. The `olean` facet above
+> skips native object compilation, but Lean still emits those C files.

Benchmarks/Compile/lake-manifest.json

@@ -51,6 +51,16 @@
    "inputRev": "75c0681bd37567af00e8f0bd13fd59f1423e4217",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/anthropics/fermats-last-theorem",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "aa2d8b34692b16c70f699536de0d8e75b9a3e9ef",
+   "name": "flt_e2e",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "aa2d8b34692b16c70f699536de0d8e75b9a3e9ef",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/ImperialCollegeLondon/FLT",
    "type": "git",
    "subDir": null,

Benchmarks/Compile/lakefile.toml

@@ -26,6 +26,9 @@ name = "CompileRedStep"
 [[lean_lib]]
 name = "CompileFLT"
 
+[[lean_lib]]
+name = "CompileAnthropicFLT"
+
 [[lean_lib]]
 name = "CompileMutualFixtures"
 
@@ -41,6 +44,11 @@ name = "flt"
 git = "https://github.com/ImperialCollegeLondon/FLT"
 rev = "v4.33.0"
 
+[[require]]
+name = "flt_e2e"
+git = "https://github.com/anthropics/fermats-last-theorem"
+rev = "aa2d8b34692b16c70f699536de0d8e75b9a3e9ef"
+
 [[require]]
 name = "CompPoly"
 git = "https://github.com/Verified-zkEVM/CompPoly"

Cargo.toml

@@ -55,7 +55,8 @@ itertools = "0.14.0"
 libc = "0.2"
 log = "0.4"
 memmap2 = "0.9"
-mimalloc = { version = "0.1", default-features = false }
+# Bundle v3.5.1 to fix large-arena failures (microsoft/mimalloc#1309).
+mimalloc = { git = "https://github.com/argumentcomputer/mimalloc_rust.git", rev = "616cc1f130d9ea2a1111a46b4e98c140e078f882", default-features = false }
 multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "9a90612286625b6cec59516532d4501677cf468c" }
 nom = "7.1.3"
 num-bigint = "0.4.6"

Ix/Cli/BenchCmd.lean

@@ -103,7 +103,9 @@ def envSpecs : List EnvSpec := [
   -- carries Init and Std).
   { name := "ISLB",    module := "Benchmarks/Compile/CompileISLB.lean" },
   { name := "Mathlib", module := "Benchmarks/Compile/CompileMathlib.lean" },
-  { name := "FLT",     module := "Benchmarks/Compile/CompileFLT.lean" }
+  { name := "FLT",     module := "Benchmarks/Compile/CompileFLT.lean" },
+  { name := "AnthropicFLT",
+    module := "Benchmarks/Compile/CompileAnthropicFLT.lean" }
 ]
 
 def findEnv (token : String) : Option EnvSpec :=
@@ -349,7 +351,11 @@ def backendSpecs : List BackendSpec := [
     testbeds := [("execute", "lean4lean-check-x64-32x")],
     metrics := [("execute", ["check-time", "throughput", "peak-rss",
                              "constants"])] },
+  -- AnthropicFLT remains on-demand: its from-scratch upstream build needs
+  -- substantially more than the per-push workflow's one-hour budget. An
+  -- explicit `--env AnthropicFLT` or `BENCH_ENVS=AnthropicFLT` still runs it.
   { name := "compile", defaultMode := "execute", inputs := .perEnv,
+    envs := some ["InitStd", "Lean", "ISLB", "Mathlib", "FLT"],
     testbeds := [("execute", "ix-compile-x64-32x")],
     metrics := [("execute", ["compile-time", "throughput", "peak-rss",
                              "file-size", "constants"])],

Ix/Cli/CompileCmd.lean

@@ -33,7 +33,10 @@ def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
   let outPath : String :=
     (p.flag? "out").map (·.as! String) |>.getD (defaultOutPathFor pathStr)
 
-  buildFile pathStr
+  -- Reuse existing imports when retrying the Ix compiler. The frontend still
+  -- elaborates the input file; only Lake's dependency build/cache step is skipped.
+  unless p.hasFlag "no-build" do
+    buildFile pathStr
   let fe ← getFileEnvCore pathStr
   let leanEnv := fe.env
 
@@ -241,6 +244,7 @@ def compileCmd : Cli.Cmd := `[Cli|
 
   FLAGS:
     v, verbose;               "Print compiler phase timings, scheduler progress, and serialization progress. Equivalent to IX_VERBOSE=1."
+    "no-build";               "Skip the Lake build/cache step and reuse existing import artifacts. The input file is still elaborated. The caller must ensure all imports are built and up to date."
     out            : String; "Output path for serialized Ixon.Env bytes; defaults to the lowercased input file stem with `.ixe` (e.g. CompileMathlib.lean -> compilemathlib.ixe)"
     consts         : String; "Comma-separated EXACT constant names to compile (transitive deps pulled in automatically) instead of the whole import env — e.g. `Nat.add_comm`. Same flag/shape as `ix check --consts`. Mutually exclusive with --module; --exclude does not apply."
     "consts-file"  : String; "Additionally read seed constant names from a file (one per line; `#` comments and blank lines ignored). Unions with --consts."

Ix/CompileM.lean

@@ -250,14 +250,15 @@ structure BlockEnv where
 
 /-! ## Compilation Error -/
 
-/-- Compilation error type. Variant order matches Rust CompileError (tags 0–5). -/
+/-- Compilation error type. Variant order matches Rust CompileError (tags 0–6). -/
 inductive CompileError where
   | missingConstant (name : String)
   | missingAddress (addr : Address)
   | invalidMutualBlock (reason : String)
   | unsupportedExpr (desc : String)
   | unknownUnivParam (curr param : String)
   | serializeError (err : Ixon.SerializeError)
+  | resourceLimit (reason : String)
   deriving Repr, BEq
 
 instance : ToString CompileError where
@@ -268,6 +269,7 @@ instance : ToString CompileError where
   | .unsupportedExpr desc => s!"unsupportedExpr: {desc}"
   | .unknownUnivParam curr param => s!"unknownUnivParam: compiling {curr}, param {param}"
   | .serializeError err => s!"serializeError: {err}"
+  | .resourceLimit reason => s!"resourceLimit: {reason}"
 
 abbrev CompileM := ReaderT (CompileEnv × BlockEnv) (ExceptT CompileError (StateT BlockState Id))
 

Tests/Cli.lean

@@ -14,8 +14,43 @@ def Tests.Cli.run (buildCmd: String) (buildArgs : Array String) (buildDir : Opti
   else
     IO.println out.stdout
 
+private def Tests.Cli.testCompileNoBuild : IO Unit := do
+  let ix ← IO.FS.realPath ".lake/build/bin/ix"
+  let dir ← IO.FS.createTempDir
+  let source := dir / "NoBuild.lean"
+  let output := dir / "no-build.ixe"
+  try
+    -- No Lake project or compiled target exists here. Only the toolchain's
+    -- implicit Init imports are available; the CLI must elaborate this body.
+    IO.FS.writeFile source
+      "def noBuildMarker : Nat := 7\ntheorem noBuildProof : noBuildMarker = 7 := rfl\n"
+    let args := #["compile", source.toString, "--consts", "noBuildProof",
+      "--out", output.toString]
+    let built ← IO.Process.output { cmd := ix.toString, args := args.push "--no-build" }
+    unless built.exitCode == 0 do
+      throw <| IO.userError s!"compile --no-build failed:\n{built.stdout}\n{built.stderr}"
+    unless (← output.pathExists) && !(← IO.FS.readBinFile output).isEmpty do
+      throw <| IO.userError "compile --no-build did not write a nonempty .ixe"
+    for ext in ["olean", "c"] do
+      if ← (source.withExtension ext).pathExists then
+        throw <| IO.userError s!"compile --no-build unexpectedly wrote a .{ext} file"
+    -- The default path must still require a Lake project/build.
+    let defaultRun ← IO.Process.output { cmd := ix.toString, args }
+    if defaultRun.exitCode == 0 then
+      throw <| IO.userError "compile without --no-build unexpectedly skipped the Lake build"
+    -- Missing imports must fail instead of silently fetching/building them.
+    IO.FS.removeFile output
+    IO.FS.writeFile source "import IxCliNoBuildMissingImport\n"
+    let missing ← IO.Process.output { cmd := ix.toString, args := args.push "--no-build" }
+    if missing.exitCode == 0 || (← output.pathExists) then
+      throw <| IO.userError "compile --no-build accepted a missing import"
+    IO.println "compile --no-build: source elaboration, output, default build, and missing-import checks passed"
+  finally
+    IO.FS.removeDirAll dir
+
 public def Tests.Cli.suite : IO UInt32 := do
   Tests.Cli.run "lake" (#["exe", "ix", "--help"]) none
+  Tests.Cli.testCompileNoBuild
   --Tests.Cli.run "ix" (#["store", "ix_test/IxTest.lean"]) none
   --Tests.Cli.run "ix" (#["prove", "ix_test/IxTest.lean", "one"]) none
   return 0

Tests/FFI/Ix.lean

@@ -250,7 +250,8 @@ def compileErrorTests : TestSeq :=
   test "CompileError.invalidMutualBlock" (roundtripCompileError (.invalidMutualBlock "empty") == .invalidMutualBlock "empty") ++
   test "CompileError.unsupportedExpr" (roundtripCompileError (.unsupportedExpr "mvar") == .unsupportedExpr "mvar") ++
   test "CompileError.unknownUnivParam" (roundtripCompileError (.unknownUnivParam "Nat" "u") == .unknownUnivParam "Nat" "u") ++
-  test "CompileError.serializeError" (roundtripCompileError (.serializeError se) == .serializeError se)
+  test "CompileError.serializeError" (roundtripCompileError (.serializeError se) == .serializeError se) ++
+  test "CompileError.resourceLimit" (roundtripCompileError (.resourceLimit "memory reserve") == .resourceLimit "memory reserve")
 
 /-! ## Test Suite -/
 

Tests/Gen/Ix.lean

@@ -665,7 +665,8 @@ def genCompileError : Gen Ix.CompileM.CompileError := do
     (1, pure (.invalidMutualBlock s)),
     (1, pure (.unsupportedExpr s)),
     (1, do let s2 ← genIxString; pure (.unknownUnivParam s s2)),
-    (1, pure (.serializeError se))
+    (1, pure (.serializeError se)),
+    (1, pure (.resourceLimit s))
   ] (pure default)
 
 instance : Shrinkable Ix.CompileM.CompileError where