From 697fd8c1f34d085e2d1e2124a71b8588d5ceb855 Mon Sep 17 00:00:00 2001 From: "John C. Burnham" Date: Tue, 25 Aug 2026 08:06:22 -0400 Subject: [PATCH] TruthMines: validate constituent libraries independently --- Benchmarks/Compile/README.md | 13 + Benchmarks/Compile/TruthMines/Members/A.lean | 2 + .../Compile/TruthMines/Members/AddCombi.lean | 2 + .../Compile/TruthMines/Members/Aesop.lean | 2 + .../TruthMines/Members/Apportionmentlib.lean | 2 + Benchmarks/Compile/TruthMines/Members/B.lean | 2 + .../Compile/TruthMines/Members/BET.lean | 2 + .../Compile/TruthMines/Members/Base64.lean | 2 + .../Compile/TruthMines/Members/Batteries.lean | 2 + .../TruthMines/Members/BibtexQuery.lean | 2 + .../Compile/TruthMines/Members/Bignum.lean | 2 + .../Compile/TruthMines/Members/Binary.lean | 2 + .../Compile/TruthMines/Members/CamCombi.lean | 2 + .../Compile/TruthMines/Members/Carleson.lean | 2 + .../Compile/TruthMines/Members/Cli.lean | 2 + .../Members/CombinatorialGames.lean | 2 + .../Compile/TruthMines/Members/CompPoly.lean | 2 + .../Compile/TruthMines/Members/Cslib.lean | 2 + .../Compile/TruthMines/Members/Curl.lean | 2 + .../Members/DescriptiveComplexity.lean | 2 + .../Compile/TruthMines/Members/DocGen4.lean | 2 + .../TruthMines/Members/DomainTheory.lean | 2 + .../Compile/TruthMines/Members/Export.lean | 2 + .../Compile/TruthMines/Members/FLT.lean | 2 + .../Compile/TruthMines/Members/Fad.lean | 2 + .../Compile/TruthMines/Members/Flow.lean | 2 + .../TruthMines/Members/GibbsMeasure.lean | 2 + .../TruthMines/Members/HaskellSpec.lean | 2 + .../Compile/TruthMines/Members/I18n.lean | 2 + .../TruthMines/Members/Illuminate.lean | 2 + .../Compile/TruthMines/Members/ImpLab.lean | 2 + .../TruthMines/Members/ImportGraph.lean | 2 + .../Members/KolmogorovExtension4.lean | 2 + .../Compile/TruthMines/Members/LSpec.lean | 2 + .../Compile/TruthMines/Members/Lapis.lean | 2 + .../Compile/TruthMines/Members/Lean4Lean.lean | 2 + .../TruthMines/Members/LeanBridge.lean | 2 + .../Compile/TruthMines/Members/LeanCert.lean | 2 + .../Compile/TruthMines/Members/LeanEff.lean | 2 + .../Compile/TruthMines/Members/LeanGrpc.lean | 2 + .../Members/LeanMachineLearning.lean | 2 + .../Compile/TruthMines/Members/LeanRedis.lean | 2 + .../TruthMines/Members/LeanReducers.lean | 2 + .../TruthMines/Members/LeanSearchClient.lean | 2 + .../TruthMines/Members/LeanSha256.lean | 2 + .../Compile/TruthMines/Members/LeanTea.lean | 2 + .../Compile/TruthMines/Members/LeanUri.lean | 2 + .../TruthMines/Members/LiterateLean.lean | 2 + .../Compile/TruthMines/Members/Loogle.lean | 2 + .../Compile/TruthMines/Members/MD4Lean.lean | 2 + .../Compile/TruthMines/Members/MRiscX.lean | 2 + .../Compile/TruthMines/Members/Mathlib.lean | 2 + .../Compile/TruthMines/Members/Maze.lean | 2 + .../Compile/TruthMines/Members/Numbers.lean | 2 + .../Compile/TruthMines/Members/Pacioli.lean | 2 + .../Compile/TruthMines/Members/Palomar.lean | 5 + .../TruthMines/Members/Paperproof.lean | 2 + .../Compile/TruthMines/Members/Parser.lean | 2 + .../TruthMines/Members/PhiConfluence.lean | 2 + .../Compile/TruthMines/Members/Plausible.lean | 2 + .../Compile/TruthMines/Members/Plfl.lean | 2 + .../Compile/TruthMines/Members/PolyFun.lean | 2 + .../TruthMines/Members/ProofWidgets.lean | 2 + .../Compile/TruthMines/Members/Protobuf.lean | 2 + Benchmarks/Compile/TruthMines/Members/Qq.lean | 2 + .../TruthMines/Members/Quantum4Lean.lean | 2 + .../Compile/TruthMines/Members/Regex.lean | 2 + .../Compile/TruthMines/Members/SQLite.lean | 2 + .../Compile/TruthMines/Members/Sail.lean | 2 + .../Compile/TruthMines/Members/SemVer.lean | 2 + .../Compile/TruthMines/Members/Statlib.lean | 2 + .../Compile/TruthMines/Members/SubVerso.lean | 2 + .../Compile/TruthMines/Members/TauCeti.lean | 2 + .../Compile/TruthMines/Members/TorchLean.lean | 2 + .../Compile/TruthMines/Members/Toric.lean | 2 + .../TruthMines/Members/UnicodeBasic.lean | 2 + .../Compile/TruthMines/Members/VerilLean.lean | 2 + .../Compile/TruthMines/Members/Verso.lean | 2 + .../TruthMines/Members/YulSemantics.lean | 2 + .../Compile/TruthMines/Members/leansi.lean | 2 + .../Compile/TruthMines/lake-manifest.json | 807 ++++++++++++++++++ Benchmarks/Compile/TruthMines/lakefile.toml | 18 + Benchmarks/Compile/TruthMines/lean-toolchain | 1 + Benchmarks/TruthMinesSpec/Main.lean | 80 +- Benchmarks/TruthMinesSpec/Projection.lean | 81 +- Ix/AuxGen/BRecOn.lean | 19 +- Ix/Cli/ValidateCmd.lean | 9 +- Ix/Meta.lean | 10 +- Tests/Ix/Compile/Mutual.lean | 20 + Tests/Ix/TruthMines.lean | 9 +- Tests/Ix/TruthMinesRecords.lean | 68 +- crates/compile/src/compile/aux_gen/brecon.rs | 31 +- 92 files changed, 1265 insertions(+), 62 deletions(-) create mode 100644 Benchmarks/Compile/TruthMines/Members/A.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/AddCombi.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Aesop.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Apportionmentlib.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/B.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/BET.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Base64.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Batteries.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/BibtexQuery.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Bignum.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Binary.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/CamCombi.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Carleson.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Cli.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/CombinatorialGames.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/CompPoly.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Cslib.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Curl.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/DescriptiveComplexity.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/DocGen4.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/DomainTheory.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Export.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/FLT.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Fad.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Flow.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/GibbsMeasure.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/HaskellSpec.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/I18n.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Illuminate.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/ImpLab.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/ImportGraph.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/KolmogorovExtension4.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LSpec.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Lapis.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Lean4Lean.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanBridge.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanCert.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanEff.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanGrpc.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanMachineLearning.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanRedis.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanReducers.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanSearchClient.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanSha256.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanTea.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LeanUri.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/LiterateLean.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Loogle.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/MD4Lean.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/MRiscX.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Mathlib.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Maze.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Numbers.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Pacioli.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Palomar.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Paperproof.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Parser.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/PhiConfluence.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Plausible.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Plfl.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/PolyFun.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/ProofWidgets.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Protobuf.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Qq.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Quantum4Lean.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Regex.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/SQLite.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Sail.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/SemVer.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Statlib.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/SubVerso.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/TauCeti.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/TorchLean.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Toric.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/UnicodeBasic.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/VerilLean.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/Verso.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/YulSemantics.lean create mode 100644 Benchmarks/Compile/TruthMines/Members/leansi.lean create mode 100644 Benchmarks/Compile/TruthMines/lake-manifest.json create mode 100644 Benchmarks/Compile/TruthMines/lakefile.toml create mode 100644 Benchmarks/Compile/TruthMines/lean-toolchain diff --git a/Benchmarks/Compile/README.md b/Benchmarks/Compile/README.md index 28278aace..31ee0c707 100644 --- a/Benchmarks/Compile/README.md +++ b/Benchmarks/Compile/README.md @@ -5,6 +5,10 @@ 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) +- Every native TruthMines member, independently, through the generated + `TruthMines/Members/.lean` fidelity drivers +- [Palomar.ix](https://github.com/argumentcomputer/Palomar.ix) as one aggregate + library (its colliding constituent projects remain in isolated workspaces) ## Usage @@ -12,5 +16,14 @@ First ensure the Lean version used to build Ix matches the `Benchmarks/Compile/l `ix compile /path/to/Compile.lean` # replace `` with `Init`, `InitStd`, `Lean`, `Mathlib`, or `FLT` +For a TruthMines constituent, use the nested fidelity workspace, for example: + +`ix validate Benchmarks/Compile/TruthMines/Members/Cli.lean` + +The native member wrappers import the canonical generated TruthMines drivers, +so the catalog records remain the only source of dependency pins. Run the +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. diff --git a/Benchmarks/Compile/TruthMines/Members/A.lean b/Benchmarks/Compile/TruthMines/Members/A.lean new file mode 100644 index 000000000..ba9bac79c --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/A.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.A diff --git a/Benchmarks/Compile/TruthMines/Members/AddCombi.lean b/Benchmarks/Compile/TruthMines/Members/AddCombi.lean new file mode 100644 index 000000000..6a163d864 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/AddCombi.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.AddCombi diff --git a/Benchmarks/Compile/TruthMines/Members/Aesop.lean b/Benchmarks/Compile/TruthMines/Members/Aesop.lean new file mode 100644 index 000000000..de1ad3560 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Aesop.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Aesop diff --git a/Benchmarks/Compile/TruthMines/Members/Apportionmentlib.lean b/Benchmarks/Compile/TruthMines/Members/Apportionmentlib.lean new file mode 100644 index 000000000..ece1c1289 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Apportionmentlib.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Apportionmentlib diff --git a/Benchmarks/Compile/TruthMines/Members/B.lean b/Benchmarks/Compile/TruthMines/Members/B.lean new file mode 100644 index 000000000..02c7dd38d --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/B.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.B diff --git a/Benchmarks/Compile/TruthMines/Members/BET.lean b/Benchmarks/Compile/TruthMines/Members/BET.lean new file mode 100644 index 000000000..a609b65a8 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/BET.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.BET diff --git a/Benchmarks/Compile/TruthMines/Members/Base64.lean b/Benchmarks/Compile/TruthMines/Members/Base64.lean new file mode 100644 index 000000000..1e0e0f7b4 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Base64.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Base64 diff --git a/Benchmarks/Compile/TruthMines/Members/Batteries.lean b/Benchmarks/Compile/TruthMines/Members/Batteries.lean new file mode 100644 index 000000000..23db6ea6e --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Batteries.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Batteries diff --git a/Benchmarks/Compile/TruthMines/Members/BibtexQuery.lean b/Benchmarks/Compile/TruthMines/Members/BibtexQuery.lean new file mode 100644 index 000000000..335a7e2e2 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/BibtexQuery.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.BibtexQuery diff --git a/Benchmarks/Compile/TruthMines/Members/Bignum.lean b/Benchmarks/Compile/TruthMines/Members/Bignum.lean new file mode 100644 index 000000000..05f9c9789 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Bignum.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Bignum diff --git a/Benchmarks/Compile/TruthMines/Members/Binary.lean b/Benchmarks/Compile/TruthMines/Members/Binary.lean new file mode 100644 index 000000000..7407cc75c --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Binary.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Binary diff --git a/Benchmarks/Compile/TruthMines/Members/CamCombi.lean b/Benchmarks/Compile/TruthMines/Members/CamCombi.lean new file mode 100644 index 000000000..1830c4b1d --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/CamCombi.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.CamCombi diff --git a/Benchmarks/Compile/TruthMines/Members/Carleson.lean b/Benchmarks/Compile/TruthMines/Members/Carleson.lean new file mode 100644 index 000000000..37539c585 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Carleson.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Carleson diff --git a/Benchmarks/Compile/TruthMines/Members/Cli.lean b/Benchmarks/Compile/TruthMines/Members/Cli.lean new file mode 100644 index 000000000..a13cdcf64 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Cli.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Cli diff --git a/Benchmarks/Compile/TruthMines/Members/CombinatorialGames.lean b/Benchmarks/Compile/TruthMines/Members/CombinatorialGames.lean new file mode 100644 index 000000000..d9cfa622b --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/CombinatorialGames.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.CombinatorialGames diff --git a/Benchmarks/Compile/TruthMines/Members/CompPoly.lean b/Benchmarks/Compile/TruthMines/Members/CompPoly.lean new file mode 100644 index 000000000..c2f8f3129 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/CompPoly.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.CompPoly diff --git a/Benchmarks/Compile/TruthMines/Members/Cslib.lean b/Benchmarks/Compile/TruthMines/Members/Cslib.lean new file mode 100644 index 000000000..33651ea08 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Cslib.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Cslib diff --git a/Benchmarks/Compile/TruthMines/Members/Curl.lean b/Benchmarks/Compile/TruthMines/Members/Curl.lean new file mode 100644 index 000000000..047c38b66 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Curl.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Curl diff --git a/Benchmarks/Compile/TruthMines/Members/DescriptiveComplexity.lean b/Benchmarks/Compile/TruthMines/Members/DescriptiveComplexity.lean new file mode 100644 index 000000000..44d72b283 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/DescriptiveComplexity.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.DescriptiveComplexity diff --git a/Benchmarks/Compile/TruthMines/Members/DocGen4.lean b/Benchmarks/Compile/TruthMines/Members/DocGen4.lean new file mode 100644 index 000000000..35a65a260 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/DocGen4.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.DocGen4 diff --git a/Benchmarks/Compile/TruthMines/Members/DomainTheory.lean b/Benchmarks/Compile/TruthMines/Members/DomainTheory.lean new file mode 100644 index 000000000..06011d623 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/DomainTheory.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.DomainTheory diff --git a/Benchmarks/Compile/TruthMines/Members/Export.lean b/Benchmarks/Compile/TruthMines/Members/Export.lean new file mode 100644 index 000000000..a2d29a3df --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Export.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Export diff --git a/Benchmarks/Compile/TruthMines/Members/FLT.lean b/Benchmarks/Compile/TruthMines/Members/FLT.lean new file mode 100644 index 000000000..19aad738f --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/FLT.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.FLT diff --git a/Benchmarks/Compile/TruthMines/Members/Fad.lean b/Benchmarks/Compile/TruthMines/Members/Fad.lean new file mode 100644 index 000000000..b9f95eefc --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Fad.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Fad diff --git a/Benchmarks/Compile/TruthMines/Members/Flow.lean b/Benchmarks/Compile/TruthMines/Members/Flow.lean new file mode 100644 index 000000000..f0e489796 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Flow.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Flow diff --git a/Benchmarks/Compile/TruthMines/Members/GibbsMeasure.lean b/Benchmarks/Compile/TruthMines/Members/GibbsMeasure.lean new file mode 100644 index 000000000..97872afe8 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/GibbsMeasure.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.GibbsMeasure diff --git a/Benchmarks/Compile/TruthMines/Members/HaskellSpec.lean b/Benchmarks/Compile/TruthMines/Members/HaskellSpec.lean new file mode 100644 index 000000000..18e61bf5e --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/HaskellSpec.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.HaskellSpec diff --git a/Benchmarks/Compile/TruthMines/Members/I18n.lean b/Benchmarks/Compile/TruthMines/Members/I18n.lean new file mode 100644 index 000000000..2391d8e20 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/I18n.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.I18n diff --git a/Benchmarks/Compile/TruthMines/Members/Illuminate.lean b/Benchmarks/Compile/TruthMines/Members/Illuminate.lean new file mode 100644 index 000000000..295683d46 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Illuminate.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Illuminate diff --git a/Benchmarks/Compile/TruthMines/Members/ImpLab.lean b/Benchmarks/Compile/TruthMines/Members/ImpLab.lean new file mode 100644 index 000000000..bdff105af --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/ImpLab.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.ImpLab diff --git a/Benchmarks/Compile/TruthMines/Members/ImportGraph.lean b/Benchmarks/Compile/TruthMines/Members/ImportGraph.lean new file mode 100644 index 000000000..2acaa361a --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/ImportGraph.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.ImportGraph diff --git a/Benchmarks/Compile/TruthMines/Members/KolmogorovExtension4.lean b/Benchmarks/Compile/TruthMines/Members/KolmogorovExtension4.lean new file mode 100644 index 000000000..97ea91b02 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/KolmogorovExtension4.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.KolmogorovExtension4 diff --git a/Benchmarks/Compile/TruthMines/Members/LSpec.lean b/Benchmarks/Compile/TruthMines/Members/LSpec.lean new file mode 100644 index 000000000..deb87c83a --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LSpec.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LSpec diff --git a/Benchmarks/Compile/TruthMines/Members/Lapis.lean b/Benchmarks/Compile/TruthMines/Members/Lapis.lean new file mode 100644 index 000000000..c52266832 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Lapis.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Lapis diff --git a/Benchmarks/Compile/TruthMines/Members/Lean4Lean.lean b/Benchmarks/Compile/TruthMines/Members/Lean4Lean.lean new file mode 100644 index 000000000..f3f063175 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Lean4Lean.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Lean4Lean diff --git a/Benchmarks/Compile/TruthMines/Members/LeanBridge.lean b/Benchmarks/Compile/TruthMines/Members/LeanBridge.lean new file mode 100644 index 000000000..9011e3105 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanBridge.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanBridge diff --git a/Benchmarks/Compile/TruthMines/Members/LeanCert.lean b/Benchmarks/Compile/TruthMines/Members/LeanCert.lean new file mode 100644 index 000000000..f0b17b298 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanCert.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanCert diff --git a/Benchmarks/Compile/TruthMines/Members/LeanEff.lean b/Benchmarks/Compile/TruthMines/Members/LeanEff.lean new file mode 100644 index 000000000..5ecb62294 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanEff.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanEff diff --git a/Benchmarks/Compile/TruthMines/Members/LeanGrpc.lean b/Benchmarks/Compile/TruthMines/Members/LeanGrpc.lean new file mode 100644 index 000000000..a96c22668 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanGrpc.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanGrpc diff --git a/Benchmarks/Compile/TruthMines/Members/LeanMachineLearning.lean b/Benchmarks/Compile/TruthMines/Members/LeanMachineLearning.lean new file mode 100644 index 000000000..c6e10b3e6 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanMachineLearning.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanMachineLearning diff --git a/Benchmarks/Compile/TruthMines/Members/LeanRedis.lean b/Benchmarks/Compile/TruthMines/Members/LeanRedis.lean new file mode 100644 index 000000000..b02cbe4c7 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanRedis.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanRedis diff --git a/Benchmarks/Compile/TruthMines/Members/LeanReducers.lean b/Benchmarks/Compile/TruthMines/Members/LeanReducers.lean new file mode 100644 index 000000000..352091908 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanReducers.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanReducers diff --git a/Benchmarks/Compile/TruthMines/Members/LeanSearchClient.lean b/Benchmarks/Compile/TruthMines/Members/LeanSearchClient.lean new file mode 100644 index 000000000..716db055e --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanSearchClient.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanSearchClient diff --git a/Benchmarks/Compile/TruthMines/Members/LeanSha256.lean b/Benchmarks/Compile/TruthMines/Members/LeanSha256.lean new file mode 100644 index 000000000..218db67b0 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanSha256.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanSha256 diff --git a/Benchmarks/Compile/TruthMines/Members/LeanTea.lean b/Benchmarks/Compile/TruthMines/Members/LeanTea.lean new file mode 100644 index 000000000..7df6778fa --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanTea.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanTea diff --git a/Benchmarks/Compile/TruthMines/Members/LeanUri.lean b/Benchmarks/Compile/TruthMines/Members/LeanUri.lean new file mode 100644 index 000000000..401f300c3 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LeanUri.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LeanUri diff --git a/Benchmarks/Compile/TruthMines/Members/LiterateLean.lean b/Benchmarks/Compile/TruthMines/Members/LiterateLean.lean new file mode 100644 index 000000000..7e4c07a7d --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/LiterateLean.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.LiterateLean diff --git a/Benchmarks/Compile/TruthMines/Members/Loogle.lean b/Benchmarks/Compile/TruthMines/Members/Loogle.lean new file mode 100644 index 000000000..81c52bee3 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Loogle.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Loogle diff --git a/Benchmarks/Compile/TruthMines/Members/MD4Lean.lean b/Benchmarks/Compile/TruthMines/Members/MD4Lean.lean new file mode 100644 index 000000000..62bd8545b --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/MD4Lean.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.MD4Lean diff --git a/Benchmarks/Compile/TruthMines/Members/MRiscX.lean b/Benchmarks/Compile/TruthMines/Members/MRiscX.lean new file mode 100644 index 000000000..2897d3f10 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/MRiscX.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.MRiscX diff --git a/Benchmarks/Compile/TruthMines/Members/Mathlib.lean b/Benchmarks/Compile/TruthMines/Members/Mathlib.lean new file mode 100644 index 000000000..4b128bda4 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Mathlib.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Mathlib diff --git a/Benchmarks/Compile/TruthMines/Members/Maze.lean b/Benchmarks/Compile/TruthMines/Members/Maze.lean new file mode 100644 index 000000000..0e9e887df --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Maze.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Maze diff --git a/Benchmarks/Compile/TruthMines/Members/Numbers.lean b/Benchmarks/Compile/TruthMines/Members/Numbers.lean new file mode 100644 index 000000000..0ba6dc81f --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Numbers.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Numbers diff --git a/Benchmarks/Compile/TruthMines/Members/Pacioli.lean b/Benchmarks/Compile/TruthMines/Members/Pacioli.lean new file mode 100644 index 000000000..293d16815 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Pacioli.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Pacioli diff --git a/Benchmarks/Compile/TruthMines/Members/Palomar.lean b/Benchmarks/Compile/TruthMines/Members/Palomar.lean new file mode 100644 index 000000000..91ee140a2 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Palomar.lean @@ -0,0 +1,5 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +/- Palomar's constituent projects intentionally remain in isolated workspaces +because their source module names collide. This driver validates the standalone +Palomar.ix library as the aggregate's Benchmarks/Compile fidelity surface. -/ +import Palomar.Main diff --git a/Benchmarks/Compile/TruthMines/Members/Paperproof.lean b/Benchmarks/Compile/TruthMines/Members/Paperproof.lean new file mode 100644 index 000000000..f21ec5c46 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Paperproof.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Paperproof diff --git a/Benchmarks/Compile/TruthMines/Members/Parser.lean b/Benchmarks/Compile/TruthMines/Members/Parser.lean new file mode 100644 index 000000000..e64e0a7af --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Parser.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Parser diff --git a/Benchmarks/Compile/TruthMines/Members/PhiConfluence.lean b/Benchmarks/Compile/TruthMines/Members/PhiConfluence.lean new file mode 100644 index 000000000..8810802c9 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/PhiConfluence.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.PhiConfluence diff --git a/Benchmarks/Compile/TruthMines/Members/Plausible.lean b/Benchmarks/Compile/TruthMines/Members/Plausible.lean new file mode 100644 index 000000000..8a1d6ad5e --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Plausible.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Plausible diff --git a/Benchmarks/Compile/TruthMines/Members/Plfl.lean b/Benchmarks/Compile/TruthMines/Members/Plfl.lean new file mode 100644 index 000000000..0d9de9e2c --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Plfl.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Plfl diff --git a/Benchmarks/Compile/TruthMines/Members/PolyFun.lean b/Benchmarks/Compile/TruthMines/Members/PolyFun.lean new file mode 100644 index 000000000..e6edb020d --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/PolyFun.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.PolyFun diff --git a/Benchmarks/Compile/TruthMines/Members/ProofWidgets.lean b/Benchmarks/Compile/TruthMines/Members/ProofWidgets.lean new file mode 100644 index 000000000..bbf4c39c6 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/ProofWidgets.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.ProofWidgets diff --git a/Benchmarks/Compile/TruthMines/Members/Protobuf.lean b/Benchmarks/Compile/TruthMines/Members/Protobuf.lean new file mode 100644 index 000000000..8aeb83d3b --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Protobuf.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Protobuf diff --git a/Benchmarks/Compile/TruthMines/Members/Qq.lean b/Benchmarks/Compile/TruthMines/Members/Qq.lean new file mode 100644 index 000000000..784af731d --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Qq.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Qq diff --git a/Benchmarks/Compile/TruthMines/Members/Quantum4Lean.lean b/Benchmarks/Compile/TruthMines/Members/Quantum4Lean.lean new file mode 100644 index 000000000..d37cb34fc --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Quantum4Lean.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Quantum4Lean diff --git a/Benchmarks/Compile/TruthMines/Members/Regex.lean b/Benchmarks/Compile/TruthMines/Members/Regex.lean new file mode 100644 index 000000000..08bc4b441 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Regex.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Regex diff --git a/Benchmarks/Compile/TruthMines/Members/SQLite.lean b/Benchmarks/Compile/TruthMines/Members/SQLite.lean new file mode 100644 index 000000000..dae44479f --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/SQLite.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.SQLite diff --git a/Benchmarks/Compile/TruthMines/Members/Sail.lean b/Benchmarks/Compile/TruthMines/Members/Sail.lean new file mode 100644 index 000000000..496b169ac --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Sail.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Sail diff --git a/Benchmarks/Compile/TruthMines/Members/SemVer.lean b/Benchmarks/Compile/TruthMines/Members/SemVer.lean new file mode 100644 index 000000000..6ee3f6e5c --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/SemVer.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.SemVer diff --git a/Benchmarks/Compile/TruthMines/Members/Statlib.lean b/Benchmarks/Compile/TruthMines/Members/Statlib.lean new file mode 100644 index 000000000..c97bc1dac --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Statlib.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Statlib diff --git a/Benchmarks/Compile/TruthMines/Members/SubVerso.lean b/Benchmarks/Compile/TruthMines/Members/SubVerso.lean new file mode 100644 index 000000000..652bb3292 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/SubVerso.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.SubVerso diff --git a/Benchmarks/Compile/TruthMines/Members/TauCeti.lean b/Benchmarks/Compile/TruthMines/Members/TauCeti.lean new file mode 100644 index 000000000..ed12fffde --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/TauCeti.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.TauCeti diff --git a/Benchmarks/Compile/TruthMines/Members/TorchLean.lean b/Benchmarks/Compile/TruthMines/Members/TorchLean.lean new file mode 100644 index 000000000..6f24c271f --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/TorchLean.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.TorchLean diff --git a/Benchmarks/Compile/TruthMines/Members/Toric.lean b/Benchmarks/Compile/TruthMines/Members/Toric.lean new file mode 100644 index 000000000..07ea965ec --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Toric.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Toric diff --git a/Benchmarks/Compile/TruthMines/Members/UnicodeBasic.lean b/Benchmarks/Compile/TruthMines/Members/UnicodeBasic.lean new file mode 100644 index 000000000..644d4c101 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/UnicodeBasic.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.UnicodeBasic diff --git a/Benchmarks/Compile/TruthMines/Members/VerilLean.lean b/Benchmarks/Compile/TruthMines/Members/VerilLean.lean new file mode 100644 index 000000000..85d889fd2 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/VerilLean.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.VerilLean diff --git a/Benchmarks/Compile/TruthMines/Members/Verso.lean b/Benchmarks/Compile/TruthMines/Members/Verso.lean new file mode 100644 index 000000000..eff67c8e3 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/Verso.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.Verso diff --git a/Benchmarks/Compile/TruthMines/Members/YulSemantics.lean b/Benchmarks/Compile/TruthMines/Members/YulSemantics.lean new file mode 100644 index 000000000..88dbb6606 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/YulSemantics.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.YulSemantics diff --git a/Benchmarks/Compile/TruthMines/Members/leansi.lean b/Benchmarks/Compile/TruthMines/Members/leansi.lean new file mode 100644 index 000000000..21d46864b --- /dev/null +++ b/Benchmarks/Compile/TruthMines/Members/leansi.lean @@ -0,0 +1,2 @@ +/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/ +import Drivers.leansi diff --git a/Benchmarks/Compile/TruthMines/lake-manifest.json b/Benchmarks/Compile/TruthMines/lake-manifest.json new file mode 100644 index 000000000..a80f29677 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/lake-manifest.json @@ -0,0 +1,807 @@ +{"version": "1.2.0", + "packagesDir": "../../TruthMines/.lake/packages", + "packages": + [{"url": "https://github.com/argumentcomputer/Palomar.ix", + "type": "git", + "subDir": null, + "scope": "", + "rev": "879aba8e6c7419bf40549f470e8867ef52c12a54", + "name": "palomar_ix", + "manifestFile": "lake-manifest.json", + "inputRev": "879aba8e6c7419bf40549f470e8867ef52c12a54", + "inherited": false, + "configFile": "lakefile.lean"}, + {"type": "path", + "scope": "", + "name": "truthmines", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../../TruthMines", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/arademaker/fad", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d9a9328f8819b2a2bb831a2b25992dcadf432878", + "name": "fad", + "manifestFile": "lake-manifest.json", + "inputRev": "d9a9328f8819b2a2bb831a2b25992dcadf432878", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/arademaker/bignum", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4b32a232d3481f9a7b4b3c101fa0dcd946392508", + "name": "bignum", + "manifestFile": "lake-manifest.json", + "inputRev": "4b32a232d3481f9a7b4b3c101fa0dcd946392508", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/Verified-zkEVM/PolyFun", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4247ad7e8fa5ece217508af97bc2e24b168a1cf6", + "name": "PolyFun", + "manifestFile": "lake-manifest.json", + "inputRev": "4247ad7e8fa5ece217508af97bc2e24b168a1cf6", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/rami3l/PLFaLean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "138c217949256462d1ed68853ab650b0bacd48f8", + "name": "plfl", + "manifestFile": "lake-manifest.json", + "inputRev": "138c217949256462d1ed68853ab650b0bacd48f8", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/objectionary/proof", + "type": "git", + "subDir": null, + "scope": "", + "rev": "58aa7731076d02bf51b2dfbcdc06c4f764101fb4", + "name": "«phi-confluence»", + "manifestFile": "lake-manifest.json", + "inputRev": "58aa7731076d02bf51b2dfbcdc06c4f764101fb4", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/ojhermann-org/pacioli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "9fa4ff363174f78ba19d74ceb1d7fc5c6efbfb90", + "name": "pacioli", + "manifestFile": "lake-manifest.json", + "inputRev": "9fa4ff363174f78ba19d74ceb1d7fc5c6efbfb90", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/SrGaabriel/lapis", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2de2282ec7f5ecae75a3c338c02a930771e691df", + "name": "lapis", + "manifestFile": "lake-manifest.json", + "inputRev": "2de2282ec7f5ecae75a3c338c02a930771e691df", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/RemyDegenne/kolmogorov_extension4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "7d76e184c3d2138a2741baf923b57e9a01b9cf25", + "name": "kolmogorov_extension4", + "manifestFile": "lake-manifest.json", + "inputRev": "7d76e184c3d2138a2741baf923b57e9a01b9cf25", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/ImperialCollegeLondon/FLT", + "type": "git", + "subDir": null, + "scope": "", + "rev": "45eb9afc55ce36516fc98ba10618c010fdced7dc", + "name": "flt", + "manifestFile": "lake-manifest.json", + "inputRev": "45eb9afc55ce36516fc98ba10618c010fdced7dc", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/zilberstein/domain-theory", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5c667c350be8b83ab49e3f9d26d7db8fb90b5f50", + "name": "«domain-theory»", + "manifestFile": "lake-manifest.json", + "inputRev": "5c667c350be8b83ab49e3f9d26d7db8fb90b5f50", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/PierreSenellart/descriptive-complexity", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5e054e156f0e1a97db28b6fe274d78834afd8ddb", + "name": "«descriptive-complexity»", + "manifestFile": "lake-manifest.json", + "inputRev": "5e054e156f0e1a97db28b6fe274d78834afd8ddb", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/cslib", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a1faa284cc5923ac11a4b8d2452749a174ef8cf1", + "name": "cslib", + "manifestFile": "lake-manifest.json", + "inputRev": "a1faa284cc5923ac11a4b8d2452749a174ef8cf1", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fpvandoorn/carleson", + "type": "git", + "subDir": null, + "scope": "", + "rev": "abad489adf7eb4e94ef5933d9880877c76fbd09f", + "name": "carleson", + "manifestFile": "lake-manifest.json", + "inputRev": "abad489adf7eb4e94ef5933d9880877c76fbd09f", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/YaelDillies/Toric", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e3aa113849165565a7d5ccfba5ee2203fa75b17a", + "name": "Toric", + "manifestFile": "lake-manifest.json", + "inputRev": "e3aa113849165565a7d5ccfba5ee2203fa75b17a", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/TauCetiProject/TauCeti", + "type": "git", + "subDir": null, + "scope": "", + "rev": "afb1aacb3632d3236eee756ea1683290c07270a3", + "name": "TauCeti", + "manifestFile": "lake-manifest.json", + "inputRev": "afb1aacb3632d3236eee756ea1683290c07270a3", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/lean-dojo/TorchLean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "fa6bbe3bf0d93679422be8a14978c26ee55d98ff", + "name": "TorchLean", + "manifestFile": "lake-manifest.json", + "inputRev": "fa6bbe3bf0d93679422be8a14978c26ee55d98ff", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/stat-lib/Statlib", + "type": "git", + "subDir": null, + "scope": "", + "rev": "01d2a03770455f5c775bb25c57e7fbb8e1eaf8d8", + "name": "Statlib", + "manifestFile": "lake-manifest.json", + "inputRev": "01d2a03770455f5c775bb25c57e7fbb8e1eaf8d8", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/JulsDE/MRiscX", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5dc879f717cf69d76805a38927ef086d0c2ea257", + "name": "MRiscX", + "manifestFile": "lake-manifest.json", + "inputRev": "5dc879f717cf69d76805a38927ef086d0c2ea257", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/LeanMachineLearning/LML", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0dcb334ae15427bb297a0cc7e0008292ec4d63af", + "name": "LeanMachineLearning", + "manifestFile": "lake-manifest.json", + "inputRev": "0dcb334ae15427bb297a0cc7e0008292ec4d63af", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/alerad/LeanCert", + "type": "git", + "subDir": null, + "scope": "", + "rev": "501b2c09e367721f58200f53261787a3d280abe2", + "name": "LeanCert", + "manifestFile": "lake-manifest.json", + "inputRev": "501b2c09e367721f58200f53261787a3d280abe2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/CBirkbeck/LeanBridge", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4dffaca404780f5ec439bda834fbc90a891174c2", + "name": "LeanBridge", + "manifestFile": "lake-manifest.json", + "inputRev": "4dffaca404780f5ec439bda834fbc90a891174c2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/YaelDillies/gibbs-measure", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2c57fb5f363f6afeb252b008f2bcedbd1b87b8cc", + "name": "GibbsMeasure", + "manifestFile": "lake-manifest.json", + "inputRev": "2c57fb5f363f6afeb252b008f2bcedbd1b87b8cc", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/Verified-zkEVM/CompPoly", + "type": "git", + "subDir": null, + "scope": "", + "rev": "75c0681bd37567af00e8f0bd13fd59f1423e4217", + "name": "CompPoly", + "manifestFile": "lake-manifest.json", + "inputRev": "75c0681bd37567af00e8f0bd13fd59f1423e4217", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/vihdzp/combinatorial-games", + "type": "git", + "subDir": null, + "scope": "", + "rev": "99a469a2e02fd9fab9a717efe27f7fc84b880bbb", + "name": "CombinatorialGames", + "manifestFile": "lake-manifest.json", + "inputRev": "99a469a2e02fd9fab9a717efe27f7fc84b880bbb", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/YaelDillies/cam-combi", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2e8be1b215cc08853390d8fde013e503bb9d0863", + "name": "CamCombi", + "manifestFile": "lake-manifest.json", + "inputRev": "2e8be1b215cc08853390d8fde013e503bb9d0863", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/mseri/BET", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e984d1b08f6c6d07fa690a78674e9ac6ef1050c2", + "name": "BET", + "manifestFile": "lake-manifest.json", + "inputRev": "e984d1b08f6c6d07fa690a78674e9ac6ef1050c2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/mdbrnowski/Apportionmentlib", + "type": "git", + "subDir": null, + "scope": "", + "rev": "34e0fb30422829494ba7d634e5ed983db94e54a2", + "name": "Apportionmentlib", + "manifestFile": "lake-manifest.json", + "inputRev": "34e0fb30422829494ba7d634e5ed983db94e54a2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/add-combi", + "type": "git", + "subDir": null, + "scope": "", + "rev": "ecee0cf8bff785b2bdffe2e292a7e08e77384c60", + "name": "AddCombi", + "manifestFile": "lake-manifest.json", + "inputRev": "ecee0cf8bff785b2bdffe2e292a7e08e77384c60", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "aceca4eeb5a79092eabefaa75fcb72b701d02205", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "aceca4eeb5a79092eabefaa75fcb72b701d02205", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/powdr-labs/yul-semantics", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d557aacbf4937ee1f7d08e32f8569108d7045eea", + "name": "«yul-semantics»", + "manifestFile": "lake-manifest.json", + "inputRev": "d557aacbf4937ee1f7d08e32f8569108d7045eea", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/verso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "74fc8d1b7bb781c3623a06ec6484f34d35eb5fba", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inputRev": "74fc8d1b7bb781c3623a06ec6484f34d35eb5fba", + "inherited": true, + "configFile": "lakefile.lean"}, + {"type": "path", + "scope": "", + "name": "relocFixtureA", + "manifestFile": "lake-manifest.json", + "inherited": true, + "dir": "../../TruthMines/../Catalog/RelocFixtureA", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/Lean-zh/protobuf", + "type": "git", + "subDir": null, + "scope": "", + "rev": "8c707f2cb4ab8eae280127651162d28e58164c1e", + "name": "protobuf", + "manifestFile": "lake-manifest.json", + "inputRev": "8c707f2cb4ab8eae280127651162d28e58164c1e", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/palladin/lean-reducers", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6e93e0ce326025f762d00b947716c2b98ce1fb06", + "name": "lean_reducers", + "manifestFile": "lake-manifest.json", + "inputRev": "6e93e0ce326025f762d00b947716c2b98ce1fb06", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/palladin/lean-eff", + "type": "git", + "subDir": null, + "scope": "", + "rev": "453f4feb6508ec787fc325a70523d38e4378ef8f", + "name": "lean_eff", + "manifestFile": "lake-manifest.json", + "inputRev": "453f4feb6508ec787fc325a70523d38e4378ef8f", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/digama0/lean4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e0e3f6bcccb840cb0ea6f11c2b274ada93a12e00", + "name": "lean4lean", + "manifestFile": "lake-manifest.json", + "inputRev": "e0e3f6bcccb840cb0ea6f11c2b274ada93a12e00", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "16f02aa7642864af59f1ff0e384a015994db9118", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/hhu-adam/lean-i18n", + "type": "git", + "subDir": null, + "scope": "", + "rev": "1a99b00a940624c0a6c3009b756fb922acf0fe78", + "name": "i18n", + "manifestFile": "lake-manifest.json", + "inputRev": "1a99b00a940624c0a6c3009b756fb922acf0fe78", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-parser", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e2c2439d75fe54df49f72f809d22ceeacf261f21", + "name": "Parser", + "manifestFile": "lake-manifest.json", + "inputRev": "e2c2439d75fe54df49f72f809d22ceeacf261f21", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/argumentcomputer/LSpec", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e780f4188c9649aef988270f4d126651460ca9c4", + "name": "LSpec", + "manifestFile": "lake-manifest.json", + "inputRev": "e780f4188c9649aef988270f4d126651460ca9c4", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3a75ede05278806fd3249bb0c97a6fb5777a4f7d", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "3a75ede05278806fd3249bb0c97a6fb5777a4f7d", + "inherited": true, + "configFile": "lakefile.lean"}, + {"type": "path", + "scope": "", + "name": "relocFixtureB", + "manifestFile": "lake-manifest.json", + "inherited": true, + "dir": "../../TruthMines/../Catalog/RelocFixtureB", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/T-Brick/Numbers", + "type": "git", + "subDir": null, + "scope": "", + "rev": "f6494eb3029f3784fb9f5902e3c2c65ce917860b", + "name": "numbers", + "manifestFile": "lake-manifest.json", + "inputRev": "f6494eb3029f3784fb9f5902e3c2c65ce917860b", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dwrensha/lean4-maze", + "type": "git", + "subDir": null, + "scope": "", + "rev": "fb7e61cb1a224ead7eac95de1511620861cd44fe", + "name": "maze", + "manifestFile": "lake-manifest.json", + "inputRev": "fb7e61cb1a224ead7eac95de1511620861cd44fe", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/nomeata/loogle", + "type": "git", + "subDir": null, + "scope": "", + "rev": "9f11169aaebf1ed1e7dcc4077f2aafe0fcf66fd0", + "name": "loogle", + "manifestFile": "lake-manifest.json", + "inputRev": "9f11169aaebf1ed1e7dcc4077f2aafe0fcf66fd0", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a117edeff8db819a001455bcbafe86748635dd6b", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "a117edeff8db819a001455bcbafe86748635dd6b", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/schergen-org/Leansi", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a4524cea6cf5a56d6433cdbfaa04bca98fa8b1d0", + "name": "leansi", + "manifestFile": "lake-manifest.json", + "inputRev": "a4524cea6cf5a56d6433cdbfaa04bca98fa8b1d0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4export", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b18d673bd29b476466a51a3be1012df2ed322b10", + "name": "lean4export", + "manifestFile": "lake-manifest.json", + "inputRev": "b18d673bd29b476466a51a3be1012df2ed322b10", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/predictable-machines/lean4-base64", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0f457b464797b5c4bde04548307f02f58ffebbd5", + "name": "«lean4-base64»", + "manifestFile": "lake-manifest.json", + "inputRev": "0f457b464797b5c4bde04548307f02f58ffebbd5", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/josephmckinsey/lean-uri", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4d717ff58f42b229ac08815855087344a62ec613", + "name": "«lean-uri»", + "manifestFile": "lake-manifest.json", + "inputRev": "4d717ff58f42b229ac08815855087344a62ec613", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/runbikeswim/lean-semver", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b818b68404b788acc8521ebc5d1db7913d543337", + "name": "«lean-semver»", + "manifestFile": "lake-manifest.json", + "inputRev": "b818b68404b788acc8521ebc5d1db7913d543337", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/rems-project/lean-sail", + "type": "git", + "subDir": null, + "scope": "", + "rev": "079463134b9c50450b8393e1566a09fc492a34d9", + "name": "«lean-sail»", + "manifestFile": "lake-manifest.json", + "inputRev": "079463134b9c50450b8393e1566a09fc492a34d9", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/ecyrbe/lean-redis", + "type": "git", + "subDir": null, + "scope": "", + "rev": "91685c1e77c84228ba54c1ab39f15288a8179b28", + "name": "«lean-redis»", + "manifestFile": "lake-manifest.json", + "inputRev": "91685c1e77c84228ba54c1ab39f15288a8179b28", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/RileyBetts/lean-grpc", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2e7712ae2f43a26a03790b573e2d788616cef655", + "name": "«lean-grpc»", + "manifestFile": "lake-manifest.json", + "inputRev": "2e7712ae2f43a26a03790b573e2d788616cef655", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/ejgallego/imp-lab", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a56ea1cd6429dba7e093f1483cf59867c5a94ab9", + "name": "implab", + "manifestFile": "lake-manifest.json", + "inputRev": "a56ea1cd6429dba7e093f1483cf59867c5a94ab9", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/illuminate", + "type": "git", + "subDir": null, + "scope": "", + "rev": "76f052847294d189dc9924a33466b4b677f47e67", + "name": "illuminate", + "manifestFile": "lake-manifest.json", + "inputRev": "76f052847294d189dc9924a33466b4b677f47e67", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/haskell-spec/haskell-spec", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d941b26f830712cdc027e04400ad94d3095dab6b", + "name": "«haskell-spec»", + "manifestFile": "lake-manifest.json", + "inputRev": "d941b26f830712cdc027e04400ad94d3095dab6b", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/predictable-machines/lean4-flow", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2f4357427dfdf934b02779cf1f0bd8ded1595ef7", + "name": "flow", + "manifestFile": "lake-manifest.json", + "inputRev": "2f4357427dfdf934b02779cf1f0bd8ded1595ef7", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/Verilean/lean-tea", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3c96270b131f6cab3b7fa41e8b0cfe73655b5481", + "name": "exes", + "manifestFile": "lake-manifest.json", + "inputRev": "3c96270b131f6cab3b7fa41e8b0cfe73655b5481", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/Lean-zh/binary", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c1adb7380ea3a538cd800bc5974a1fa05d8b488e", + "name": "binary", + "manifestFile": "lake-manifest.json", + "inputRev": "c1adb7380ea3a538cd800bc5974a1fa05d8b488e", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/verilog-proof/VerilLean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "18acff7b33019bcbcc64154d5b6fdf566867f4d7", + "name": "VerilLean", + "manifestFile": "lake-manifest.json", + "inputRev": "18acff7b33019bcbcc64154d5b6fdf566867f4d7", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "f199e403002f82257a35add247ae05e00fd01c3c", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "f199e403002f82257a35add247ae05e00fd01c3c", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/pandaman64/lean-regex", + "type": "git", + "subDir": "regex", + "scope": "", + "rev": "30b7188eeecd7268d0f9816f97eb6304083c1bfb", + "name": "Regex", + "manifestFile": "lake-manifest.json", + "inputRev": "30b7188eeecd7268d0f9816f97eb6304083c1bfb", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/Alektronnik/Quantum4Lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0a4ec3a76464fd36dea0150e571daa356350d0bf", + "name": "Quantum4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "0a4ec3a76464fd36dea0150e571daa356350d0bf", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/Paper-Proof/paperproof", + "type": "git", + "subDir": "lean", + "scope": "", + "rev": "69401f7d9348699e1532194734b5dda0771278b7", + "name": "Paperproof", + "manifestFile": "lake-manifest.json", + "inputRev": "69401f7d9348699e1532194734b5dda0771278b7", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "31907cc18f48a95384f99cee5582c00fb39e0f67", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/tani/literate-lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a9be26ba1190072fe4d5b15d9622bdf1bf3a8234", + "name": "LiterateLean", + "manifestFile": "lake-manifest.json", + "inputRev": "a9be26ba1190072fe4d5b15d9622bdf1bf3a8234", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/etheorem/LeanSha256", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d8a7dc10c8a089330f9a13632b6f2a2283e4e43b", + "name": "LeanSha256", + "manifestFile": "lake-manifest.json", + "inputRev": "d8a7dc10c8a089330f9a13632b6f2a2283e4e43b", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/bergmannjg/leanCurl", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d725fede14f67acc746c18eaec962f6461dee5cb", + "name": "Curl", + "manifestFile": "lake-manifest.json", + "inputRev": "d725fede14f67acc746c18eaec962f6461dee5cb", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", + "name": "checkdecls", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}], + "name": "TruthMinesCompile", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/Benchmarks/Compile/TruthMines/lakefile.toml b/Benchmarks/Compile/TruthMines/lakefile.toml new file mode 100644 index 000000000..c0e7c4fa8 --- /dev/null +++ b/Benchmarks/Compile/TruthMines/lakefile.toml @@ -0,0 +1,18 @@ +# GENERATED by `lake exe truthmines gen`; do not edit. +name = "TruthMinesCompile" +version = "0.1.0" +packagesDir = "../../TruthMines/.lake/packages" +defaultTargets = ["TruthMinesMembers"] + +[[lean_lib]] +name = "TruthMinesMembers" +globs = ["Members.+"] + +[[require]] +name = "truthmines" +path = "../../TruthMines" + +[[require]] +name = "palomar_ix" +git = "https://github.com/argumentcomputer/Palomar.ix" +rev = "879aba8e6c7419bf40549f470e8867ef52c12a54" diff --git a/Benchmarks/Compile/TruthMines/lean-toolchain b/Benchmarks/Compile/TruthMines/lean-toolchain new file mode 100644 index 000000000..a8afa7d1b --- /dev/null +++ b/Benchmarks/Compile/TruthMines/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.1 diff --git a/Benchmarks/TruthMinesSpec/Main.lean b/Benchmarks/TruthMinesSpec/Main.lean index 58ce6e579..f98df3f1f 100644 --- a/Benchmarks/TruthMinesSpec/Main.lean +++ b/Benchmarks/TruthMinesSpec/Main.lean @@ -10,17 +10,20 @@ module, roots) for the full or mini tier validate [--mini] [--only Q[,Q…]] [--jobs N] [--ceiling-gb N] [--no-watchdog] - per-member METADATA fidelity: run the 8-phase + per-library METADATA fidelity: run the 8-phase `ix validate` pipeline (aux-gen congruence, alpha canonicity, decompile both ways, per-constant - roundtrip) over each member's driver module — the - same import closure its piece compiles from, so - the records stay the only pin source. Exit-code - gated, no report artifacts. Heavy members + roundtrip) over each member's Benchmarks/Compile + driver — the same import closure its piece compiles + from, so the records stay the only pin source. The + full tier also validates Palomar.ix as one aggregate + library. Exit-code gated, no report artifacts. Heavy members (mathlib-class) hold two compile+decompile states at once, so the default is one member at a time - under the box-level ceiling; raise --jobs for - small-member sweeps or --only subsets. + under the box-level ceiling. Sweeps first prebuild + their selected drivers in one Lake process, then run + --jobs validators with `--no-build` over the quiescent + shared package store. build [--mini] [--out DIR.ixc] [--jobs N] [--ceiling-gb N] [--no-watchdog] [--no-cache] [--palomar-ixc DIR.ixc] gen-check, build the member root oleans (network + @@ -88,9 +91,15 @@ private structure GenFile where private def genFiles : List GenFile := [ ⟨workspaceLakefilePath, renderWorkspaceLakefile⟩, - ⟨workspaceToolchainPath, renderWorkspaceToolchain⟩ ] + ⟨workspaceToolchainPath, renderWorkspaceToolchain⟩, + ⟨compileWorkspaceLakefilePath, renderCompileWorkspaceLakefile⟩, + ⟨compileWorkspaceToolchainPath, renderWorkspaceToolchain⟩, + ⟨compilePalomarModulePath, renderCompilePalomarModule⟩ ] ++ (driverLibs.map fun lib => ⟨driverModulePath lib.qualifier, renderDriverModule lib⟩).toList + ++ (driverLibs.map fun lib => + ⟨compileMemberModulePath lib.qualifier, + renderCompileMemberModule lib⟩).toList private def readIfExists (path : System.FilePath) : IO (Option String) := do if (← path.pathExists) then return some (← IO.FS.readFile path) @@ -609,6 +618,11 @@ private structure ValidateOptions where noWatchdog : Bool := false mini : Bool := false +private structure ValidationLib where + qualifier : String + driver : System.FilePath +deriving Inhabited + private def parseValidate : List String → Except String ValidateOptions | [] => .ok {} | "--only" :: value :: rest => do @@ -628,9 +642,10 @@ private def parseValidate : List String → Except String ValidateOptions pure { ← parseValidate rest with mini := true } | arg :: _ => .error s!"unknown validate argument `{arg}`" -/-- Per-member metadata-fidelity sweep: the 8-phase `ix validate` - pipeline over each member's driver module. Exit-code gated (the - validator's phase table goes to stdout); no artifacts. -/ +/-- Per-library metadata-fidelity sweep: the 8-phase `ix validate` pipeline + over each native member's `Benchmarks/Compile` driver plus Palomar.ix as + one aggregate library in the full tier. Exit-code gated (the validator's + phase table goes to stdout); no artifacts. -/ private def runValidate (options : ValidateOptions) : IO UInt32 := do let tier := if options.mini then "mini" else "corpus" let spec := if options.mini then catalogMiniSpec else catalogSpec @@ -642,15 +657,22 @@ run `lake exe truthmines gen` first" unless (← ixExe.pathExists) do IO.eprintln s!"{ixExe} missing — run `lake build ix` first" return 1 + let available := spec.libs.map fun lib => { + qualifier := lib.qualifier.toString (escape := false) + driver := compileMemberModulePath lib.qualifier + } + let available := if options.mini then available else available.push { + qualifier := "Palomar" + driver := compilePalomarModulePath + } let libs ← match options.only with - | none => pure spec.libs + | none => pure available | some wanted => do for w in wanted do - unless spec.libs.any (·.qualifier.toString (escape := false) == w) do - IO.eprintln s!"--only names `{w}`, which is not a {tier} member" + unless available.any (·.qualifier == w) do + IO.eprintln s!"--only names `{w}`, which is not a {tier} library" return 1 - pure <| spec.libs.filter fun lib => - wanted.contains (lib.qualifier.toString (escape := false)) + pure <| available.filter fun lib => wanted.contains lib.qualifier let ceiling? : Option Nat ← if options.noWatchdog then pure none @@ -664,18 +686,26 @@ unprotected" return 1 -- Validation holds two compile states plus a decompile state at -- mathlib scale: one member at a time under the box ceiling is the - -- safe default; --jobs is for small-member subsets. + -- safe default. Validation must never race separate Lake builds against + -- the shared package store: prebuild every selected driver in one Lake + -- process, then tell each validator to skip its implicit build. This also + -- makes the single-job path use the same deterministic boundary. let jobs := options.jobs?.getD 1 + stageLine s!"[truthmines] prebuilding {libs.size} selected driver(s) in one Lake process…" + let buildArgs := #["build"] ++ libs.map fun lib => s!"Members.{lib.qualifier}" + let buildExit ← watched ceiling? "lake" buildArgs compileWorkspaceDir + if buildExit != 0 then + reportOom buildExit ceiling? "validate prebuild" + IO.eprintln s!"selected-driver prebuild failed ({buildExit})" + return 1 let exe ← IO.FS.realPath ixExe let root ← IO.currentDir - stageLine s!"[truthmines] validate: {libs.size} member(s), {jobs} in \ -flight ({tier} tier; 8-phase ix validate per driver module)" - let runOne (lib : CatalogSpecLib) : IO MemberOutcome := do - let q := lib.qualifier.toString (escape := false) - let driver := driverModulePath lib.qualifier + stageLine s!"[truthmines] validate: {libs.size} libraries, {jobs} in \ +flight ({tier} tier; 8-phase ix validate per Benchmarks/Compile driver)" + let runOne (lib : ValidationLib) : IO MemberOutcome := do let exit ← watched ceiling? exe.toString - #["validate", driver.toString] root - return { qualifier := q, cached := false, exit } + #["validate", lib.driver.toString, "--no-build"] root + return { qualifier := lib.qualifier, cached := false, exit } let mut pending := libs.toList let mut inFlight : Array (Task (Except IO.Error MemberOutcome)) := #[] let mut failures : List String := [] @@ -697,7 +727,7 @@ flight ({tier} tier; 8-phase ix validate per driver module)" failures := failures ++ [s!"{outcome.qualifier} ({outcome.exit})"] stageLine s!"[truthmines] {outcome.qualifier}: fidelity FAILED \ ({outcome.exit})" - stageLine s!"[truthmines] validate done: {passed}/{libs.size} member(s) \ + stageLine s!"[truthmines] validate done: {passed}/{libs.size} libraries \ clean{if failures.isEmpty then "" else s!"; failed: {failures}"}" return if failures.isEmpty then 0 else 1 diff --git a/Benchmarks/TruthMinesSpec/Projection.lean b/Benchmarks/TruthMinesSpec/Projection.lean index 49a83da4e..f7d322644 100644 --- a/Benchmarks/TruthMinesSpec/Projection.lean +++ b/Benchmarks/TruthMinesSpec/Projection.lean @@ -7,14 +7,15 @@ public import Benchmarks.TruthMinesSpec.Validate namespace TruthMinesSpec /-! Deterministic projections of the typed records into the nested corpus -workspace `Benchmarks/TruthMines/` and into `ix catalog` inputs. The rendered -strings are the whole contract: `lake exe truthmines gen` writes the -workspace files, `gen --check` (and the fast `truthmines-spec` suite) asserts -byte-idempotence against the files on disk, and the catalog spec goes to -`ix catalog` as its positional argument vector — nothing is serialized to an -intermediate format anywhere. `lake-manifest.json` is Lake's own lockfile, -ported once and thereafter maintained by Lake — it is pin-checked against -the records, not rendered. -/ +workspace `Benchmarks/TruthMines/`, the per-library fidelity surface under +`Benchmarks/Compile/TruthMines/`, and `ix catalog` inputs. The rendered strings +are the whole contract: `lake exe truthmines gen` writes the workspace files, +`gen --check` (and the fast `truthmines-spec` suite) asserts byte-idempotence +against the files on disk, and the catalog spec goes to `ix catalog` as its +positional argument vector — nothing is serialized to an intermediate format +anywhere. `lake-manifest.json` is Lake's own lockfile, ported once and +thereafter maintained by Lake — it is pin-checked against the records, not +rendered. -/ def workspaceDir : System.FilePath := "Benchmarks" / "TruthMines" @@ -89,6 +90,70 @@ def renderDriverModule (lib : CatalogSpecLib) : String := ++ (lib.roots.map fun root => s!"import {root.toString (escape := false)}").toList) ++ "\n" +/-- The `Benchmarks/Compile` workspace exposing one independently addressable + fidelity driver for every native TruthMines member. It depends on the + canonical generated workspace, so this surface adds no second pin set. -/ +def compileWorkspaceDir : System.FilePath := + "Benchmarks" / "Compile" / "TruthMines" + +def compileWorkspaceLakefilePath : System.FilePath := + compileWorkspaceDir / "lakefile.toml" + +def compileWorkspaceToolchainPath : System.FilePath := + compileWorkspaceDir / "lean-toolchain" + +def compileWorkspaceManifestPath : System.FilePath := + compileWorkspaceDir / "lake-manifest.json" + +def compileMembersDir : System.FilePath := compileWorkspaceDir / "Members" + +def compileMemberModulePath (qualifier : Lean.Name) : System.FilePath := + compileMembersDir / s!"{qualifier.toString (escape := false)}.lean" + +def compilePalomarModulePath : System.FilePath := + compileMembersDir / "Palomar.lean" + +def palomarRepoUrl : String := + "https://github.com/argumentcomputer/Palomar.ix" + +def palomarRev : String := + "879aba8e6c7419bf40549f470e8867ef52c12a54" + +def renderCompileWorkspaceLakefile : String := + s!"# GENERATED by `lake exe truthmines gen`; do not edit. +name = \"TruthMinesCompile\" +version = \"0.1.0\" +packagesDir = \"../../TruthMines/.lake/packages\" +defaultTargets = [\"TruthMinesMembers\"] + +[[lean_lib]] +name = \"TruthMinesMembers\" +globs = [\"Members.+\"] + +[[require]] +name = \"truthmines\" +path = \"../../TruthMines\" + +[[require]] +name = \"palomar_ix\" +git = \"{palomarRepoUrl}\" +rev = \"{palomarRev}\" +" + +def renderCompilePalomarModule : String := + s!"{generatedHeader} +/- Palomar's constituent projects intentionally remain in isolated workspaces +because their source module names collide. This driver validates the standalone +Palomar.ix library as the aggregate's Benchmarks/Compile fidelity surface. -/ +import Palomar.Main +" + +/-- A thin `Benchmarks/Compile` wrapper around the canonical member driver. + Importing `Drivers.` preserves exactly the member root closure while + keeping the catalog records and generated workspace as the pin authority. -/ +def renderCompileMemberModule (lib : CatalogSpecLib) : String := + s!"{generatedHeader}\nimport Drivers.{lib.qualifier.toString (escape := false)}\n" + /-- The workspace `lakefile.lean`: the union pin set in dependency order, root-module lists and olean-fetch targets for the full spec (`catalogOleans`, the default target) and the mini spec diff --git a/Ix/AuxGen/BRecOn.lean b/Ix/AuxGen/BRecOn.lean index c95ea0582..bcc42a396 100644 --- a/Ix/AuxGen/BRecOn.lean +++ b/Ix/AuxGen/BRecOn.lean @@ -385,15 +385,20 @@ partial def handleSubstcoreStep (decl : LocalDecl) (substInEqBinderKind k abstractedFvarName replacement, { d with domain := substFVar d.domain abstractedFvarName replacement }) - -- Continuation local context: forward deps replaced by their - -- substituted versions; the abstracted fvar removed (`clearH := true`). - let newLocalContext : Array LocalDecl := localContext.filterMap fun d => - if d.fvarName == abstractedFvarName then + -- Continuation local context: `substCore` reverts the abstracted fvar and + -- all forward dependencies, then re-introduces the forward dependencies + -- after every unaffected declaration. This movement is observable by the + -- next substitution: for `C : I i j → T j → I i j`, substituting `i` + -- moves `C` behind `T`, so substituting `j` must discover them in `T, C` + -- order. Remove the old declarations and append their substituted forms; + -- replacing them in place would preserve the stale pre-revert order. + let survivingLocalContext : Array LocalDecl := localContext.filterMap fun d => + if d.fvarName == abstractedFvarName + || forwardDeps.any fun fd => fd.fvarName == d.fvarName then none else - match newForwardDeps.find? (fun nd => nd.fvarName == d.fvarName) with - | some newD => some newD - | none => some d + some d + let newLocalContext := survivingLocalContext ++ newForwardDeps let some innerProof := buildProofForRemaining newRest newBody newLocalContext fvarOrder ctorIdx (depth + 1) diff --git a/Ix/Cli/ValidateCmd.lean b/Ix/Cli/ValidateCmd.lean index 498360754..fd9c42a2b 100644 --- a/Ix/Cli/ValidateCmd.lean +++ b/Ix/Cli/ValidateCmd.lean @@ -58,8 +58,12 @@ def runValidateCmd (p : Cli.Parsed) : IO UInt32 := do -- `buildFile` also runs `lake exe cache get` if the target depends on -- Mathlib, so large-env validation (`Benchmarks/Compile/CompileMathlib.lean`) - -- works out of the box without a prior `lake build`. - buildFile pathStr + -- works out of the box without a prior `lake build`. Corpus orchestrators + -- can instead prebuild several targets in one authoritative Lake process + -- and pass `--no-build`; this avoids racing concurrent Lake processes over + -- a shared package store while the validators themselves run in parallel. + unless p.hasFlag "no-build" do + buildFile pathStr let fe ← getFileEnvCore pathStr let leanEnv := fe.env @@ -133,6 +137,7 @@ def validateCmd : Cli.Cmd := `[Cli| FLAGS: ns : String; "Comma-separated Lean name prefixes to filter on (e.g. 'Aesop,SetTheory.PGame'). When set, only seeds matching any prefix are validated; transitive deps are pulled in automatically." report : String; "Write a machine-readable JSON report (phase table + pass/fail + counts) to this path. Written on abort paths too." + "no-build"; "Skip the Lake build/cache step. The caller must have already built the input and all of its imports. Intended for orchestrators that prebuild targets once before running validators in parallel." ARGS: path : String; "Path to the Lean source file whose env should be validated." diff --git a/Ix/Meta.lean b/Ix/Meta.lean index e396a6cc0..33b1a75ef 100644 --- a/Ix/Meta.lean +++ b/Ix/Meta.lean @@ -157,7 +157,15 @@ def fetchMathlibCache (cwd : Option FilePath) : IO Unit := do let manifest := root / "lake-manifest.json" let contents ← IO.FS.readFile manifest if contents.contains "leanprover-community/mathlib4" then - let mathlibBuild := root / ".lake" / "packages" / "mathlib" / ".lake" / "build" + let packagesDir := + (Lean.Json.parse contents).toOption + |>.bind (fun json => (json.getObjVal? "packagesDir").toOption) + |>.bind (fun value => value.getStr?.toOption) + |>.map FilePath.mk + |>.getD (".lake" / "packages") + let packagesRoot := + if packagesDir.isAbsolute then packagesDir else root / packagesDir + let mathlibBuild := packagesRoot / "mathlib" / ".lake" / "build" if ← mathlibBuild.pathExists then println! "Mathlib cache already present, skipping fetch." return diff --git a/Tests/Ix/Compile/Mutual.lean b/Tests/Ix/Compile/Mutual.lean index 00fd76988..9fb9deb39 100644 --- a/Tests/Ix/Compile/Mutual.lean +++ b/Tests/Ix/Compile/Mutual.lean @@ -837,6 +837,26 @@ def arWkEqDef := @Ar.wk.eq_def end TypeBrecOnEqDefUnit +-- Indexed `.brecOn.eq` with constructor fields whose dependency sets overlap +-- only after an earlier index substitution. Lean's `substCore` reverts each +-- forward dependency and re-introduces it at the end of the surviving local +-- context. Thus, in `recThenPayload`, substituting `i` first moves the +-- recursive field behind the unaffected `Payload j` field; the subsequent +-- substitution of `j` must see `Payload` before `Indexed`. Preserving the +-- fields' original positions instead produced the Plfl failures +-- `Compositional.Holed.brecOn.eq` and `Inference.TyS.brecOn.eq`. +namespace TypeBrecOnForwardDepOrder + +public inductive Payload : Nat → Type where + | mk {j : Nat} : Payload j + +public inductive Indexed : Nat → Nat → Type where + | base {i : Nat} : Indexed i i + | recThenPayload {i j : Nat} : Indexed i j → Payload j → Indexed i j + | payloadThenRec {i j : Nat} : Payload j → Indexed i j → Indexed i j + +end TypeBrecOnForwardDepOrder + -- Mutual Prop-valued inductive predicates consumed through the raw mutual -- recursor with explicit motives (the PhiConfluence `Par`/`ParB` shape; -- phiconfluence.ixe check-rs failures of 2026-08-22: `parB_domain`, diff --git a/Tests/Ix/TruthMines.lean b/Tests/Ix/TruthMines.lean index 7cc7867a7..c6e0e6abe 100644 --- a/Tests/Ix/TruthMines.lean +++ b/Tests/Ix/TruthMines.lean @@ -24,9 +24,10 @@ * `truthmines-validate` / `truthmines-validate-mini` — the METADATA fidelity rung (Q1): `truthmines validate [--mini]`, the 8-phase `ix validate` pipeline (aux-gen congruence, alpha canonicity, - decompile both ways, per-constant roundtrip) over every member's - driver module. The anon check sweep never touches §4/§5; this leg - is what gates them, per constituent library. + decompile both ways, per-constant roundtrip) over every native + member's driver module, plus Palomar.ix as one aggregate library in + the full tier. The anon check sweep never touches §4/§5; this leg is + what gates them, per validation target. All heavy steps run under the driver's `Ix.Watchdog` ceilings. Needs `lake build ix truthmines` first; network + `lake exe cache get` on @@ -155,7 +156,7 @@ private def driverValidate (mini : Bool) : def validateSuite : List TestSeq := [ .individualIO - "truthmines-validate: 8-phase metadata fidelity over every corpus member" + "truthmines-validate: 8-phase metadata fidelity over every validation target" none (driverValidate false) .done ] def validateMiniSuite : List TestSeq := [ diff --git a/Tests/Ix/TruthMinesRecords.lean b/Tests/Ix/TruthMinesRecords.lean index a65b33b6b..9e6e13793 100644 --- a/Tests/Ix/TruthMinesRecords.lean +++ b/Tests/Ix/TruthMinesRecords.lean @@ -6,9 +6,10 @@ elaboration; re-asserting here reports the errors instead of a build failure when records are edited); * one toolchain by construction: the derived `expectedToolchain` equals - the repo's `lean-toolchain` and the generated workspace's copy; - * the generated workspace files are byte-identical to their projections - (`lake exe truthmines gen --check` as a test); + the repo's `lean-toolchain` and both nested workspaces' copies; + * every generated workspace and per-library compile-driver file is + byte-identical to its projection (`lake exe truthmines gen --check` + as a test); * Lake's lockfile pins every admitted git record at exactly the recorded revision, carries the two local fixtures at their ported paths, and names no direct git package outside the workspace pin set (inherited @@ -41,18 +42,30 @@ private def validationTest : IO (Bool × Nat × Nat × Option String) := do private def toolchainTest : IO (Bool × Nat × Nat × Option String) := do let repo := (← IO.FS.readFile "lean-toolchain").trimAscii.toString let workspace := (← IO.FS.readFile workspaceToolchainPath).trimAscii.toString + let compileWorkspace := + (← IO.FS.readFile compileWorkspaceToolchainPath).trimAscii.toString if repo != expectedToolchain then return check false s!"repo lean-toolchain `{repo}` != derived `{expectedToolchain}`" if workspace != expectedToolchain then return check false s!"workspace lean-toolchain `{workspace}` != derived `{expectedToolchain}`" + if compileWorkspace != expectedToolchain then + return check false + s!"compile workspace lean-toolchain `{compileWorkspace}` != derived `{expectedToolchain}`" return check true "" private def projectionTest : IO (Bool × Nat × Nat × Option String) := do - let expected := [ + let mut expected := [ (workspaceLakefilePath, renderWorkspaceLakefile), - (workspaceToolchainPath, renderWorkspaceToolchain)] + (workspaceToolchainPath, renderWorkspaceToolchain), + (compileWorkspaceLakefilePath, renderCompileWorkspaceLakefile), + (compileWorkspaceToolchainPath, renderWorkspaceToolchain), + (compilePalomarModulePath, renderCompilePalomarModule)] + for lib in driverLibs do + expected := expected ++ [ + (driverModulePath lib.qualifier, renderDriverModule lib), + (compileMemberModulePath lib.qualifier, renderCompileMemberModule lib)] for (path, content) in expected do unless (← path.pathExists) do return check false s!"{path} missing — run `lake exe truthmines gen`" @@ -114,6 +127,49 @@ private def manifestTest : IO (Bool × Nat × Nat × Option String) := do return check errors.isEmpty s!"lockfile/record drift:\n{String.intercalate "\n" errors.toList}" +/-- The independent fidelity workspace shares the canonical package store and + adds exactly one authored source pin: the aggregate Palomar.ix library. -/ +private def compileManifestErrors (content : String) : Except String (Array String) := do + let json ← Lean.Json.parse content + let packagesDir ← (← json.getObjVal? "packagesDir").getStr? + let packages ← (← json.getObjVal? "packages").getArr? + let mut errors := #[] + unless packagesDir == "../../TruthMines/.lake/packages" do + errors := errors.push + s!"compile lockfile packagesDir is `{packagesDir}`" + let mut foundPalomar := false + let mut foundTruthMines := false + for package in packages do + let name := stripGuillemets <| ← (← package.getObjVal? "name").getStr? + if name == "palomar_ix" then + foundPalomar := true + let url ← (← package.getObjVal? "url").getStr? + let rev ← (← package.getObjVal? "rev").getStr? + let inherited ← (← package.getObjVal? "inherited").getBool? + unless url == palomarRepoUrl && rev == palomarRev && !inherited do + errors := errors.push + s!"compile lockfile Palomar pin is `{url}@{rev}` (inherited={inherited})" + if name == "truthmines" then + foundTruthMines := true + let type ← (← package.getObjVal? "type").getStr? + let dir ← (← package.getObjVal? "dir").getStr? + unless type == "path" && dir == "../../TruthMines" do + errors := errors.push + s!"compile lockfile TruthMines source is `{type}:{dir}`" + unless foundPalomar do + errors := errors.push "compile lockfile is missing direct Palomar.ix pin" + unless foundTruthMines do + errors := errors.push "compile lockfile is missing canonical TruthMines path" + return errors + +private def compileManifestTest : IO (Bool × Nat × Nat × Option String) := do + let content ← IO.FS.readFile compileWorkspaceManifestPath + match compileManifestErrors content with + | .error error => return check false s!"compile lockfile walk failed: {error}" + | .ok errors => + return check errors.isEmpty + s!"compile lockfile drift:\n{String.intercalate "\n" errors.toList}" + /-- The positional member vector is what `ix catalog` receives: one `Qualifier=Root[,Root…]` entry per member, parseable by the same splitting the CLI does (`=` once, roots comma-joined, no whitespace or @@ -149,6 +205,8 @@ def suite : List TestSeq := [ none projectionTest .done, .individualIO "truthmines records: lockfile pins match the records" none manifestTest .done, + .individualIO "truthmines records: compile workspace pins are coherent" + none compileManifestTest .done, .individualIO "truthmines records: positional spec argv is well-formed" none specArgvTest .done ] diff --git a/crates/compile/src/compile/aux_gen/brecon.rs b/crates/compile/src/compile/aux_gen/brecon.rs index ebd2b571f..ee9134edb 100644 --- a/crates/compile/src/compile/aux_gen/brecon.rs +++ b/crates/compile/src/compile/aux_gen/brecon.rs @@ -2593,24 +2593,35 @@ fn handle_substcore_step( }) .collect(); - // Build the new local_context for the continuation: replace the - // original forward_deps with their substituted versions (same fvar - // names, substituted domains). Non-dep entries are unchanged. The - // abstracted_fvar is removed (Lean's `clearH := true` clears it). - let new_local_context: Vec = local_context + // Build the new local_context for the continuation. `substCore` reverts + // the abstracted fvar together with every forward dependency, introduces + // the equality pair, and only then re-introduces the remaining reverted + // declarations (`introNP (vars.size - 2)`). Consequently forward deps move + // to the END of the surviving local context; replacing them in place is + // observably wrong when a later substitution depends on both a moved field + // and an unaffected field. For example, after substituting the first index + // of `C : I i j -> T j -> I i j`, `C` moves behind `T`; substituting `j` + // must therefore see the forward deps in `T, C` order, exactly as Lean's + // local context does. + // + // Remove the abstracted fvar and the old forward-dep declarations first, + // preserve every unaffected declaration in place, then append the + // substituted forward deps in their revert order. `clearH := true` also + // removes the abstracted fvar; equality binders are modeled separately by + // `remaining` and never participate in forward-dependency discovery here. + let mut new_local_context: Vec = local_context .iter() .filter_map(|d| { - if d.fvar_name == abstracted_fvar_name { - None - } else if let Some(new_d) = - new_forward_deps.iter().find(|nd| nd.fvar_name == d.fvar_name) + if d.fvar_name == abstracted_fvar_name + || forward_deps.iter().any(|fd| fd.fvar_name == d.fvar_name) { - Some(new_d.clone()) + None } else { Some(d.clone()) } }) .collect(); + new_local_context.extend(new_forward_deps.iter().cloned()); let inner_proof = build_proof_for_remaining( &new_rest,