argumentcomputer · johnchandlerburnham · Aug 25, 2026 · Aug 25, 2026
diff --git a/Benchmarks/Compile/README.md b/Benchmarks/Compile/README.md
@@ -5,12 +5,25 @@ 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/<Qualifier>.lean` fidelity drivers
+- [Palomar.ix](https://github.com/argumentcomputer/Palomar.ix) as one aggregate
+  library (its colliding constituent projects remain in isolated workspaces)
 
 ## Usage
 
 First ensure the Lean version used to build Ix matches the `Benchmarks/Compile/lean-toolchain` version (check against `ix --version`). Then run
 
 `ix compile /path/to/Compile<Lib>.lean` # replace `<Lib>` with `Init`, `InitStd`, `Lean`, `Mathlib`, or `FLT`
 
+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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -0,0 +1,2 @@
+/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
+import Drivers.leansi
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
		import Drivers.A
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
		import Drivers.AddCombi
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
		import Drivers.Aesop
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
		import Drivers.Apportionmentlib
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
		import Drivers.B
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
		import Drivers.BET
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
		import Drivers.Base64
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
		import Drivers.Batteries
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
		import Drivers.BibtexQuery
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		/- GENERATED by `lake exe truthmines gen` from `Benchmarks.TruthMinesSpec`; do not edit. -/
		import Drivers.Bignum