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

[johnchandlerburnham]

Summary

Add the Anthropic Fermat's Last Theorem artifact as an on-demand benchmark,
and make the Ix compilation pipeline practical for its large expression DAGs.
The changes cover cached-artifact retries, allocation diagnostics, adaptive
admission, and eliminating repeated traversal of shared subexpressions.

Changes

• Add CompileAnthropicFLT.lean and register the AnthropicFLT benchmark.
  Pin the upstream proof artifact and retain the workspace's Mathlib pin.
• Add ix compile --no-build to reuse existing import artifacts without
  rerunning the target's Lake build/cache step. The input file is still
  elaborated; callers must ensure the imports are present and up to date.
• Pin the mimalloc Rust fork bundling mimalloc v3.5.1 for the large-arena
  allocation failure encountered during the FLT runs.
• Add optional process/system memory diagnostics and per-group progress logs.
  Report active work and time since the last completion without implying that
  a long-running block is deadlocked.
• Use Linux memory telemetry, cgroup-v2 headroom, swap growth, and memory
  pressure to control admission to validation and main compilation.
  The pool-size ceiling remains fixed; the number of admitted jobs changes.
• Make validation expression walks cancellation-aware and DAG-preserving.
  Cancelled validation attempts discard scratch state and retry alone.
  Main compiler blocks are not cancelled because they publish shared state.
• Fold setup scanning into chunk-local accumulators, reducing per-constant
  map allocations while preserving graph, grounding, and group results.
• Add call-local DAG memoization to the Lean/kernel expression bridge and
  kernel expression/universe interner, preserving sharing and metadata.
• Make source-name hint collection and restoration DAG-aware. Match content
  using exact shallow structural identities, avoiding repeated temporary
  kernel-expression construction and unchecked 64-bit hash equality.
• Add frozen, test-only reference implementations, differential regression
  tests, forced-collision tests, and opt-in synthetic benchmarks.

Correctness boundaries

• Caches are scoped to one call/pass, with the required binder depth and
  conversion context. Pointer-keyed caches retain their original input roots
  and never use rebuilt temporaries as input identities.
• Source-name matching uses a fixed pass-local view of referenced addresses.
  It does not retain lookups across calls or claim an atomic snapshot of all
  shared compiler state.
• Hint collection remains preorder, left-to-right, and first-insert-wins.
  Restoration starts after collection finishes. Eligibility remains App/Proj
  with no bound-variable node anywhere, including underneath binders.
• Structural equality confirms hash-table hits; temporary content IDs never
  enter serialized output. Restoration caches distinguish metadata-bearing
  occurrences even when their anonymous content is equal.
• Admission is a soft safeguard, not a hard memory cap or thread preemption.
  One large allocation or block can still exhaust memory. Resource exhaustion
  is reported separately from invalid-proof errors.

Measurements

Measured on Linux with 64 logical CPUs, approximately 495 GiB RAM, cached
import artifacts, and the same adaptive admission settings before/after the
source-name cache. These are Ix recompilation measurements, not cold builds
of the Lean libraries.

Benchmark	Timing scope	Before source-name cache	With source-name cache	Output comparison
Anthropic FLT	Whole command wall time	16m 13.60s	6m 51.92s	Byte-identical
Mathlib	Compiler-reported elapsed time	55.85s	56.11s	Byte-identical

• FLT is 2.36x faster (58% less wall time) with the source-name cache.
  Both sides already include the DAG-aware interner. Peak RSS was
  138.8 GiB before and 146.5 GiB afterward. It compiles 1,930,038 source
  constants and writes 30,113,168,066 bytes (28.0 GiB).
• Mathlib timing is essentially unchanged. Peak RSS was 21.2 GiB before
  and 20.2 GiB afterward; it compiled 771,129 source constants. The controlled
  comparison used the immediately preceding implementation, not the older
  September 1 artifact, which uses a different .ixe format version.
• The earlier pre-interner FLT run took 49m 22.55s. Its output was also
  byte-identical, but cache warmth differed, so this is not a controlled
  measurement of the interner alone.
• On the synthetic depth-16 shared-DAG hint-restoration case, the old pass
  took about 176 ms versus 25 microseconds with caching. This isolates a
  pathological shared-DAG case, not general compiler throughput.

Validation

• Kernel/compiler library suites: 988 passing tests in debug and release
  (700 kernel and 288 compiler; manual benchmarks remain ignored).
• Clippy for the compiler library and tests with warnings denied.
• Rust formatting and whitespace checks.
• Remote lake build ix IxTests, FFI tests, and CLI tests passed.
• Init and Lean recompilations are byte-identical to their prior artifacts.
• Full FLT recompilation and controlled Mathlib before/after comparisons are
  byte-identical, including metadata.
• Regression coverage includes binder depth, alias spellings, metadata,
  universe normalization, first-hint-wins ordering, changing address
  resolution between passes, deliberate hash collisions, and shared DAGs.

The remote integration checks used the existing cached workspace with this
compiler/kernel patch set. They were not a fresh build of every dependency
on the latest main branch. Local validation targets the kernel/compiler
crates; the full workspace has a separate Rust toolchain requirement.

Reproduce a cached run

From the repository root, after building the benchmark's import artifacts:

export LEAN_NUM_THREADS=64 RAYON_NUM_THREADS=64 IX_COMPILE_WORKERS=64
lake exe ix compile Benchmarks/Compile/CompileAnthropicFLT.lean \
  --no-build --verbose --out anthropic-flt-cached.ixe
lake exe ix compile Benchmarks/Compile/CompileMathlib.lean \
  --no-build --verbose --out mathlib-cached.ixe

Optional diagnostics: IX_MEMORY_DIAG=1 and IX_LOG_IND_GROUPS=1.
Worker ceilings and memory-budget controls are documented in
Benchmarks/Compile/README.md.

Deferred

Whole-block cancellation/parking and more aggressive initial admission ramps
remain follow-up work. This PR does not introduce unsafe worker suspension,
active-block preemption, or an aggressive ramp based on the final FLT peak.