TruthMines: self-contained .ixc catalogs and corpus-scale compiler/kernel fixes by johnchandlerburnham · Pull Request #590 · argumentcomputer/ix

johnchandlerburnham · 2026-08-24T16:52:03Z

Summary

This PR replaces the old monolithic, name-qualified catalog pipeline with self-contained, content-addressed .ixc catalogs and adds TruthMines as the corpus-scale driver for building, validating, and kernel-checking them.

The resulting architecture compiles each library independently into an ordinary .ixe piece, commits their anonymous union in a compact manifest, and checks each piece in an isolated process. This avoids namespace collisions, keeps peak memory proportional to the largest member rather than the entire union, and makes catalog identity independent of storage partitioning.

Running this pipeline over Mathlib, TauCeti, CompPoly, TorchLean, PhiConfluence, and the Palomar corpus exposed several compiler and kernel issues. This PR includes the corresponding fixes:

General call-site adapters for partial recursor applications.
Correct .brecOn.go/.brecOn.eq call-site planning.
Bounded same-head congruence for CompPoly’s pathological Abbrev case.
Scalable structural WHNF for PrimeGaps certificate evaluation.
Definitive Rule-K rejection for TauCeti’s expensive equality transports.
A discoverable ix compile --verbose / -v flag.
Focused, source-contained regression fixtures for each failure class.

The native TruthMines catalog contains 78 members. A verified 19-member catalog from the standalone Palomar.ix repository can be composed into it, producing a 97-member catalog without importing Palomar’s source workspaces or compatibility patches into this repository.

Motivation

The previous ix catalog implementation loaded multiple Lean environments into one frontend process, qualified their names, replayed them into a combined environment, and wrote one monolithic .ixe.

That approach had several problems:

Peak memory tracked the full combined environment.
Libraries with reused namespaces or generic module names could not coexist naturally.
Catalog construction mixed compilation, qualification, replay, auditing, and artifact storage.
Long stages could die under memory pressure without flushed diagnostic output.
A machine-readable JSON report became a second representation of catalog identity.
Corpus-scale checking made it difficult to isolate one failing library or reproduce one constant.

Ixon constants are already content-addressed and alpha-invariant. Two pieces that contain the same address necessarily contain the same anonymous declaration, so their anonymous sections can coexist without qualification. This PR makes that property the catalog abstraction.

What changed

1. Self-contained `.ixc` catalogs

A catalog is now a directory containing a binary manifest and its member pieces:

corpus.ixc/
  manifest
  MemberA.ixe
  MemberB.ixe
  ...
  .cache/

The manifest commits two independent roots:

members_root: the canonical Merkle root of the member environment roots.
content_root: the canonical Merkle root of the union of all member constant addresses.

The union is computed by a streaming k-way traversal over the already-sorted constant sections. It is never materialized during catalog assembly or verification, and resident memory is proportional to the number of pieces.

The format supports:

A fat profile containing one self-contained .ixe per member.
A chunked profile whose chunks must form a disjoint partition.
Member labels, toolchains, source pins, topologically ordered dependencies, and optional preimage commitments.
Opaque preservation of future trailing manifest sections.
Catalog claims binding both roots.

The implementation is mirrored in:

crates/ixon/src/catalog.rs, the Rust source of truth.
Ix/Catalog.lean, the Lean wire-format mirror.
crates/ffi/src/catalog.rs, the CLI/Lean FFI layer.

The Lean and Rust implementations are tested for byte-identical serialization, root parity, identity deduplication, dependency preservation, and malformed-manifest rejection.

2. New catalog CLI

The old compilation-oriented ix catalog surface, including authored JSON specs and side report files, is replaced by artifact operations:

ix catalog assemble corpus.ixc A.ixe B.ixe \
  --labels A,B \
  --toolchains leanprover/lean4:v4.33.0 \
  --pins pin-a,pin-b \
  --deps '1:0'

ix catalog verify corpus.ixc
ix catalog verify corpus.ixc --deep
ix catalog info corpus.ixc

assemble ingests pieces by hard link when possible, with a copy fallback. It writes the manifest only after the complete catalog has been computed.

verify independently recomputes the roots and checks member roots, constant counts, storage sizes, dependency ordering, and the storage profile’s deduplication rules. --deep additionally rehashes every file and fully loads every piece.

For consumers that still need one anonymous .ixe, ix merge materializes a derived union:

ix merge merged.ixe --ixc corpus.ixc
ix merge subset.ixe --ixc corpus.ixc --only Mathlib,FLT

The .ixc directory remains the source of truth.

ix compile --anon is also available for strict anonymous output. It removes names, metadata, and commitments after finalizing anonymous reducibility hints, leaving the environment root unchanged.

3. TruthMines corpus driver

Benchmarks/TruthMinesSpec adds a typed registry, frozen admission spec, validation rules, and deterministic workspace projection.

The native full tier contains:

78 members.
565 declared roots.
Mathlib and its dependency spine.
Large downstream libraries including FLT, CompPoly, TauCeti, TorchLean, Carleson, and others.
Two relocation fixtures that intentionally declare colliding source names.

A 12-member mini tier provides a smaller end-to-end infrastructure gate containing the collision fixtures, Mathlib’s dependency spine, Mathlib, and FLT.

The generated workspace lives under Benchmarks/TruthMines/. Its Lake configuration, toolchain, member drivers, and lockfile pins are derived from or checked against the typed records.

The driver exposes:

lake exe truthmines gen
lake exe truthmines gen --check
lake exe truthmines spec
lake exe truthmines spec --mini

lake exe truthmines build
lake exe truthmines build --mini
lake exe truthmines check
lake exe truthmines check --only Mathlib,TauCeti
lake exe truthmines validate
lake exe truthmines validate --mini

A build:

Rejects stale generated workspace files.
Builds the member root .oleans.
Compiles each member directly into the .ixc directory in an isolated ix compile process.
Reuses pieces when the source-pin closure, toolchain, and Ix version match their cache key.
Assembles the manifest.
Independently verifies the completed catalog.

check reads member labels from the manifest and runs ix check-rs --anon over each piece. Rejections include the member log and a standalone reproduction command.

validate runs the eight-phase metadata-fidelity pipeline independently over each member’s driver closure.

4. External Palomar composition

The Palomar registry, isolated workspaces, and Lean 4.33 compatibility ports now live in the standalone Palomar.ix repository rather than under Benchmarks/Palomar.

A full TruthMines build can import its verified fat catalog:

cd ../Palomar.ix
nix develop --command lake exe palomar build

cd ../ix
lake exe truthmines build \
  --palomar-ixc ../Palomar.ix/palomar.ixc

The driver:

Verifies the external catalog before using it.
Rejects missing pieces, malformed manifests, chunked inputs, and label collisions.
Preserves member order, source pins, toolchains, and internal dependency edges.
Shifts imported dependency indices behind the 78 native members.
Hard-links the pieces into the final catalog.
Verifies the complete 97-member result.

truthmines check discovers these imported members directly from the final manifest, so commands such as the following work without any Palomar source checkout in the Ix workspace:

lake exe truthmines check \
  --only PalomarPrimeGaps,PalomarCardB

5. Typed memory watchdog

The shell-based watchdog has been replaced by Ix.Watchdog, shared by ix bench and TruthMines.

It runs subprocess trees under a systemd user scope with:

MemoryMax.
MemorySwapMax=0.
memory.oom.group=1.
Whole-process-tree accounting and termination.
Exit code 137 for a cgroup OOM kill.
An Open MPI signal-handler workaround used by proof workloads.
A fail-closed end-to-end availability probe.

TruthMines applies a per-member ceiling—25 GiB by default—to piece compilation and derives safe parallelism from the machine-level ceiling. Non-systemd environments must opt out explicitly with --no-watchdog.

6. Generalized compiler call-site adapters

Canonical reordering of mutual inductive blocks changes regenerated recursor telescopes. Every source reference to a plan-bearing recursor must therefore be adapted at its call site.

This PR extends that machinery to cover:

Fully applied recursors.
Partial applications missing only an identity suffix.
Arbitrarily short applications.
Bare recursor references used as function values.
Partial .below and .brecOn references.
Named-argument elaboration that splits a recursor spine across a lambda application.

Short applications receive a local eta adapter whose interface retains the source-order telescope while its body calls the canonical recursor with the required permutation. New additive EtaCallSite metadata reconstructs the exact original source expression during decompilation.

A fail-closed arity audit detects unsupported plan heads obscured by mdata or let nodes and names the owner, head, actual arity, and expected floor.

The first version of this audit traversed shared Lean expressions as expanded trees and caused several Mathlib proofs to run for more than 230 seconds. The final implementation deduplicates expression DAG nodes using (expression, obscured-context) as the key. A 40-level synthetic DAG pins the traversal to 41 visits instead of 2^40 paths.

The compiler also registers brecOn plans under .brecOn.go and .brecOn.eq, and the generated equality theorem now uses elaborator-strength definitional equality when selecting Eq versus HEq for its major premise.

7. Kernel fixes found by the corpus

CompPoly: bounded same-head congruence

BF128Ghash.gcd_start_reduction previously sent the kernel into a linear Nat.rec computation with exponent 2^64.

Content addressing had merged several alpha-identical binary-operation projections at one Abbrev address. Definitional equality unfolded that shared head before comparing its already-aligned arguments, exposing the impossible computation.

The fix keeps the existing unbounded same-head path for Regular definitions and gives Abbrev/Opaque heads a bounded speculative congruence attempt:

4,096 units of local recursive fuel per attempt.
No fresh speculation after 16,384 units have been consumed by the enclosing check.
Nested attempts inherit the remaining slice.
Failure or local exhaustion resumes the unchanged delta path.
The rejection cache records only “do not retry this speculation,” never a false definitional-equality result.

The exact theorem and full CompPoly environment now pass at the default production budget.

PrimeGaps: productive structural WHNF

The generated cert246Data.data_ok and cert246Data.enc_ok proofs need approximately 281,000 productive beta/zeta/iota transitions in one finite structural normalization.

The previous closure-machine-local 10,000-step guard reported this as “max recursion depth exceeded.” Productive structural transitions now charge the existing per-constant shared recursion budget instead. The pure-Lean kernel mirrors this by giving only the structural WHNF core a maxRecFuel-sized emergency ceiling; unrelated auxiliary loops retain their smaller bounds.

TauCeti: definitive Rule-K rejection

TauCeti’s Type-level Eq.rec reductions performed an expensive full-strength constructor-synthesis comparison, conclusively rejected it, and then fully normalized the same opaque equality proof as the recursor major.

K synthesis now has three outcomes:

synthesized
definitiveReject
inconclusive

A full-strength rejection returns the recursor application stuck immediately. Cheap-mode rejection remains inconclusive and retains the conservative fallback.

The Rust kernel, pure-Lean Ix.Tc, and the formal verification layer implement the same policy.

8. Focused regression fixtures

The previously external failures now have source-contained fixtures:

CheckCompPoly.lean
PrimeGapsReduction.lean and CheckPrimeGaps.lean
TauCetiReduction.lean and CheckTauCetiReduction.lean
The exact TauCeti focused environment suite
Expanded mutual-recursion and partial-call-site fixtures

The PrimeGaps fixture preserves the exact packed inputs and original theorem addresses in a 393-constant closure. The minimal TauCeti Rule-K fixture has a 51-constant closure. Neither depends on a Palomar checkout, Mathlib, or a prebuilt TruthMines artifact.

Validation

Catalog and TruthMines

lake build truthmines
lake exe truthmines gen --check
lake test -- truthmines-spec
- 5/5 record, toolchain, projection, lockfile, and argv coherence tests passed.
Standalone Palomar catalog verified:
- 19 members.
- 753,224 unique constants.
Full documented composition build completed:
- 14,762 Lake jobs.
- 78/78 native piece cache hits.
- 97 members after Palomar composition.
- 995,368 unique union constants.
- members_root = 76cca48fd37eaa9365a255e21fe322419a4f08a5cb22a1081e2390d6897946dc
- content_root = f89df2db01f81e43db0b7f3f3148731c333279c9829938ebaa4e30960f45bc1a
Mixed native/imported smoke sweep:
- Cli
- PalomarCardB
Full historically pathological pieces:
- TauCeti
- PalomarPrimeGaps

All four pieces were kernel-clean under the ordinary production limits.

Mathlib

Full Mathlib compilation:
- 771,129 requested constants.
- 761,006 scheduler blocks.
- Scheduler drained in 32.5 seconds.
- 60.818 seconds end to end.
- 3.0 GiB serialized environment.
Full anonymous Rust-kernel sweep:
- 672,981/672,981 checkable constants passed.
- 663,254 unique verification work items.
- 203.9 seconds kernel time / 206.1 seconds total.
- 6.4 GiB peak RSS.
- Default 10M production fuel, 32 workers.
- Zero streamed failures.

CompPoly and focused kernel gates

Exact CompPoly theorem:
- Rust: 19.6 ms.
- Pure Lean: 118 ms, depth 16.
Full Rust CompPoly sweep:
- 329,109 constants.
- 42.6 seconds kernel time.
- 2.61 GiB peak RSS.
PrimeGaps focused closure:
- Rust: 0.62 seconds.
- Pure Lean: 16.1 seconds.
Minimal TauCeti Rule-K fixture:
- Rust: 35 ms.
- Pure Lean: 720 ms.
Exact extracted TauCeti closures passed at approximately seven seconds per direction.
CompPoly remained clean during the 97-piece TruthMines sweep.

The optional full pure-Lean CompPoly timing run was stopped at 245,766/323,368 work items with zero failures; corpus-wide pure-Lean timing was not treated as a release criterion.

Compiler and formal verification

cargo test -p ix-compile: 235/235.
Rust kernel unit tests: 681/681.
lake test -- tc-unit.
Aux generation and decompilation differential gates.
Compiler determinism and call-site replay gates.
lake build IxTcVerify.
Completed-theorem trust audit: 1,797 roots.
Statement audit: 7 roots.
Clean sorryAx frontier.

Compatibility and operational notes

This is a breaking change to the old ix catalog CLI. Authored --spec JSON, qualified catalog compilation, and side report files are removed. Callers should compile pieces independently and use ix catalog assemble.
The old Benchmarks/Catalog, CatalogReal, and CatalogSpine workspaces and their qualified-loader tests are replaced by TruthMines and the network-free .ixc fixture suites.
The EtaCallSite metadata variant is additive; existing .ixe files remain readable.
TruthMines currently produces the fat storage profile. External Palomar composition therefore requires a fat catalog.
assemble and verify independently scan every member index. Rebuilding the 97-member, approximately 100 GiB catalog can spend several minutes in each phase even when all pieces are cached.
The watchdog requires a writable cgroup-v2 systemd user scope. Use --no-watchdog only when explicitly accepting an unenforced run.
truthmines check --jobs N currently controls piece-level concurrency, while each child kernel chooses its own worker count. For the largest TauCeti/PrimeGaps checks, --jobs 1 avoids host oversubscription. A single global worker budget and child-process RSS attribution remain follow-up harness work.
Palomar source ports remain outside this repository. This PR only consumes a verified palomar.ixc.

Reviewer guide

A useful review order is:

crates/ixon/src/catalog.rs, crates/ffi/src/catalog.rs, and Ix/Catalog.lean for the artifact model and Rust/Lean format parity.
Ix/Cli/CatalogCmd.lean, Ix/Cli/MergeCmd.lean, and the catalog tests for the user-facing algebra.
Benchmarks/TruthMinesSpec/*, Benchmarks/TruthMines/*, and Tests/Ix/TruthMines*.lean for corpus orchestration.
Ix/Watchdog.lean and its consumers for resource enforcement.
The compiler call-site changes in crates/compile, Ix/CompileM.lean, and the metadata/decompiler mirrors.
The DefEq/WHNF changes in crates/kernel and Ix/Tc, followed by their formal verification and focused fixtures.

johnchandlerburnham · 2026-08-24T17:34:49Z

!benchmark

johnchandlerburnham · 2026-08-24T17:34:56Z

!benchmark compile decompile

argument-ci-bot · 2026-08-24T17:38:50Z

`!benchmark` — main vs `cb52cc3`

backends: aiur=prove · envs: InitStd

`aiur` · `InitStd` · `prove` — main from: base run @ `7da4132` (not on bencher)

7 constants · 3 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

IxVM on FRI (7 constants)

constant	execute-time (main)	execute-time (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	8.790 s	8.814 s	+0.3%	29.885 s	29.970 s	+0.3%	92.860	92.590	-0.3%	70.74 GiB	70.75 GiB	+0.0%	11.33 MiB	11.33 MiB	+0.0%	68.8 ms	68.8 ms	-0.1%	134.35B	134.35B	+0.0%
`Char.ofOrdinal_le_of_le`	6.758 s	6.750 s	-0.1%	25.513 s	25.758 s	+1.0%	108.300	107.270	-1.0%	63.89 GiB	63.87 GiB	-0.0%	11.33 MiB	11.33 MiB	+0.0%	67.8 ms	75.1 ms	+10.7% (1.11× slower) ⚠️	102.60B	102.60B	+0.0%
`Array.extract_append`	6.378 s	6.620 s	+3.8% ⚠️	22.617 s	22.800 s	+0.8%	71.010	70.440	-0.8%	51.94 GiB	51.96 GiB	+0.0%	11.24 MiB	11.24 MiB	+0.0%	70.3 ms	70.2 ms	-0.2%	97.08B	97.08B	+0.0%
`Std.HashMap`	3.954 s	3.999 s	+1.2%	15.578 s	15.626 s	+0.3%	131.090	130.680	-0.3%	36.33 GiB	36.30 GiB	-0.1%	11.26 MiB	11.26 MiB	+0.0%	79.1 ms	77.2 ms	-2.3%	61.88B	61.88B	+0.0%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	3.521 s	3.520 s	-0.0%	14.209 s	14.336 s	+0.9%	131.400	130.230	-0.9%	33.93 GiB	33.97 GiB	+0.1%	11.26 MiB	11.26 MiB	+0.0%	69.9 ms	70.6 ms	+1.0%	55.68B	55.68B	+0.0%
`String.append`	423.9 ms	426.0 ms	+0.5%	2.268 s	2.267 s	-0.0%	144.190	144.220	+0.0%	4.96 GiB	4.92 GiB	-0.8%	9.94 MiB	9.94 MiB	+0.0%	62.5 ms	63.6 ms	+1.8%	3.37B	3.37B	+0.0%
`Nat.add_comm`	261.1 ms	263.7 ms	+1.0%	1.028 s	1.075 s	+4.6% ⚠️	44.770	42.810	-4.4% ⚠️	4.62 GiB	4.84 GiB	+4.7% ⚠️	9.09 MiB	9.09 MiB	+0.0%	53.8 ms	53.7 ms	-0.2%	308.40M	308.40M	+0.0%

FRI verifier on FRI (7 constants)

constant	execute-time (main)	execute-time (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	5.471 s	5.463 s	-0.1%	31.232 s	31.302 s	+0.2%	88.850	88.650	-0.2%	100.16 GiB	100.13 GiB	-0.0%	3.97 MiB	3.97 MiB	+0.0%	29.5 ms	29.1 ms	-1.2%	210.23B	210.23B	+0.0%
`Char.ofOrdinal_le_of_le`	5.447 s	5.315 s	-2.4%	30.744 s	31.143 s	+1.3%	89.870	88.720	-1.3%	99.07 GiB	99.17 GiB	+0.1%	3.97 MiB	3.97 MiB	+0.0%	24.7 ms	24.8 ms	+0.4%	207.18B	207.18B	+0.0%
`Array.extract_append`	5.218 s	5.205 s	-0.2%	29.582 s	29.665 s	+0.3%	54.290	54.140	-0.3%	94.67 GiB	94.20 GiB	-0.5%	3.97 MiB	3.97 MiB	+0.0%	24.8 ms	24.5 ms	-1.2%	200.65B	200.65B	+0.0%
`Std.HashMap`	5.343 s	5.252 s	-1.7%	29.620 s	29.812 s	+0.6%	68.940	68.500	-0.6%	94.24 GiB	94.23 GiB	-0.0%	3.97 MiB	3.97 MiB	+0.0%	24.8 ms	24.6 ms	-0.7%	203.35B	203.35B	+0.0%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	5.316 s	5.340 s	+0.4%	30.899 s	31.078 s	+0.6%	60.420	60.080	-0.6%	98.48 GiB	98.97 GiB	+0.5%	3.97 MiB	3.97 MiB	+0.0%	29.7 ms	27.1 ms	-8.8% (1.10× faster) 🟢	205.59B	205.59B	+0.0%
`String.append`	4.386 s	4.400 s	+0.3%	27.399 s	27.364 s	-0.1%	11.930	11.950	+0.2%	87.81 GiB	87.82 GiB	+0.0%	3.97 MiB	3.97 MiB	+0.0%	24.6 ms	24.6 ms	-0.2%	168.67B	168.67B	+0.0%
`Nat.add_comm`	3.512 s	3.546 s	+1.0%	18.449 s	18.458 s	+0.0%	2.490	2.490	+0.0%	58.62 GiB	58.60 GiB	-0.0%	3.97 MiB	3.97 MiB	+0.0%	24.3 ms	24.4 ms	+0.6%	130.84B	130.84B	+0.0%

Pipeline total (7 constants)

constant	total-time (main)	total-time (PR)	Δ%	pipeline-throughput (const/s) (main)	pipeline-throughput (const/s) (PR)	Δ%	pipeline-peak-ram (main)	pipeline-peak-ram (PR)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	1m 1.1s	1m 1.3s	+0.3%	45.400	45.290	-0.2%	100.16 GiB	100.13 GiB	-0.0%
`Char.ofOrdinal_le_of_le`	56.257 s	56.900 s	+1.1%	49.110	48.560	-1.1%	99.07 GiB	99.17 GiB	+0.1%
`Array.extract_append`	52.199 s	52.466 s	+0.5%	30.770	30.610	-0.5%	94.67 GiB	94.20 GiB	-0.5%
`Std.HashMap`	45.198 s	45.438 s	+0.5%	45.180	44.940	-0.5%	94.24 GiB	94.23 GiB	-0.0%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	45.108 s	45.414 s	+0.7%	41.390	41.110	-0.7%	98.48 GiB	98.97 GiB	+0.5%
`String.append`	29.667 s	29.631 s	-0.1%	11.020	11.040	+0.2%	87.81 GiB	87.82 GiB	+0.0%
`Nat.add_comm`	19.477 s	19.533 s	+0.3%	2.360	2.360	+0.0%	58.62 GiB	58.60 GiB	-0.0%

Workflow logs

argument-ci-bot · 2026-08-24T17:39:55Z

`!benchmark` — main vs `cb52cc3`

backends: compile decompile · envs: InitStd,Lean,ISLB,Mathlib,FLT

Warning

CPU model mismatch for PR benchmark binaries in this job: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.
CPU model mismatch for PR benchmark binaries during compile: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.

`compile` · `FLT` — main from: base run @ `7da4132` (not on bencher)

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

env	compile-time (main)	compile-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	env-size (main)	env-size (PR)	Δ%	constants (main)	constants (PR)	Δ%
`FLT`	52.523 s	48.436 s	-7.8% (1.08× faster) 🟢	14.87K	16.12K	+8.4% (1.08× faster) 🟢	19.87 GiB	19.56 GiB	-1.6%	3.20 GiB	3.20 GiB	+0.0%	780,906	780,906	+0.0%

Warning

CPU model mismatch for PR benchmark binaries in this job: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.
CPU model mismatch for PR benchmark binaries during compile: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.

`compile` · `ISLB` — main from: base run @ `7da4132` (not on bencher)

1 env · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

env	compile-time (main)	compile-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	env-size (main)	env-size (PR)	Δ%	constants (main)	constants (PR)	Δ%
`ISLB`	8.100 s	9.317 s	+15.0% (1.15× slower) ⚠️	26.76K	23.27K	-13.1% (1.15× slower) ⚠️	5.48 GiB	5.40 GiB	-1.4%	512.40 MiB	512.40 MiB	+0.0%	216,785	216,785	+0.0%

Warning

CPU model mismatch for PR benchmark binaries in this job: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.
CPU model mismatch for PR benchmark binaries during compile: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.

`compile` · `InitStd` — main from: base run @ `7da4132` (not on bencher)

1 env · 1 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

env	compile-time (main)	compile-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	env-size (main)	env-size (PR)	Δ%	constants (main)	constants (PR)	Δ%
`InitStd`	4.579 s	5.009 s	+9.4% (1.09× slower) ⚠️	25.57K	23.37K	-8.6% (1.09× slower) ⚠️	3.96 GiB	3.80 GiB	-4.2% 🟢	324.65 MiB	324.65 MiB	+0.0%	117,084	117,084	+0.0%

Warning

CPU model mismatch for PR benchmark binaries in this job: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.
CPU model mismatch for PR benchmark binaries during compile: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.

`compile` · `Lean` — main from: base run @ `7da4132` (not on bencher)

1 env · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

env	compile-time (main)	compile-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	env-size (main)	env-size (PR)	Δ%	constants (main)	constants (PR)	Δ%
`Lean`	8.256 s	9.668 s	+17.1% (1.17× slower) ⚠️	25.03K	21.37K	-14.6% (1.17× slower) ⚠️	5.34 GiB	5.25 GiB	-1.7%	481.18 MiB	481.18 MiB	+0.0%	206,647	206,647	+0.0%

Warning

CPU model mismatch for PR benchmark binaries in this job: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.
CPU model mismatch for PR benchmark binaries during compile: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.

`compile` · `Mathlib` — main from: base run @ `7da4132` (not on bencher)

1 env · 1 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

env	compile-time (main)	compile-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	env-size (main)	env-size (PR)	Δ%	constants (main)	constants (PR)	Δ%
`Mathlib`	51.860 s	45.469 s	-12.3% (1.14× faster) 🟢	14.87K	16.96K	+14.1% (1.14× faster) 🟢	19.30 GiB	20.18 GiB	+4.6% ⚠️	3.10 GiB	3.10 GiB	+0.0%	771,129	771,129	+0.0%

Warning

CPU model mismatch for PR benchmark binaries in this job: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.

`decompile` · `FLT` — main from: base run @ `7da4132` (not on bencher)

1 constant · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

constant	decompile-time (main)	decompile-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	env-size (main)	env-size (PR)	Δ%	constants (main)	constants (PR)	Δ%
`FLT`	1m 46.5s	1m 47.7s	+1.2%	7.33K	7.25K	-1.2%	32.21 GiB	32.17 GiB	-0.1%	3.20 GiB	3.20 GiB	+0.0%	780,906	780,906	+0.0%

Warning

CPU model mismatch for PR benchmark binaries in this job: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.

`decompile` · `InitStd` — main from: base run @ `7da4132` (not on bencher)

1 constant · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

constant	decompile-time (main)	decompile-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	env-size (main)	env-size (PR)	Δ%	constants (main)	constants (PR)	Δ%
`InitStd`	3.472 s	3.461 s	-0.3%	33.72K	33.83K	+0.3%	3.67 GiB	3.64 GiB	-0.8%	324.65 MiB	324.65 MiB	+0.0%	117,084	117,084	+0.0%

Warning

CPU model mismatch for PR benchmark binaries in this job: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.

`decompile` · `Lean` — main from: base run @ `7da4132` (not on bencher)

1 constant · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

constant	decompile-time (main)	decompile-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	env-size (main)	env-size (PR)	Δ%	constants (main)	constants (PR)	Δ%
`Lean`	7.715 s	7.675 s	-0.5%	26.79K	26.92K	+0.5%	4.77 GiB	4.78 GiB	+0.3%	481.18 MiB	481.18 MiB	+0.0%	206,647	206,647	+0.0%

Warning

CPU model mismatch for PR benchmark binaries in this job: built on Intel(R) Xeon(R) 6975P-C; measured on AMD EPYC 9R45. Native Rust code uses -Ctarget-cpu=native.

`decompile` · `Mathlib` — main from: base run @ `7da4132` (not on bencher)

1 constant · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

constant	decompile-time (main)	decompile-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	env-size (main)	env-size (PR)	Δ%	constants (main)	constants (PR)	Δ%
`Mathlib`	1m 36.1s	1m 35.4s	-0.7%	8.02K	8.08K	+0.7%	30.93 GiB	30.95 GiB	+0.1%	3.10 GiB	3.10 GiB	+0.0%	771,129	771,129	+0.0%

Workflow logs

Port the TruthMines repo's typed corpus into Benchmarks (consolidation plan Phase 0.1-0.2; TruthMines-the-repo is deprecated in its favor): - Benchmarks/TruthMinesSpec: PackageSpec records (125: 77 admitted, 44 growth candidates, 4 excluded), ported verbatim with the probe-evidence machinery collapsed into a frozen admission spec — membership in the generated 77-member/79-root Spec.lean IS admission. expectedToolchain is derived from Lean.versionString (one toolchain by construction; the external-CLI version handshake dissolves). Fail-closed validation runs as an elaboration-time run_cmd gate, extended with admission-spec coherence: unknown/excluded qualifiers, non-admitted dependencies, and provider-after-consumer ordering all fail the build. - lake exe truthmines: gen [--check] projects the nested workspace (lakefile.lean requires block + catalogOleans olean-fetch default target + lean-toolchain) byte-idempotently from the records; spec prints the ix catalog --spec JSON (rendered at invocation time, never checked in); build = gen-check, member root oleans (lake exe cache get tolerated), then ix catalog over the rendered spec — one command, one truthmines.ixe, the compilemathlib.ixe of the corpus tier. - Benchmarks/TruthMines: the generated workspace; lake-manifest.json is ported from TruthMines (Lake's lockfile, maintained by Lake) with the fixture paths repointed at Benchmarks/Catalog/RelocFixture{A,B}. - lake test -- truthmines-spec (primary suite): validation clean, the toolchain triple agrees, projections byte-identical, lockfile pins match the records name-for-name (guillemet-normalized) with no direct entry outside the admitted set, and the rendered spec round-trips through Ix.Catalog.specFromJson member-for-member.

--close-roots absorbs the fix behind the I5 diagnostic from TruthMines (TruthMinesBuild/Workspace.lean closeCrossPackageImports, reduced to kernel-catalog needs): extend every member's declared roots to the global cross-package source-import fixed point through the cwd's Lake workspace — a provider module some member imports that the provider's own roots do not reach becomes additional provider coverage — then re-root each member at its terminal modules. Ix.Catalog.Lake is spec-driven (qualifier + roots resolve the member's package; no typed records needed) and source-level only: Lake is the authority for module providers, Lean's header parser for import edges, and nothing imports an environment. Fail-closed on unresolved imports, imports from outside the cataloged members, ambiguous providers, cross-member module collisions, and roots spanning packages. The I5 coverage gate in the loader stays as the backstop; the resolved roots are echoed into --report. Requires a lake-provided process env (LAKE/LEAN) to locate the installation — lake exe/lake env callers have it. --copy-stage-max-owned exposes the copy-vs-share staging threshold (default 100000; threshold-0 and default builds are byte-identical) and echoes it into --report; report schemaVersion bumps to 2 for the new field (no consumer asserts the old value). Gates: catalog-fixtures grows a close-roots regression — the exact narrowed spec the I5 test proves fail-closed builds clean after closeRoots re-roots B at [FixtureB.Base, FixtureB.Model]; suite green end to end (workspace-load-first ordering matters: Lake config elaboration resets the process search path, so imports re-init after it, matching the CLI's phase order). lake build ix green. Manual smoke on Benchmarks/Catalog: control run fails with the named I5 error; --close-roots run augments 2 declared → 3 terminal roots and builds.

The corpus tier (plan Phase 0.4), two chained ignored suites so build and typecheck gate independently: - truthmines: run .lake/build/bin/truthmines build with its default repo-root outputs (truthmines.ixe / truthmines.report.json, both gitignored — the compilemathlib.ixe convention, and what lets the check leg and local iteration reuse the artifact), then assert the report: written fail-closed, zero ungrounded, all 77 members, a positive replay count, peak RSS measured (hard fail without the Linux sampler, like the spine gate) and under a 96 GiB safety ceiling — to be tightened once the first green run records baselines. - truthmines-check: ix check-rs over the artifact the build leg left, IX_MAX_REC_FUEL=10^9 (the spine run's BET fuel finding). The driver invokes ix WITHOUT --close-roots: the frozen admission spec already carries closed roots; closure recomputation belongs to spec regeneration (Phase 1), not to every build.

The SDL member's include-flag detection produces garbage (-I/SDL2, an empty -I) under nix's sdl2-compat even with SDL2.dev's sdl2-config on PATH and its package config cache invalidated, so its C shim cannot compile in the ix dev environment — the one failure in an otherwise green 12,596-target first corpus workspace build (Curl's ldd-based detection works fine). The record stays as a candidate with the demotion note; re-admission is restoring its spec entry once the environment satisfies its lakefile. Also repoint the two ported lockfile fixture entries at lakefile.toml (ix's Benchmarks/Catalog fixtures are TOML; TruthMines' were lakefile.lean).

The first corpus run OOM'd the whole box during the ix catalog leg — the driver ran it unwatched, violating the bench principle the repo already institutionalized ('an unenforced ceiling is not a benchmark run'). truthmines build now wraps the workspace build and the ix catalog invocation in a systemd user scope by default: cgroup MemoryMax, swap off, memory.oom.group=1 so a breach kills the whole scope (exit 137, reported with guidance). The invocation is INLINED in the driver with .github/scripts/watchdog.sh (the ix bench watchdog) kept as the shared spec, not a runtime dependency — a lake exe should not depend on CI scripts; omissions vs the script (CI linger bootstrap, the zisk-specific Open MPI signal workaround) are recorded at the definition. Default ceiling is total RAM − 15 GiB (bench convention, from /proc/meminfo); --ceiling-gb N overrides, --no-watchdog opts out explicitly (non-systemd platforms, or when RAM cannot be determined). Verified: a deliberate --ceiling-gb 1 run dies with a clean cgroup OOM kill and the named diagnostic; the box stays untouched.

Every lake exe must be standalone — no runtime dependencies on CI scripts. The RAM watchdog is now a typed IO module (Ix/Watchdog.lean) carrying the script's full semantics and hard-won commentary: systemd user scope with cgroup MemoryMax and MemorySwapMax=0 (kernel SIGKILL at the cap, exit 137 = oomExitCode, whole-tree charging, no sampler race), memory.oom.group=1 set inside the scope with fail-closed exit 2, the Open MPI signal-handler opt-out (zisk-host wedge), best-effort CI linger bootstrap, and an XDG_RUNTIME_DIR default for headless shells. defaultCeilingGb (RAM − 15 GiB, floor 8, fallback 16) moves here as the one rule for every consumer; Ix.Watchdog.available probes the whole path end to end. ix bench run: runGuarded takes a Bool instead of a script path; the script-existence refusal becomes an availability-probe refusal (same 'no watchdog, no run' semantics); the --watchdog path-override flag is retired. lake exe truthmines: the previously inlined systemd-run invocation collapses to Ix.Watchdog.run, and the driver's own /proc/meminfo duplicate dissolves into the shared defaultCeilingGb + availability probe. .github/scripts/watchdog.sh is deleted; docs updated. Verified: --ceiling-gb 1 still dies with the clean cgroup whole-scope kill and diagnostic.

A small spec for testing the catalog infrastructure end to end (12 members): the RelocFixture collision pair (qualified imports must coexist), Batteries and the rest of mathlib's dependency spine, Mathlib, and FLT (new record, pinned at its v4.33.0 release tag — the rev Benchmarks/Compile benches, whose mathlib pin is byte-identical to the corpus spine's). Init/Std/Lean enter as the shared unqualified toolchain base by contract — toolchain modules cannot be cataloged as members. Policy, validated at elaboration: mini ⊆ full — FLT joins the full admission spec too (77 members again). - Spec.lean: catalogMiniSpec; FLT in the full spec (generator- conventional position). Validation: specCoherenceErrors generalized over every checked-in spec + the mini-subset rule. - Projection: workspacePackages = union of spec member sets in dependency order; the generated lakefile carries root lists and olean-fetch targets for both tiers (catalogOleans default, catalogMiniOleans). - Driver: build --mini / spec --mini (defaults truthmines-mini.ixe / .report.json; builds only the mini roots); same watchdog. - lake-manifest.json: FLT entry added by hand (Lake's lockfile). - Suites: --ignored truthmines-mini chains a driver build with --audit-only A,B (the fixture audit proves the anon-address invariant through the driver end to end) and ix check-rs over the mini artifact; the fast truthmines-spec suite now pin-checks the union and round-trips both specs through Ix.Catalog.specFromJson.

The driver now renders the typed records straight to ix catalog's positional Qualifier=Root[,Root…] argument vector (--prefix + members), the TruthMines-original design: no spec file, no JSON, the typed record is the only representation end to end. The two invocation forms are byte-equivalent per #584's I3 gate, so artifacts are unchanged. The spec verb prints the vector; the fast suite's JSON round-trip check becomes a well-formedness check over the rendered argv for both tiers (the end-to-end contract is covered by the truthmines-mini suite driving the real CLI). ix's --spec file form remains as landed CLI surface (CatalogSpine uses it); nothing in the corpus path writes one. --report stays as ix's machine-readable output schema, consumed never authored.

--spec is gone: the typed CatalogSpec and the positional Qualifier=Root[,Root…] vector are the only representations (specFromJson deleted; the Item 2 grouped-loading reservation moves to the CatalogSpec docstring — the typed spec and CLI surface are where groups will land, there is no file format to reserve keys in). CatalogSpine's legs go positional; the --spec parse unit test retires with the parser; the report drops specFile (still schemaVersion 2 — one coherent schema change against main). Progress: buildCatalog/forEachLib gain a progress flag (CLI on, in-process callers default off) that narrates the long silent phases with FLUSHED lines — per-member 'importing → staged (copy/share, owned count)', the toolchain-base import, and per-member replay cumulative counts; the CLI brackets the final compile. Lean stdout block-buffers under redirection, so unflushed lines were being lost to watchdog kills — both OOM'd runs died with their catalog output trapped in the buffer. The truthmines driver gains flushed stage banners (1/3 oleans, 2/3 ix catalog, 3/3 done) with the ceiling stated up front.

Every streaming progress line now carries ' · rss X.Y GiB (hwm Z.W)' from /proc/self/status (the catalog is single-process, so VmRSS is the build's footprint). Motivation: the mini tier's FLT member import breached an 80 GiB ceiling where the spine leg — three sequential dependent imports of the same mathlib-scale shape — peaked at 35.3 GiB total; the kill line alone cannot say where the memory went, the per-line trajectory can.

Kernel-checking the TorchLean corpus member surfaced two aux_gen bugs on the NN.GraphSpec.DAG mutual Term/Args family: * Call-site surgery: derived BRecOnCallSitePlans now also register under `X.brecOn.go` and `X.brecOn.eq` (same telescope as `X.brecOn`). Lean's auto-generated equation lemmas (`f.eq_def`) reference both directly with explicit motive arguments, so any block whose canonical class order differs from Lean's source order shipped source-order motives against the canonical-order regenerated `.go`/`.eq` — AppTypeMismatch on nine `NN.GraphSpec.DAG.*.eq_def`s (Lean's own kernel accepts all nine; verified by addDeclCore replay). Applied to all three plan-install copies: compile.rs, decompile.rs, and the Lean pipeline (CompileAux.lean, DecompileDriver.lean). Fixture: Tests/Ix/Compile/Mutual.lean `TypeBrecOnEqDef`, declared in both source orders so one twin always disagrees with the canonical order. * .brecOn.eq generation: the Eq-vs-HEq binder decision now runs at elaborator defeq strength (meta_defeq/metaDefeq = kernel def-eq + isDefEqUnitLike + app congruence), and the MAJOR premise takes the same decision instead of hard-coded HEq. Unit-like-indexed families (index types with a single 0-field ctor) now match Lean's homogeneous `Eq` at the outer major type — generically ill-typed inside the motive but valid under infer-only proof checking — discharged by Eq.refl and consumed by plain Eq.ndrec in the minors. Fixture: `TypeBrecOnEqDefUnit`, incl. a concrete `.mk` return index. Gates: validate-aux 0 failures; aux-gen-diff and decompile-diff all gates PASS (patches byte-parity 1879 compared; Pass-2 plan parity); kernel-check-env 219794/219794; kernel-check-const 45/45; cargo test -p ix-compile 235/235. `ix check-rs` over the recompiled TorchLean member: 513781/513781 (was 9 failures). Also here: TruthMines corpus consolidation in-flight work — per-member driver modules under Benchmarks/TruthMines/Drivers/, retired Benchmarks/Catalog* trees, Benchmarks/Compile updates, .ixc gitignore, merge-tests suite wiring.

Benchmarks.PalomarSpec snapshots the live Palomar Registry (19 current projects, refreshed 2026-08-22) as typed records, with a `palomar` driver (gen/spec/build/check/validate) projecting one isolated wrapper workspace per entry over a shared Mathlib compatibility spine — submissions reuse generic Challenge/Solution module names, so pieces compose anonymously instead of co-loading. The TruthMines admission spec extends to 97 members: TauCeti (maximal-root import cover of its 1,819 modules, plus the Compile-workspace pin and TruthMines driver) and the 19 Palomar entries at the piece layer. Ignored suites: palomar, palomar-check, palomar-validate; palomar-spec joins the primary set.

TauCeti analogue of CheckEnv.focusConsts: seed rsCheckIxonFFI on tauceti.ixe with known slow/failing constants — the same subject-only seeded path as `ix check-rs tauceti.ixe --consts …`, narrowable via IX_KERNEL_FOCUS_CONST. Carries the 2026-08-22 sweep residue: chebyshevWeightL2Isometry_apply/_symm_apply exhaust the 10M recursive-fuel default but pass at 20M (true cost in (10M, 20M], not divergence) — the embedded rfl unfolds the composed isometry, and castLpₗᵢ is an Eq.rec-in-Type transport over a propositional measure equality, forcing a failing K-synthesis def-eq plus Lp instance-tower unfolding. Three slow-pass canaries (winding number, grid-diagram swap-equiv pair) ride along. Optimization work items in plans/kernel-rec-fuel.md.

arthurpaulino

LGTM
The IxVM will likely need to be patched to succeed on all these envs.

arthurpaulino · 2026-08-24T18:36:04Z

!benchmark aiur-sharded-env

argument-ci-bot · 2026-08-24T18:39:52Z

`!benchmark` — main vs `a647e7d`

backends: aiur-sharded-env · envs: ISLB

`aiur-sharded-env` · `ISLB` — main from: base run @ `e47a1b7` (not on bencher)

1 constant · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

constant	check-time (main)	check-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	constants (main)	constants (PR)	Δ%	shards (main)	shards (PR)	Δ%
`ISLB`	1m 22.2s	1m 26.0s	+4.6% ⚠️	2.23K	2.13K	-4.4% ⚠️	94.41 GiB	94.61 GiB	+0.2%	183,062	183,062	+0.0%	151	151	+0.0%

Workflow logs

johnchandlerburnham force-pushed the jcb/truth-mines branch from 76508be to cb52cc3 Compare August 24, 2026 17:19

johnchandlerburnham added 19 commits August 24, 2026 14:09

compile: generalize call-site adapters for partial applications

d2b05dd

cli: add verbose flag to compile

39774b9

bench: extract Palomar compatibility corpus

5189acb

kernel: optimize PrimeGaps and TauCeti reductions

a635c3e

truthmines: compose standalone Palomar catalog

5b937a3

ci: fix Rust formatting and lifetime lint failures

803c780

arthurpaulino previously approved these changes Aug 24, 2026

View reviewed changes

chore: regenerate TruthMines for Lean v4.33.1

a647e7d

johnchandlerburnham dismissed arthurpaulino’s stale review via a647e7d August 24, 2026 18:19

johnchandlerburnham force-pushed the jcb/truth-mines branch from cb52cc3 to a647e7d Compare August 24, 2026 18:19

arthurpaulino previously approved these changes Aug 24, 2026

View reviewed changes

johnchandlerburnham added this pull request to the merge queue Aug 24, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 24, 2026

johnchandlerburnham added this pull request to the merge queue Aug 24, 2026

johnchandlerburnham removed this pull request from the merge queue due to a manual request Aug 24, 2026

ci: rebuild ix before merge subprocess tests

9bef19c

johnchandlerburnham dismissed arthurpaulino’s stale review via 9bef19c August 24, 2026 22:09

Merge branch 'main' into jcb/truth-mines

f24fa03

johnchandlerburnham enabled auto-merge August 24, 2026 22:10

arthurpaulino previously approved these changes Aug 24, 2026

View reviewed changes

johnchandlerburnham added this pull request to the merge queue Aug 24, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 25, 2026

johnchandlerburnham added this pull request to the merge queue Aug 25, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 25, 2026

test: make CLI-backed suites self-contained

2523885

johnchandlerburnham dismissed arthurpaulino’s stale review via 2523885 August 25, 2026 09:53

Merge branch 'main' into jcb/truth-mines

11176b8

johnchandlerburnham enabled auto-merge August 25, 2026 10:13

arthurpaulino approved these changes Aug 25, 2026

View reviewed changes

johnchandlerburnham added this pull request to the merge queue Aug 25, 2026

Merged via the queue into main with commit 0f34977 Aug 25, 2026
13 checks passed

johnchandlerburnham deleted the jcb/truth-mines branch August 25, 2026 11:03

Navigation Menu

Uh oh!

TruthMines: self-contained .ixc catalogs and corpus-scale compiler/kernel fixes - #590

TruthMines: self-contained .ixc catalogs and corpus-scale compiler/kernel fixes#590
johnchandlerburnham merged 24 commits into
mainfrom
jcb/truth-mines

johnchandlerburnham commented Aug 24, 2026 •

edited

Loading

Uh oh!

johnchandlerburnham commented Aug 24, 2026

Uh oh!

johnchandlerburnham commented Aug 24, 2026

Uh oh!

argument-ci-bot Bot commented Aug 24, 2026 •

edited

Loading

Uh oh!

argument-ci-bot Bot commented Aug 24, 2026 •

edited

Loading

Uh oh!

arthurpaulino left a comment

Uh oh!

arthurpaulino commented Aug 24, 2026

Uh oh!

argument-ci-bot Bot commented Aug 24, 2026 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

johnchandlerburnham commented Aug 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Motivation

What changed

1. Self-contained .ixc catalogs

2. New catalog CLI

3. TruthMines corpus driver

4. External Palomar composition

5. Typed memory watchdog

6. Generalized compiler call-site adapters

7. Kernel fixes found by the corpus

CompPoly: bounded same-head congruence

PrimeGaps: productive structural WHNF

TauCeti: definitive Rule-K rejection

8. Focused regression fixtures

Validation

Catalog and TruthMines

Mathlib

CompPoly and focused kernel gates

Compiler and formal verification

Compatibility and operational notes

Reviewer guide

Uh oh!

johnchandlerburnham commented Aug 24, 2026

Uh oh!

johnchandlerburnham commented Aug 24, 2026

Uh oh!

argument-ci-bot Bot commented Aug 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

!benchmark — main vs cb52cc3

aiur · InitStd · prove — main from: base run @ 7da4132 (not on bencher)

Uh oh!

argument-ci-bot Bot commented Aug 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

!benchmark — main vs cb52cc3

compile · FLT — main from: base run @ 7da4132 (not on bencher)

compile · ISLB — main from: base run @ 7da4132 (not on bencher)

compile · InitStd — main from: base run @ 7da4132 (not on bencher)

compile · Lean — main from: base run @ 7da4132 (not on bencher)

compile · Mathlib — main from: base run @ 7da4132 (not on bencher)

decompile · FLT — main from: base run @ 7da4132 (not on bencher)

decompile · InitStd — main from: base run @ 7da4132 (not on bencher)

decompile · Lean — main from: base run @ 7da4132 (not on bencher)

decompile · Mathlib — main from: base run @ 7da4132 (not on bencher)

Uh oh!

arthurpaulino left a comment

Choose a reason for hiding this comment

Uh oh!

arthurpaulino commented Aug 24, 2026

Uh oh!

argument-ci-bot Bot commented Aug 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

!benchmark — main vs a647e7d

aiur-sharded-env · ISLB — main from: base run @ e47a1b7 (not on bencher)

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

johnchandlerburnham commented Aug 24, 2026 •

edited

Loading

1. Self-contained `.ixc` catalogs

argument-ci-bot Bot commented Aug 24, 2026 •

edited

Loading

`!benchmark` — main vs `cb52cc3`

`aiur` · `InitStd` · `prove` — main from: base run @ `7da4132` (not on bencher)

argument-ci-bot Bot commented Aug 24, 2026 •

edited

Loading

`!benchmark` — main vs `cb52cc3`

`compile` · `FLT` — main from: base run @ `7da4132` (not on bencher)

`compile` · `ISLB` — main from: base run @ `7da4132` (not on bencher)

`compile` · `InitStd` — main from: base run @ `7da4132` (not on bencher)

`compile` · `Lean` — main from: base run @ `7da4132` (not on bencher)

`compile` · `Mathlib` — main from: base run @ `7da4132` (not on bencher)

`decompile` · `FLT` — main from: base run @ `7da4132` (not on bencher)

`decompile` · `InitStd` — main from: base run @ `7da4132` (not on bencher)

`decompile` · `Lean` — main from: base run @ `7da4132` (not on bencher)

`decompile` · `Mathlib` — main from: base run @ `7da4132` (not on bencher)

argument-ci-bot Bot commented Aug 24, 2026 •

edited

Loading

`!benchmark` — main vs `a647e7d`

`aiur-sharded-env` · `ISLB` — main from: base run @ `e47a1b7` (not on bencher)