From 3207bf4265ec3000398c82f20e677859e3d3ccd4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 13 Nov 2026 04:14:48 +0000 Subject: [PATCH 1/7] Add CFSG and Stacks cache routing and update to Lean v4.36.0-rc2 --- .github/workflows/cache-restoration.yml | 4 + .github/workflows/ci.yml | 37 ++- .github/workflows/regenerate-main.yml | 20 +- LeanEval/AlgebraicGeometry/Bezout.lean | 4 +- LeanEval/Analysis/FractalUncertainty.lean | 3 +- LeanEval/ConvexGeometry/Ulam.lean | 2 +- LeanEval/Geometry/MostowRigidity.lean | 5 +- LeanEval/KnotTheory/Slice.lean | 2 +- LeanEval/LinearAlgebra/TraceNewton.lean | 2 +- .../ZagierHoffmanPositiveChar.lean | 8 +- LeanEval/RepresentationTheory/SchurWeyl.lean | 4 +- LeanEval/Topology/AnnulusBase.lean | 2 +- LeanEval/Topology/Hurewicz.lean | 2 +- README.md | 37 ++- SECURITY.md | 15 +- lake-manifest.json | 46 ++-- lakefile.toml | 20 +- lean-toolchain | 2 +- scripts/dependency_imports.lean | 25 ++ scripts/fetch_dependency_caches.py | 217 ++++++++++++++++++ scripts/fetch_dependency_caches.sh | 172 +------------- solution-dependencies.json | 28 ++- tests/python/test_fetch_dependency_caches.py | 119 +++++++++- tests/python/test_lake_cache_restore.py | 14 +- 24 files changed, 571 insertions(+), 219 deletions(-) create mode 100644 scripts/dependency_imports.lean create mode 100644 scripts/fetch_dependency_caches.py diff --git a/.github/workflows/cache-restoration.yml b/.github/workflows/cache-restoration.yml index a66fcf1d2..cede9fae0 100644 --- a/.github/workflows/cache-restoration.yml +++ b/.github/workflows/cache-restoration.yml @@ -4,6 +4,8 @@ on: pull_request: paths: - scripts/fetch_dependency_caches.sh + - scripts/fetch_dependency_caches.py + - scripts/dependency_imports.lean - scripts/lake_cache_curl.py - tests/python/test_lake_cache_*.py - tests/python/test_fetch_dependency_caches.py @@ -13,6 +15,8 @@ on: branches: [main] paths: - scripts/fetch_dependency_caches.sh + - scripts/fetch_dependency_caches.py + - scripts/dependency_imports.lean - scripts/lake_cache_curl.py - tests/python/test_lake_cache_*.py - tests/python/test_fetch_dependency_caches.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 771873099..d2c53b6ba 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -18,7 +18,7 @@ jobs: classify: name: Classify changes runs-on: ubuntu-latest - timeout-minutes: 5 + timeout-minutes: 15 outputs: source_changed: ${{ steps.changes.outputs.source_changed }} generated_changed: ${{ steps.changes.outputs.generated_changed }} @@ -29,6 +29,19 @@ jobs: selected_modules: ${{ steps.changes.outputs.selected_modules }} matrix: ${{ steps.changes.outputs.matrix }} steps: + - name: Free up disk space + # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04). + # Bump procedure: SECURITY.md > "Bumping pinned dependencies". + uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be + with: + tool-cache: false + android: true + dotnet: true + haskell: true + large-packages: true + docker-images: true + swap-storage: true + # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30). - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 with: @@ -282,9 +295,12 @@ jobs: test: false lint: false - - name: Fetch TauCeti's build cache - # Problem modules that import TauCeti download its published oleans - # instead of compiling it; see scripts/fetch_dependency_caches.sh. + - name: Fetch imported dependency build caches + env: + STACKS_ARTIFACT_ENDPOINT: ${{ vars.STACKS_ARTIFACT_ENDPOINT }} + STACKS_REVISION_ENDPOINT: ${{ vars.STACKS_REVISION_ENDPOINT }} + # Imported large libraries download their published oleans + # without compiling on a cache miss; see scripts/fetch_dependency_caches.sh. run: bash scripts/fetch_dependency_caches.sh --restore . - name: Clear cached problem-module artifacts @@ -378,6 +394,19 @@ jobs: runs-on: ubuntu-latest timeout-minutes: 15 steps: + - name: Free up disk space + # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04). + # Bump procedure: SECURITY.md > "Bumping pinned dependencies". + uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be + with: + tool-cache: false + android: true + dotnet: true + haskell: true + large-packages: true + docker-images: true + swap-storage: true + # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30). - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 with: diff --git a/.github/workflows/regenerate-main.yml b/.github/workflows/regenerate-main.yml index ef5678a2d..e0d14ef2c 100644 --- a/.github/workflows/regenerate-main.yml +++ b/.github/workflows/regenerate-main.yml @@ -27,6 +27,19 @@ jobs: regenerate: runs-on: ubuntu-latest steps: + - name: Free up disk space + # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04). + # Bump procedure: SECURITY.md > "Bumping pinned dependencies". + uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be + with: + tool-cache: false + android: true + dotnet: true + haskell: true + large-packages: true + docker-images: true + swap-storage: true + # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30). - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 with: @@ -47,6 +60,9 @@ jobs: lint: false - name: Regenerate against a stable main + env: + STACKS_ARTIFACT_ENDPOINT: ${{ vars.STACKS_ARTIFACT_ENDPOINT }} + STACKS_REVISION_ENDPOINT: ${{ vars.STACKS_REVISION_ENDPOINT }} # A merge can land during the hour-long full-catalog generation. Repeat # from the new main instead of rebasing stale generated output over it. # Three attempts bound runner use during an unusually busy merge burst. @@ -57,8 +73,8 @@ jobs: git fetch origin main git reset --hard origin/main git clean -ffd generated/ - # Problem modules that import TauCeti restore its published oleans - # instead of compiling it, at the pins of this checkout; see + # Imported large libraries restore their published oleans + # without compiling on a cache miss, at the pins of this checkout; see # scripts/fetch_dependency_caches.sh. # Check out the dependencies this revision pins before comparing # them, and drop the previous attempt's cache settings. diff --git a/LeanEval/AlgebraicGeometry/Bezout.lean b/LeanEval/AlgebraicGeometry/Bezout.lean index 606701a0f..06ef53780 100644 --- a/LeanEval/AlgebraicGeometry/Bezout.lean +++ b/LeanEval/AlgebraicGeometry/Bezout.lean @@ -43,11 +43,11 @@ def vanishingSet {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) : /-- A chosen index `i : Fin (n+1)` with `p.rep i ≠ 0`. -/ noncomputable def chartIndex {n : ℕ} (p : ProjSpace K n) : Fin (n + 1) := - Classical.choose (Function.ne_iff.mp p.rep_nonzero) + Classical.choose (Function.ne_iff.mp p.rep_ne_zero) lemma chartIndex_rep_ne_zero {n : ℕ} (p : ProjSpace K n) : Projectivization.rep p (chartIndex p) ≠ 0 := - Classical.choose_spec (Function.ne_iff.mp p.rep_nonzero) + Classical.choose_spec (Function.ne_iff.mp p.rep_ne_zero) /-- Affine cone coordinates of `p` on the chart `X_{chartIndex p} = 1`. -/ noncomputable def affineConeCoord {n : ℕ} (p : ProjSpace K n) : diff --git a/LeanEval/Analysis/FractalUncertainty.lean b/LeanEval/Analysis/FractalUncertainty.lean index 019cc5827..932067f09 100644 --- a/LeanEval/Analysis/FractalUncertainty.lean +++ b/LeanEval/Analysis/FractalUncertainty.lean @@ -38,7 +38,8 @@ def PorousOnLines (ν α₀ α₁ : ℝ) (X : Set ℝᵈ) : Prop := ∃ x ∈ segment ℝ y₁ y₂, closedBall x (ν * R) ∩ X = ∅ /-- Given `a b : ℝ`, the cube `[a,b]ᵈ` in `ℝᵈ`. -/ -abbrev cube (a b : ℝ) : Set ℝᵈ := EuclideanSpace.equiv (Fin d) ℝ ⁻¹' Set.univ.pi fun _ ↦ Set.Icc a b +noncomputable abbrev cube (a b : ℝ) : Set ℝᵈ := + EuclideanSpace.equiv (Fin d) ℝ ⁻¹' Set.univ.pi fun _ ↦ Set.Icc a b /-- Statement of Theorem 1.1: diff --git a/LeanEval/ConvexGeometry/Ulam.lean b/LeanEval/ConvexGeometry/Ulam.lean index 7f4338e0c..6e94635d5 100644 --- a/LeanEval/ConvexGeometry/Ulam.lean +++ b/LeanEval/ConvexGeometry/Ulam.lean @@ -31,7 +31,7 @@ local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d) variable (d) in /-- The unit sphere in `ℝᵈ`, centered at the origin. This is denoted `Sᵈ⁻¹` in the paper. -/ -abbrev S : Set ℝᵈ := Metric.sphere 0 1 +noncomputable abbrev S : Set ℝᵈ := Metric.sphere 0 1 /-- A subset `K ⊆ ℝᵈ` is called origin-symmetric if `K = -K`. -/ abbrev IsOriginSymmetric (K : Set ℝᵈ) : Prop := diff --git a/LeanEval/Geometry/MostowRigidity.lean b/LeanEval/Geometry/MostowRigidity.lean index dd31f3a60..11bf18b90 100644 --- a/LeanEval/Geometry/MostowRigidity.lean +++ b/LeanEval/Geometry/MostowRigidity.lean @@ -87,7 +87,10 @@ instance [Star α] [ContinuousStar α] : IsTopologicalRing (MatrixSum p q α) := variable [StarRing α] [ContinuousStar α] instance : ContinuousStar (MatrixSum p q α) where - continuous_star := by rw [star]; fun_prop + continuous_star := by + change Continuous (fun A : MatrixSum p q α => + MatrixSum.ofMatrix (pmOneMat * (MatrixSum.ofMatrix.symm A).conjTranspose * pmOneMat)) + fun_prop theorem MatrixSum.isClosed_unitary [T1Space α] : IsClosed (SetLike.coe <| unitary (MatrixSum p q α)) := diff --git a/LeanEval/KnotTheory/Slice.lean b/LeanEval/KnotTheory/Slice.lean index 7f32373a0..9e04eea86 100644 --- a/LeanEval/KnotTheory/Slice.lean +++ b/LeanEval/KnotTheory/Slice.lean @@ -178,7 +178,7 @@ structure PLKnot where three_le : 3 ≤ vertices.length /-- The image of the PL knot in `ℝ³` (the trace of the polyline). -/ -def PLKnot.image (K : PLKnot) : Set R3 := +noncomputable def PLKnot.image (K : PLKnot) : Set R3 := plCurve K.vertices '' Set.Ico (0 : ℝ) (K.vertices.length : ℝ) /-- The polyline is a *simple closed curve*: the periodic parametrization is diff --git a/LeanEval/LinearAlgebra/TraceNewton.lean b/LeanEval/LinearAlgebra/TraceNewton.lean index 2cec2b8fe..7d89f7fd7 100644 --- a/LeanEval/LinearAlgebra/TraceNewton.lean +++ b/LeanEval/LinearAlgebra/TraceNewton.lean @@ -28,7 +28,7 @@ stated uniformly for all positive `k`. -/ noncomputable def charpolyDescendingCoeff {R : Type*} [CommRing R] (A : Matrix n n R) (k : ℕ) : R := if k ≤ Fintype.card n then - Polynomial.coeff A.charpoly (Fintype.card n - k) + A.charpoly.coeff (Fintype.card n - k) else 0 diff --git a/LeanEval/NumberTheory/ZagierHoffmanPositiveChar.lean b/LeanEval/NumberTheory/ZagierHoffmanPositiveChar.lean index c2aea8f13..cdc2d8616 100644 --- a/LeanEval/NumberTheory/ZagierHoffmanPositiveChar.lean +++ b/LeanEval/NumberTheory/ZagierHoffmanPositiveChar.lean @@ -52,25 +52,25 @@ noncomputable def 𝒵 (w : ℕ) : Submodule (RatFunc F) (CompletionAtInfty F) : /-- Let `q` be the size of the finite field `F`. `𝒯_aux w r` is the set of `ζ_A(s_1, ..., s_r)` of weight `w`, with `1 ≤ s_i ≤ q` for `1 ≤ i ≤ r − 1` and `1 ≤ s_r < q`. -/ -def 𝒯_aux (w : ℕ) (r : ℕ+) : Set (CompletionAtInfty F) := +noncomputable def 𝒯_aux (w : ℕ) (r : ℕ+) : Set (CompletionAtInfty F) := let q := Nat.card F let 𝔖'_w := {𝔰 ∈ 𝔖_w w r | (∀ i : Fin r, i < (r - 1 : ℕ) → 𝔰 i ≤ q) ∧ 𝔰 ⟨r - 1, by simp⟩ < q} {ζ_A F s | s ∈ 𝔖'_w} /-- Let `q` be the size of the finite field `F`. `𝒯_w` is the set of `ζ_A(s_1,..., s_r)` of weight `w`, with `1 ≤ s_i ≤ q` for `1 ≤ i ≤ r − 1` and `1 ≤ s_r < q`, as `r` varies. -/ -def 𝒯 (w : ℕ) : Set (CompletionAtInfty F) := ⋃ r : ℕ+, 𝒯_aux F w r +noncomputable def 𝒯 (w : ℕ) : Set (CompletionAtInfty F) := ⋃ r : ℕ+, 𝒯_aux F w r /-- Let `q` be the size of the finite field `F`. `𝒯0_aux` is the set of `ζ_A(s_1,..., s_r)` of weight `w`, with `1 ≤ s_i < q` for all `i`. -/ -def 𝒯0_aux (w : ℕ) (r : ℕ+) : Set (CompletionAtInfty F) := +noncomputable def 𝒯0_aux (w : ℕ) (r : ℕ+) : Set (CompletionAtInfty F) := let q := Nat.card F let 𝔖'_w := {𝔰 ∈ 𝔖_w w r | ∀ i, 𝔰 i < q} {ζ_A F s | s ∈ 𝔖'_w} /-- Let `q` be the size of the finite field `F`. `𝒯0 w` is the set of `ζ_A(s_1,..., s_r)` of weight `w`, with `1 ≤ s_i < q` for all `i`, as `r` varies. -/ -def 𝒯0 (w : ℕ) : Set (CompletionAtInfty F) := ⋃ r : ℕ+, 𝒯0_aux F w r +noncomputable def 𝒯0 (w : ℕ) : Set (CompletionAtInfty F) := ⋃ r : ℕ+, 𝒯0_aux F w r /-- The sequence `d(w)` from Conjecture 1.5 and Theorems A and D. -/ noncomputable def d (w : ℕ) : ℕ := diff --git a/LeanEval/RepresentationTheory/SchurWeyl.lean b/LeanEval/RepresentationTheory/SchurWeyl.lean index b2aa47e83..e648b850b 100644 --- a/LeanEval/RepresentationTheory/SchurWeyl.lean +++ b/LeanEval/RepresentationTheory/SchurWeyl.lean @@ -29,11 +29,11 @@ def symAction (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] (k : map_one' := by ext x simp only [LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, Function.comp_apply, - PiTensorProduct.reindex_tprod, Module.End.one_apply] + PiTensorProduct.reindex_tprod, one_apply_eq_self] rfl map_mul' σ τ := by ext x - simp only [Module.End.mul_apply, LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, + simp only [mul_apply_eq_comp, LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, Function.comp_apply, PiTensorProduct.reindex_tprod] rfl diff --git a/LeanEval/Topology/AnnulusBase.lean b/LeanEval/Topology/AnnulusBase.lean index 0ee95c9b1..ed5167f23 100644 --- a/LeanEval/Topology/AnnulusBase.lean +++ b/LeanEval/Topology/AnnulusBase.lean @@ -52,7 +52,7 @@ embedding, and nothing of Kirby's torus trick or Quinn's 4-dimensional work. abbrev Amb (n : ℕ) : Type := EuclideanSpace ℝ (Fin n) /-- The unit `(n-1)`-sphere `Sⁿ⁻¹ ⊂ ℝⁿ`. -/ -abbrev Sph (n : ℕ) : Set (Amb n) := sphere (0 : Amb n) 1 +noncomputable abbrev Sph (n : ℕ) : Set (Amb n) := sphere (0 : Amb n) 1 /-- The model hyperplane `{x | x₀ = 0}` in `ℝⁿ`, the local model for a flatly embedded sphere. -/ diff --git a/LeanEval/Topology/Hurewicz.lean b/LeanEval/Topology/Hurewicz.lean index 42eded5d4..90c0c1367 100644 --- a/LeanEval/Topology/Hurewicz.lean +++ b/LeanEval/Topology/Hurewicz.lean @@ -25,7 +25,7 @@ abelianization of `π₁(X, x)`. -/ @[eval_problem] theorem hurewicz_h1_abelianization (X : Type) [TopologicalSpace X] [PathConnectedSpace X] (x : X) : - Nonempty (Additive (Abelianization (FundamentalGroup X x)) ≃+ + Nonempty (Additive (Group.Abelianization (FundamentalGroup X x)) ≃+ (IntegralHomology 1 X : Type)) := by sorry diff --git a/README.md b/README.md index 561b4262e..344444c62 100644 --- a/README.md +++ b/README.md @@ -206,11 +206,34 @@ Trusted files you should not edit in the normal solver workflow are: `Challenge.lean` contains the benchmark statement. `Solution.lean` is the fixed bridge that tells comparator to check your theorem from the `Submission` namespace. -Solutions may import `LeanPool.*` modules from [Lean Pool](https://github.com/Vilin97/lean-pool) -in `Submission.lean` or `Submission/` helpers. The pinned dependency is included in -all generated workspaces via `solution-dependencies.json`. Problem statements and -their local helpers may not import it; workspace generation rejects these imports. -Comparator and nanoda checks apply as usual. +Solutions may import modules from [Lean Pool](https://github.com/Vilin97/lean-pool), +[CFSG](https://github.com/AxiomMath/CFSG), and +[Stacks](https://github.com/AxiomMath/Stacks) in `Submission.lean` or `Submission/` +helpers. These pinned dependencies are included in generated workspaces via +`solution-dependencies.json`. Problem statements and their local helpers may not +import them; workspace generation rejects these imports. Comparator and NanoDa +checks apply as usual. + +After fetching the workspace dependencies, prepare the libraries it imports: + +```bash +cache_env="$(bash /path/to/lean-eval/scripts/fetch_dependency_caches.sh --restore .)" && eval "$cache_env" +``` + +This parses Lean import headers, fetches each required library's revision mappings, +and restores only the imported modules and their transitive dependencies. It uses +`lake --no-build`, so missing artifacts fail rather than starting a large rebuild. +Each library must match the workspace's Lean toolchain and all transitive dependency +pins. Unused libraries require no artifact downloads. + +LeanEval currently uses Lean **v4.36.0-rc2**. The public CFSG pin still uses +v4.35.0-rc3, and the public Stacks pin uses v4.35.0. Their imports will fail the +cache compatibility check until matching upstream builds are published. CFSG's +published cache URLs are configured in the helper. Stacks' public README does not +yet give cache URLs; set `STACKS_ARTIFACT_ENDPOINT` and `STACKS_REVISION_ENDPOINT` +when preparing a compatible Stacks checkout. Endpoint overrides are also available +as `CFSG_*` and `TAUCETI_*`. CI and the submission runner read the Stacks URLs +from repository variables with those same names. ### 5. Run comparator locally @@ -352,8 +375,8 @@ In practice, solvers should normally work in `Submission.lean` and `Submission/` ## End-To-End Repo Checks -`bash scripts/fetch_dependency_caches.sh --restore .` restores imported TauCeti -modules without permitting compilation. Downloads have bounded retries and +`bash scripts/fetch_dependency_caches.sh --restore .` restores imported TauCeti, +CFSG, and Stacks modules without permitting compilation. Downloads have bounded retries and timeouts and use temporary files to keep interrupted transfers out of the artifact cache. Cache-only restoration is retried once; if it still fails, the script prints verbose diagnostics before stopping. Verify the pinned versions diff --git a/SECURITY.md b/SECURITY.md index c05654915..9bc3bd6be 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -92,9 +92,12 @@ an empty environment. It preserves Lake's other arguments and settings. Mounts come from trusted root state, never submission input. Private local workspaces do not need this visibility adapter. -Existing trusted root builds finish dependency setup before evaluation, including -ProofWidgets metadata that cannot be updated in a read-only cache. Shared source -and cached artifacts remain read-only during submission builds. The submissions +Trusted root builds prepare dependencies before evaluation, including ProofWidgets +metadata that cannot be updated in a read-only cache. After overlaying solver files, +the submissions adapter can restore additional publisher artifacts selected by +registered library imports and pinned cache mappings. It parses headers without +elaborating solver code and permits no compilation during restoration. Shared +source and cached artifacts remain read-only during submission builds. The submissions adapter gives Lean Pool its own writable build outputs in each workspace while sharing its pinned source read-only; one submission must never supply writable artifacts to another. @@ -119,8 +122,10 @@ in both benchmark and submission installers. Review the actual sandbox behavior, not just the reported version. No standalone comparator/exporter/NanoDa build or Landrun pin is required by this benchmark. -The generator rejects Lean Pool imports in trusted statements and helpers while -making its pinned source available to solutions. Maintain that separation. +The generator rejects Lean Pool, CFSG, and Stacks imports in trusted statements +and helpers while making their pinned source available to solutions. Cache +preparation parses submission headers without elaborating them and restores only +registered library targets with `lake --no-build`. Maintain that separation. Historical replay locks and instrumentation are versioned independently; do not silently change their verifier or metric semantics. diff --git a/lake-manifest.json b/lake-manifest.json index be874ffb4..50817ff4e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,20 +15,40 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b63f6e8a68d220e3b3bc4f3792bb53650d375f24", + "rev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "b63f6e8a68d220e3b3bc4f3792bb53650d375f24", + "inputRev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/TauCetiProject/TauCeti", "type": "git", "subDir": null, "scope": "", - "rev": "6e0c6acab5f4c6f42e5f5bab9bd5e4e84f74c380", + "rev": "be86813dc92e6bac8614c2c2dd34572145df09c0", "name": "TauCeti", "manifestFile": "lake-manifest.json", - "inputRev": "6e0c6acab5f4c6f42e5f5bab9bd5e4e84f74c380", + "inputRev": "be86813dc92e6bac8614c2c2dd34572145df09c0", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/AxiomMath/Stacks.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c496df0d9beea9deaeabcea8492605f9a0a2313b", + "name": "Stacks", + "manifestFile": "lake-manifest.json", + "inputRev": "c496df0d9beea9deaeabcea8492605f9a0a2313b", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/AxiomMath/CFSG.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33", + "name": "cfsg", + "manifestFile": "lake-manifest.json", + "inputRev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/Vilin97/lean-pool.git", @@ -45,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b", + "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3", + "rev": "c61286b7b63cbfd563b28e11e81d0a18233a044a", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "10a2cfff285e1c7c2ebc49c0ba22cab0f3c58ee5", + "rev": "e5d5639bedc7feecfbcb98e30b3bf26463d9f722", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1", + "rev": "16259c0d07d61ee37d999d05b5cf96338b8daa11", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +105,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea", + "rev": "7d11bfa88558f8d3d90afdf6bd877ed70001498d", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +115,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9", + "rev": "b0256621cb88178e9ad932a53633077b3029e621", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -105,7 +125,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "33131f4fb10067cb3009bf4db615d9680c1ccd6b", + "rev": "4af7237d146261353907b06a01b6f3fc06cfa067", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,10 +135,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", + "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.35.0-rc3", + "inputRev": "v4.36.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "«lean-eval»", diff --git a/lakefile.toml b/lakefile.toml index b54b07d77..5e17c52ac 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,5 +1,7 @@ name = "lean-eval" defaultTargets = ["LeanEval"] +# Generated benchmark statements retain legacy visibility rules. +allowNonModules = true [leanOptions] autoImplicit = false @@ -11,6 +13,20 @@ name = "lean-pool" git = "https://github.com/Vilin97/lean-pool.git" rev = "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f" +# Large solution libraries. Their caches are fetched only when imported. +# Keep these before TauCeti and Mathlib so the benchmark owns shared pins. +# Their published pins currently predate this toolchain; cache preparation +# rejects imports until the publishers provide matching builds (see README). +[[require]] +name = "cfsg" +git = "https://github.com/AxiomMath/CFSG.git" +rev = "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33" + +[[require]] +name = "Stacks" +git = "https://github.com/AxiomMath/Stacks.git" +rev = "c496df0d9beea9deaeabcea8492605f9a0a2313b" + # TauCeti supplies the definitions in the classification of finite simple groups # problem. It is listed before Mathlib because Lake takes shared transitive # dependencies (batteries, aesop, ...) from the later require, and those must be @@ -20,12 +36,12 @@ rev = "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f" [[require]] name = "TauCeti" git = "https://github.com/TauCetiProject/TauCeti" -rev = "6e0c6acab5f4c6f42e5f5bab9bd5e4e84f74c380" +rev = "be86813dc92e6bac8614c2c2dd34572145df09c0" [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "b63f6e8a68d220e3b3bc4f3792bb53650d375f24" +rev = "2ddf59c8f14245864e6c0ed227a2dab76b9efea2" [[require]] name = "lean-eval-generator" diff --git a/lean-toolchain b/lean-toolchain index f0e00b333..0fc433692 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.35.0-rc3 +leanprover/lean4:v4.36.0-rc2 diff --git a/scripts/dependency_imports.lean b/scripts/dependency_imports.lean new file mode 100644 index 000000000..08d3a8a85 --- /dev/null +++ b/scripts/dependency_imports.lean @@ -0,0 +1,25 @@ +import Lean + +/- Parse headers without loading the imported libraries or running submission code. -/ +def main (args : List String) : IO Unit := do + let [pathsFile] := args + | throw <| IO.userError "usage: dependency_imports.lean " + let paths ← IO.ofExcept <| + (Lean.Json.parse (← IO.FS.readFile pathsFile)).bind (Lean.fromJson? (α := Array String)) + let mut imports : Array (String × Array String) := #[] + for path in paths do + let (header, _, messages) ← Lean.Elab.parseImports (← IO.FS.readFile path) path + if messages.hasErrors then + -- Comparator reports malformed solver headers as ordinary proof failures. + IO.eprintln s!"Skipping malformed import header in {path}; the Lean build will report it" + continue + for imp in header do + let name := imp.module.toString + unless imports.any (·.1 == name) do + let parts := imp.module.components.toArray.map fun component => + match component with + | .str _ s => s + | .num _ n => toString n + | .anonymous => "" + imports := imports.push (name, parts) + IO.println <| Lean.Json.compress <| Lean.toJson imports diff --git a/scripts/fetch_dependency_caches.py b/scripts/fetch_dependency_caches.py new file mode 100644 index 000000000..e0121f5aa --- /dev/null +++ b/scripts/fetch_dependency_caches.py @@ -0,0 +1,217 @@ +#!/usr/bin/env python3 +"""Restore published Lake artifacts for the large libraries a project imports.""" +from __future__ import annotations + +import argparse +from dataclasses import dataclass +import json +import os +from pathlib import Path +import re +import shlex +import subprocess +import sys +import tempfile +import time + + +SCRIPTS = Path(__file__).resolve().parent + + +@dataclass(frozen=True) +class Library: + package: str + repo: str + roots: tuple[str, ...] + prefix: str + endpoint: str = "" + + +LIBRARIES = ( + Library("TauCeti", "TauCetiProject/TauCeti", ("TauCeti",), "TAUCETI", + "https://cache.taucetiproject.org"), + Library("cfsg", "AxiomMath/CFSG", ("CFSG", "CFSGWithCertificates", "Certificates", "Comparator"), + "CFSG", "https://cfsg-downloads.axiommath.workers.dev/lake"), + # Supply STACKS_ARTIFACT_ENDPOINT and STACKS_REVISION_ENDPOINT until the + # publisher confirms its public URLs. Never guess a cache's provenance. + Library("Stacks", "AxiomMath/Stacks", ("Stacks", "StacksCore", "StacksFrontier"), "STACKS"), +) + + +def manifest(path: Path) -> dict[str, dict]: + data = json.loads(path.read_text(encoding="utf-8")) + return {p["name"].strip("«»"): p for p in data["packages"]} + + +def imported_modules(project: Path) -> dict[str, list[str]]: + paths = [] + + def unreadable(error: OSError) -> None: + raise error + + for directory, subdirs, files in os.walk(project, onerror=unreadable): + subdirs[:] = sorted(d for d in subdirs if d not in {".lake", ".git"}) + paths.extend(str(Path(directory) / f) for f in sorted(files) if f.endswith(".lean")) + with tempfile.TemporaryDirectory(prefix="lean-eval-imports-") as temporary: + source_list = Path(temporary) / "paths.json" + source_list.write_text(json.dumps(paths), encoding="utf-8") + result = subprocess.run( + ["lean", "--run", str(SCRIPTS / "dependency_imports.lean"), str(source_list)], + cwd=project, text=True, capture_output=True, check=False, + ) + if result.returncode: + raise RuntimeError(f"could not parse project imports:\n{result.stdout}{result.stderr}") + if result.stderr: + print(result.stderr, file=sys.stderr, end="") + return dict(json.loads(result.stdout)) + + +def belongs(module: str, library: Library) -> bool: + return any(module == root or module.startswith(root + ".") for root in library.roots) + + +def retry(command: list[str], project: Path, env: dict[str, str], attempts: int) -> str: + for attempt in range(1, attempts + 1): + # Buffer only the diagnostics, not downloaded artifacts. Keep stdout + # reserved for the export line the shell caller evaluates. + result = subprocess.run(command, cwd=project, env=env, text=True, + stdout=subprocess.PIPE, stderr=subprocess.STDOUT, check=False) + if result.returncode == 0: + return result.stdout + print(result.stdout, file=sys.stderr, end="") + if attempt < attempts: + print(f"::notice::dependency cache operation failed (attempt {attempt} of {attempts}); retrying", + file=sys.stderr) + time.sleep(5) + raise RuntimeError("dependency cache restoration failed after bounded retries; no compilation " + "was permitted. Check the pins and published cache coverage.") + + +def prepare(project: Path, restore: bool) -> dict[str, str]: + packages = manifest(project / "lake-manifest.json") + available = [lib for lib in LIBRARIES if lib.package in packages] + if not available: + print("fetch_dependency_caches: no supported packages in the manifest; nothing to fetch", + file=sys.stderr) + return {} + modules = imported_modules(project) + for module, parts in list(modules.items()): + library = next((lib for lib in available if belongs(module, lib)), None) + if library is None: + continue + directory = project / ".lake/packages" / library.package + # Invalid/missing solver imports belong to comparator's verdict, not + # an infrastructure failure for every problem in the submission. + # Restrict CLI targets as well: quoted components can contain path + # separators or dots, which Lake's target parser treats differently. + plain = module == ".".join(parts) and all( + part and all(c.isalnum() or c in "_'" for c in part) for part in parts) + source = directory.joinpath(*parts[:-1], parts[-1] + ".lean") + if not plain or ((directory / "lake-manifest.json").is_file() and not source.is_file()): + print(f"fetch_dependency_caches: leaving unresolved import {module} to comparator", + file=sys.stderr) + del modules[module] + needed = [lib for lib in available if any(belongs(m, lib) for m in modules)] + # CFSG's artifacts depend on TauCeti, even if the submission does not import + # TauCeti directly. Register every supported transitive cache as well. + directories = {} + index = 0 + while index < len(needed): + library = needed[index] + index += 1 + directory = project / ".lake/packages" / library.package + if not (directory / "lake-manifest.json").is_file(): + raise RuntimeError(f"{directory} is not checked out; fetch the dependencies first") + directories[library.package] = directory + dependencies = manifest(directory / "lake-manifest.json") + for other in available: + if other.package in dependencies and other not in needed: + needed.append(other) + if not needed: + print("fetch_dependency_caches: no supported library imports; nothing to fetch", file=sys.stderr) + return {} + + toolchain = (project / "lean-toolchain").read_text().strip() + services = [] + # Validate every library before fetching anything: a different transitive + # pin changes build traces just as a different Mathlib pin does. + for library in needed: + directory = directories[library.package] + their_toolchain = (directory / "lean-toolchain").read_text().strip() + dependencies = manifest(directory / "lake-manifest.json") + mismatches = [name for name, dep in dependencies.items() + if name not in packages or packages[name].get("rev") != dep.get("rev")] + if toolchain != their_toolchain or mismatches: + raise RuntimeError( + f"{library.package} {packages[library.package]['rev']} was built with {their_toolchain}; " + f"this project pins {toolchain}. Different dependency pins: {', '.join(mismatches) or 'none'}. " + "Pin the same toolchain and Mathlib (and other transitive dependencies) as the library " + "commit so its build cache applies.") + artifacts = os.environ.get(f"{library.prefix}_ARTIFACT_ENDPOINT", + f"{library.endpoint}/artifacts" if library.endpoint else "") + revisions = os.environ.get(f"{library.prefix}_REVISION_ENDPOINT", + f"{library.endpoint}/revisions" if library.endpoint else "") + if not artifacts or not revisions: + raise RuntimeError(f"set {library.prefix}_ARTIFACT_ENDPOINT and " + f"{library.prefix}_REVISION_ENDPOINT to the publisher's public cache URLs") + services.append((library, artifacts, revisions)) + + descriptor, config_name = tempfile.mkstemp( + prefix="lean-eval-dependency-cache.", dir=os.environ.get("RUNNER_TEMP") or None) + config = Path(config_name) + try: + with os.fdopen(descriptor, "w", encoding="utf-8") as output: + for library, artifacts, revisions in services: + # JSON strings are valid TOML basic strings. Each fetched + # mapping records its service, so multiple caches coexist. + output.write('[[cache.service]]\n') + output.write(f'name = "{library.prefix.lower()}-public"\nkind = "s3"\n') + output.write(f"artifactEndpoint = {json.dumps(artifacts)}\n") + output.write(f"revisionEndpoint = {json.dumps(revisions)}\n") + settings = {"LAKE_CONFIG": str(config), "LAKE_ARTIFACT_CACHE": "true", + "CURL": str(SCRIPTS / "lake_cache_curl.py")} + env = dict(os.environ, **settings, LAKE_RESTORE_ARTIFACTS="true") + for library, _, _ in services: + retry(["lake", "-v", "cache", "get", "--service", f"{library.prefix.lower()}-public", + "--repo", library.repo, "--package", library.package, + "--rev", packages[library.package]["rev"], "--mappings-only"], project, env, 3) + if restore: + targets = sorted({m for m in modules if any(belongs(m, lib) for lib in needed)}) + print(f"fetch_dependency_caches: restoring {len(targets)} imported library module(s) " + "and their dependencies", file=sys.stderr) + # `+` selects a module even when a library has the same name; + # a bare name could otherwise restore every module of that library. + log = retry(["lake", "-v", "--no-build", "build", *("+" + m for m in targets)], + project, env, 2) + roots = "|".join(re.escape(root) for lib in needed for root in lib.roots) + if re.search(rf"Built (?:{roots})(?:[.\s]|$)", log): + raise RuntimeError("a dependency module was compiled instead of downloaded:\n" + log) + return settings + except BaseException: + config.unlink(missing_ok=True) + raise + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--restore", action="store_true") + parser.add_argument("project", type=Path) + args = parser.parse_args() + try: + settings = prepare(args.project.resolve(), args.restore) + if settings: + if github_env := os.environ.get("GITHUB_ENV"): + with open(github_env, "a", encoding="utf-8") as output: + for name, value in settings.items(): + output.write(f"{name}={value}\n") + else: + print("export " + " ".join(f"{name}={shlex.quote(value)}" + for name, value in settings.items())) + return 0 + except (OSError, ValueError, RuntimeError) as error: + print(f"::error::fetch_dependency_caches: {error}", file=sys.stderr) + return 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/fetch_dependency_caches.sh b/scripts/fetch_dependency_caches.sh index 0a1462719..1519b27bd 100644 --- a/scripts/fetch_dependency_caches.sh +++ b/scripts/fetch_dependency_caches.sh @@ -1,166 +1,12 @@ #!/usr/bin/env bash -# Prepare a lean-eval checkout (or a project that reuses its dependencies) to download TauCeti's -# build outputs instead of compiling TauCeti. -# # Usage: bash scripts/fetch_dependency_caches.sh [--restore] -# -# TauCeti publishes the oleans of every main commit to a public Lake artifact cache. Lake only -# reuses them if TauCeti is built here exactly as TauCeti's CI built it, so this script first -# checks that the project pins the same Lean toolchain and Mathlib revision as the pinned TauCeti -# commit, and fails if not. It then downloads the (small) input-to-output mappings for the -# pinned TauCeti revision and writes a Lake configuration naming TauCeti's cache service. Builds -# that run with LAKE_CONFIG pointing at that file and LAKE_ARTIFACT_CACHE=true fetch the TauCeti -# artifacts they need. -# -# With --restore, the script also builds every TauCeti module that a `.lean` file of the project -# imports, restoring the downloaded outputs into TauCeti's build directory. --no-build prevents -# compilation on a cache miss. Verbose diagnostics retain artifact errors; a curl wrapper adds -# bounded retries and publishes downloads atomically so interrupted transfers cannot poison -# later cache attempts. -# Later builds then find those modules up to date even without the cache settings. -# -# Under GitHub Actions the cache and curl settings are appended to $GITHUB_ENV. Otherwise, -# when GITHUB_ENV is unset or empty, stdout is a single `export` line for the caller: -# -# cache_env="$(bash scripts/fetch_dependency_caches.sh .)" && eval "$cache_env" -# -# (Assign first: `eval "$(...)"` would hide a failure of the script.) -# -# A project whose manifest has no TauCeti package needs nothing, and the script exits cleanly. -# The dependencies must already be checked out (for example by `lake exe cache get`). +# Dependencies must already be checked out (e.g. by `lake exe cache get`). +# --restore downloads imported library modules and their dependencies with +# `lake --no-build`, refusing to compile on a cache miss. Without --restore, +# fetch only revision mappings. See README.md for supported public libraries. +# +# In GitHub Actions, settings are appended to GITHUB_ENV. Otherwise stdout is +# one shell export line, suitable for: +# cache_env="$(bash scripts/fetch_dependency_caches.sh --restore .)" && eval "$cache_env" set -euo pipefail -# Stdout carries only the final `export` line, so it can be passed to `eval`. -exec 3>&1 1>&2 - -RESTORE=0 -if [ "${1:-}" = "--restore" ]; then - RESTORE=1 - shift -fi -PROJECT_DIR="$(cd "${1:?usage: fetch_dependency_caches.sh [--restore] }" && pwd)" -CACHE_CURL="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)/lake_cache_curl.py" -ARTIFACT_ENDPOINT="${TAUCETI_ARTIFACT_ENDPOINT:-https://cache.taucetiproject.org/artifacts}" -REVISION_ENDPOINT="${TAUCETI_REVISION_ENDPOINT:-https://cache.taucetiproject.org/revisions}" - -manifest_rev() { - # manifest_rev : the pinned rev, or nothing. - python3 - "$1" "$2" <<'PY' -import json, sys -with open(sys.argv[1], encoding="utf-8") as f: - packages = json.load(f)["packages"] -print(next((p["rev"] for p in packages if p["name"] == sys.argv[2]), "")) -PY -} - -TAUCETI_REV="$(manifest_rev "$PROJECT_DIR/lake-manifest.json" TauCeti)" -if [ -z "$TAUCETI_REV" ]; then - echo "fetch_dependency_caches: no TauCeti package in the manifest; nothing to fetch" - exit 0 -fi - -TAUCETI_DIR="$PROJECT_DIR/.lake/packages/TauCeti" -if [ ! -f "$TAUCETI_DIR/lake-manifest.json" ]; then - echo "::error::fetch_dependency_caches: $TAUCETI_DIR is not checked out; fetch the dependencies first" - exit 1 -fi - -# TauCeti's published outputs are keyed by the toolchain and by the traces of the Mathlib it was -# built against, so any difference here turns every lookup into a miss and a full rebuild. -ours_toolchain="$(tr -d '[:space:]' < "$PROJECT_DIR/lean-toolchain")" -their_toolchain="$(tr -d '[:space:]' < "$TAUCETI_DIR/lean-toolchain")" -ours_mathlib="$(manifest_rev "$PROJECT_DIR/lake-manifest.json" mathlib)" -their_mathlib="$(manifest_rev "$TAUCETI_DIR/lake-manifest.json" mathlib)" -if [ "$ours_toolchain" != "$their_toolchain" ] || [ "$ours_mathlib" != "$their_mathlib" ]; then - echo "::error::fetch_dependency_caches: TauCeti $TAUCETI_REV was built with $their_toolchain and Mathlib $their_mathlib, but this project pins $ours_toolchain and Mathlib $ours_mathlib. Pin the same toolchain and Mathlib as the TauCeti commit so its build cache applies." - exit 1 -fi - -CONFIG="$(mktemp "${RUNNER_TEMP:-${TMPDIR:-/tmp}}/lean-eval-dependency-cache.XXXXXX")" -python3 - "$CONFIG" "$ARTIFACT_ENDPOINT" "$REVISION_ENDPOINT" <<'PY' -import json, sys -path, artifacts, revisions = sys.argv[1:] -with open(path, "w", encoding="utf-8") as f: - # JSON strings are valid TOML basic strings. - f.write('cache.defaultService = "tauceti-public"\n') - f.write('[[cache.service]]\n') - f.write('name = "tauceti-public"\n') - f.write('kind = "s3"\n') - f.write(f"artifactEndpoint = {json.dumps(artifacts)}\n") - f.write(f"revisionEndpoint = {json.dumps(revisions)}\n") -PY - -fetched=0 -for attempt in 1 2 3; do - if (cd "$PROJECT_DIR" && CURL="$CACHE_CURL" LAKE_CONFIG="$CONFIG" lake -v cache get --service tauceti-public \ - --repo TauCetiProject/TauCeti --package TauCeti --rev "$TAUCETI_REV" --mappings-only); then - fetched=1 - break - fi - echo "::notice::fetching TauCeti's cache mappings failed (attempt $attempt of 3)" - sleep 5 -done -if [ "$fetched" != 1 ]; then - echo "::error::fetch_dependency_caches: could not fetch TauCeti's cache mappings for $TAUCETI_REV" - exit 1 -fi - -if [ "$RESTORE" = 1 ]; then - # Every TauCeti module a `.lean` file of the project (outside .lake) imports, one per line. - # Lean's header syntax is `[public] [meta] import [all] Module`; a file that cannot be read - # makes this fail rather than silently restore less. - modules="$(python3 - "$PROJECT_DIR" <<'PY' -import pathlib, re, sys -root = pathlib.Path(sys.argv[1]) -pattern = re.compile( - r"^\s*(?:public\s+)?(?:meta\s+)?import\s+(?:all\s+)?(TauCeti(?:\.[^\s.-]+)*)", re.M) -found = set() -for path in root.rglob("*.lean"): - if ".lake" in path.relative_to(root).parts: - continue - found.update(pattern.findall(path.read_text(encoding="utf-8"))) -print("\n".join(sorted(found))) -PY -)" - if [ -n "$modules" ]; then - count="$(printf '%s\n' "$modules" | wc -l)" - echo "fetch_dependency_caches: restoring $count imported TauCeti module(s) and their dependencies" - log="$(mktemp)" - restored=0 - for attempt in 1 2; do - # shellcheck disable=SC2086 # one module name per word; no whitespace - if (cd "$PROJECT_DIR" && CURL="$CACHE_CURL" LAKE_CONFIG="$CONFIG" LAKE_ARTIFACT_CACHE=true \ - LAKE_RESTORE_ARTIFACTS=true lake -v --no-build build $modules) > "$log" 2>&1; then - restored=1 - break - fi - cat "$log" - if [ "$attempt" = 1 ]; then - echo "::notice::cache-only restoration failed (attempt 1 of 2); retrying without compiling dependencies" - sleep 5 - fi - done - if [ "$restored" != 1 ]; then - rm -f "$log" - echo "::error::fetch_dependency_caches: dependency cache restoration failed after bounded retries; no compilation was permitted. Inspect the diagnostics above for unavailable artifacts or out-of-date dependencies, and check the pins and published cache coverage." - exit 1 - fi - compiled="$(grep -cE 'Built TauCeti(\.|$| )' "$log" || true)" - if [ "$compiled" != 0 ]; then - grep -m 20 -E 'Built TauCeti(\.|$| )' "$log" || true - rm -f "$log" - echo "::error::fetch_dependency_caches: $compiled TauCeti module(s) were compiled instead of downloaded; TauCeti's cache does not cover this pin" - exit 1 - fi - rm -f "$log" - fi -fi - -if [ -n "${GITHUB_ENV:-}" ]; then - { - echo "LAKE_CONFIG=$CONFIG" - echo "LAKE_ARTIFACT_CACHE=true" - echo "CURL=$CACHE_CURL" - } >> "$GITHUB_ENV" -else - printf 'export LAKE_CONFIG=%q LAKE_ARTIFACT_CACHE=true CURL=%q\n' "$CONFIG" "$CACHE_CURL" >&3 -fi +exec python3 "$(dirname "${BASH_SOURCE[0]}")/fetch_dependency_caches.py" "$@" diff --git a/solution-dependencies.json b/solution-dependencies.json index d7a619eee..eca594726 100644 --- a/solution-dependencies.json +++ b/solution-dependencies.json @@ -1 +1,27 @@ -[{"name": "lean-pool", "moduleRoots": ["LeanPool", "Challenge", "Solution"]}] +[ + { + "name": "lean-pool", + "moduleRoots": [ + "LeanPool", + "Challenge", + "Solution" + ] + }, + { + "name": "cfsg", + "moduleRoots": [ + "CFSG", + "CFSGWithCertificates", + "Certificates", + "Comparator" + ] + }, + { + "name": "Stacks", + "moduleRoots": [ + "Stacks", + "StacksCore", + "StacksFrontier" + ] + } +] diff --git a/tests/python/test_fetch_dependency_caches.py b/tests/python/test_fetch_dependency_caches.py index 81d37dfa7..49882c101 100644 --- a/tests/python/test_fetch_dependency_caches.py +++ b/tests/python/test_fetch_dependency_caches.py @@ -8,6 +8,7 @@ import sys import tempfile import unittest +import tomllib ROOT = pathlib.Path(__file__).resolve().parents[2] @@ -26,8 +27,10 @@ def setUp(self): {"name": "mathlib", "rev": "2" * 40}]} for path in [self.project, package]: (path / "lake-manifest.json").write_text(json.dumps(manifest)) - (path / "lean-toolchain").write_text("leanprover/lean4:v4.35.0-rc3\n") + (path / "lean-toolchain").write_text((ROOT / "lean-toolchain").read_text()) (self.project / "Main.lean").write_text("import TauCeti.Example\n") + (package / "TauCeti").mkdir() + (package / "TauCeti/Example.lean").write_text("def example := 1\n") self.calls = self.root / "calls.jsonl" tools = self.root / "bin" tools.mkdir() @@ -37,13 +40,13 @@ def setUp(self): f"calls=pathlib.Path({str(self.calls)!r})\n" "previous=calls.read_text().splitlines() if calls.exists() else []\n" "with calls.open('a') as f: f.write(json.dumps({'args':sys.argv[1:]," - "'curl':os.environ.get('CURL')})+'\\n')\n" + "'curl':os.environ.get('CURL'), 'config':pathlib.Path(os.environ['LAKE_CONFIG']).read_text()})+'\\n')\n" "if 'build' in sys.argv:\n" " count=sum('build' in json.loads(p)['args'] for p in previous)\n" " if count < int(os.environ.get('FAIL_RESTORES','0')):\n" " print('curl: (22) artifact service returned 503')\n" " sys.exit(3)\n" - " print('Fetched TauCeti.Example')\n" + " print(os.environ.get('BUILD_MESSAGE', 'Fetched TauCeti.Example'))\n" ) (tools / "lake").chmod(0o755) (tools / "sleep").write_text("#!/bin/sh\nexit 0\n") @@ -86,5 +89,115 @@ def test_pin_mismatch_stops_before_any_lake_command(self): self.assertFalse(self.calls.exists()) + def add_library(self, name, dependencies=None): + path = self.project / ".lake/packages" / name + path.mkdir(parents=True) + root_manifest = json.loads((self.project / "lake-manifest.json").read_text()) + root_manifest["packages"].append({"name": name, "rev": "3" * 40}) + (self.project / "lake-manifest.json").write_text(json.dumps(root_manifest)) + (path / "lake-manifest.json").write_text(json.dumps({"packages": dependencies or [ + {"name": "mathlib", "rev": "2" * 40}]})) + (path / "lean-toolchain").write_text((ROOT / "lean-toolchain").read_text()) + for module in {"cfsg": ["CFSG", "CFSG/Real", "CFSG/Example", "Certificates/Data/Example"], + "Stacks": ["Stacks", "StacksCore/Example", "StacksFrontier/Example"]}.get(name, []): + source = path / (module + ".lean") + source.parent.mkdir(parents=True, exist_ok=True) + source.write_text("def example := 1\n") + return path + + def test_multiple_caches_and_transitive_tauceti_use_distinct_services(self): + self.add_library("cfsg", [{"name": "mathlib", "rev": "2" * 40}, + {"name": "TauCeti", "rev": "1" * 40}]) + self.add_library("Stacks") + self.env.update(STACKS_ARTIFACT_ENDPOINT="https://stacks.example/artifacts", + STACKS_REVISION_ENDPOINT="https://stacks.example/revisions") + (self.project / "Main.lean").write_text( + "module\n/- outer /- import CFSG.Fake -/ comment -/\n" + "public import\n CFSG.Real\nimport Certificates.Data.Example\n" + "meta import all StacksCore.Example\nimport StacksFrontier.Example\n") + result = self.run_script(0) + self.assertEqual(result.returncode, 0, result.stderr) + calls = [json.loads(line) for line in self.calls.read_text().splitlines()] + mappings = [c for c in calls if "cache" in c["args"]] + self.assertEqual({c["args"][c["args"].index("--package") + 1] for c in mappings}, + {"cfsg", "Stacks", "TauCeti"}) + config = tomllib.loads(calls[0]["config"]) + self.assertEqual({s["name"] for s in config["cache"]["service"]}, + {"cfsg-public", "stacks-public", "tauceti-public"}) + build = next(c["args"] for c in calls if "build" in c["args"]) + self.assertIn("+CFSG.Real", build) + self.assertIn("+Certificates.Data.Example", build) + self.assertIn("+StacksCore.Example", build) + self.assertIn("+StacksFrontier.Example", build) + self.assertNotIn("+CFSG.Fake", build) + + def test_unused_libraries_need_no_cache_or_matching_toolchain(self): + stacks = self.add_library("Stacks") + (stacks / "lean-toolchain").write_text("leanprover/lean4:v4.34.0\n") + (self.project / "Main.lean").write_text("import Mathlib\n") + result = self.run_script(0) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(result.stdout, "") + self.assertFalse(self.calls.exists()) + + def test_parsing_submission_headers_never_executes_solver_code(self): + marker = self.root / "solver-code-ran" + (self.project / "Main.lean").write_text( + f'import Lean\n#eval IO.FS.writeFile {json.dumps(str(marker))} "executed"\n') + result = self.run_script(0) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertFalse(marker.exists()) + self.assertFalse(self.calls.exists()) + + def test_bad_solver_imports_are_left_to_comparator_without_running_lake(self): + for header in ["import TauCeti.\n", "import TauCeti.Missing\n", + "import TauCeti.«../../Submission/Evil»\n"]: + with self.subTest(header=header): + (self.project / "Main.lean").write_text(header) + result = self.run_script(0) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertFalse(self.calls.exists()) + + def test_transitive_pin_mismatch_is_rejected_before_fetching(self): + self.add_library("cfsg", [{"name": "mathlib", "rev": "2" * 40}, + {"name": "TauCeti", "rev": "0" * 40}]) + (self.project / "Main.lean").write_text("import CFSG.Example\n") + result = self.run_script(0) + self.assertNotEqual(result.returncode, 0) + self.assertIn("Different dependency pins: TauCeti", result.stderr) + self.assertFalse(self.calls.exists()) + + def test_unconfigured_stacks_endpoint_fails_before_fetching(self): + self.add_library("Stacks") + (self.project / "Main.lean").write_text("import Stacks\n") + result = self.run_script(0) + self.assertNotEqual(result.returncode, 0) + self.assertIn("STACKS_ARTIFACT_ENDPOINT", result.stderr) + self.assertFalse(self.calls.exists()) + + def test_missing_checkout_fails_before_fetching(self): + self.add_library("Stacks") + (self.project / ".lake/packages/Stacks/lake-manifest.json").unlink() + (self.project / "Main.lean").write_text("import Stacks\n") + result = self.run_script(0) + self.assertNotEqual(result.returncode, 0) + self.assertIn("fetch the dependencies first", result.stderr) + self.assertFalse(self.calls.exists()) + + def test_github_environment_and_no_build_defense(self): + environment = self.root / "github-env" + self.env["GITHUB_ENV"] = str(environment) + result = self.run_script(0) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(result.stdout, "") + self.assertIn("LAKE_CONFIG=", environment.read_text()) + self.env["BUILD_MESSAGE"] = "Built TauCeti.Example" + environment.unlink() + result = self.run_script(0) + self.assertNotEqual(result.returncode, 0) + self.assertIn("compiled instead of downloaded", result.stderr) + self.assertFalse(environment.exists()) + + if __name__ == "__main__": unittest.main() diff --git a/tests/python/test_lake_cache_restore.py b/tests/python/test_lake_cache_restore.py index 34493ead9..d8ee9ab95 100644 --- a/tests/python/test_lake_cache_restore.py +++ b/tests/python/test_lake_cache_restore.py @@ -25,8 +25,11 @@ def test_failed_download_can_be_retried_without_compilation_or_poisoned_cache(se (root / "lakefile.toml").write_text( 'name = "cache-probe"\ndefaultTargets = ["CacheProbe"]\n' '[[lean_lib]]\nname = "CacheProbe"\n' + '[[lean_lib]]\nname = "Precompiled"\nprecompileModules = true\n' ) - (root / "CacheProbe.lean").write_text("def cacheProbe : Nat := 42\n") + (root / "Precompiled.lean").write_text("def precompiledValue : Nat := 41\n") + (root / "CacheProbe.lean").write_text( + "import Precompiled\ndef cacheProbe : Nat := precompiledValue + 1\n") (root / "UseCacheProbe.lean").write_text( "import CacheProbe\nexample : cacheProbe = 42 := rfl\n" ) @@ -71,6 +74,10 @@ def lake(*args): self.assertEqual(built.returncode, 0, built.stdout + built.stderr) artifacts = cache / "artifacts" self.assertTrue(list(artifacts.glob("*.olean"))) + # CFSG uses precompiled libraries. Their linked native outputs + # must also restore without invoking a compiler or linker. + self.assertTrue(any(p.suffix in {".so", ".dylib", ".dll"} + for p in artifacts.iterdir())) payloads.update({p.stem: p.read_bytes() for p in artifacts.iterdir()}) # Remote mappings imported by `lake cache get --mappings-only` # bind their service and scope; locally produced mappings do not. @@ -84,16 +91,17 @@ def lake(*args): thread = threading.Thread(target=server.serve_forever, daemon=True) thread.start() try: - failed = lake("-v", "--no-build", "build") + failed = lake("-v", "--no-build", "build", "+CacheProbe") self.assertNotEqual(failed.returncode, 0) self.assertIn("curl", failed.stdout + failed.stderr) self.assertTrue(requests) self.assertFalse((root / ".lake/build/lib/lean/CacheProbe.olean").exists()) self.assertEqual(list(artifacts.iterdir()), []) healthy = True - restored = lake("-v", "--no-build", "build") + restored = lake("-v", "--no-build", "build", "+CacheProbe") self.assertEqual(restored.returncode, 0, restored.stdout + restored.stderr) self.assertNotIn("Built CacheProbe", restored.stdout + restored.stderr) + self.assertNotIn("Built Precompiled", restored.stdout + restored.stderr) checked = lake("env", "lean", "UseCacheProbe.lean") self.assertEqual(checked.returncode, 0, checked.stdout + checked.stderr) finally: From 7b8a636615cfd7fd2833b1bef579d76a402db5d8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 13 Nov 2026 04:59:27 +0000 Subject: [PATCH 2/7] Use the published Stacks cache service by default --- README.md | 13 +++++++------ scripts/fetch_dependency_caches.py | 15 +++++++-------- tests/python/test_fetch_dependency_caches.py | 17 ++++++++++++----- 3 files changed, 26 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index 344444c62..1ae5d0e44 100644 --- a/README.md +++ b/README.md @@ -228,12 +228,13 @@ pins. Unused libraries require no artifact downloads. LeanEval currently uses Lean **v4.36.0-rc2**. The public CFSG pin still uses v4.35.0-rc3, and the public Stacks pin uses v4.35.0. Their imports will fail the -cache compatibility check until matching upstream builds are published. CFSG's -published cache URLs are configured in the helper. Stacks' public README does not -yet give cache URLs; set `STACKS_ARTIFACT_ENDPOINT` and `STACKS_REVISION_ENDPOINT` -when preparing a compatible Stacks checkout. Endpoint overrides are also available -as `CFSG_*` and `TAUCETI_*`. CI and the submission runner read the Stacks URLs -from repository variables with those same names. +cache compatibility check until matching upstream builds are published. The helper +uses the published [CFSG cache](https://cfsg-downloads.axiommath.workers.dev/lake/lake-cache-get-fast.sh) +and [Stacks cache](https://stacks-cache.axiommath.workers.dev/lake/lake-cache-get-fast.sh) +endpoints by default. Set `STACKS_ARTIFACT_ENDPOINT` and `STACKS_REVISION_ENDPOINT` +to override the Stacks endpoints; corresponding overrides are available as +`CFSG_*` and `TAUCETI_*`. CI and the submission runner accept the Stacks overrides +from repository variables with those same names; empty variables use the defaults. ### 5. Run comparator locally diff --git a/scripts/fetch_dependency_caches.py b/scripts/fetch_dependency_caches.py index e0121f5aa..6e6cd1e2f 100644 --- a/scripts/fetch_dependency_caches.py +++ b/scripts/fetch_dependency_caches.py @@ -32,9 +32,8 @@ class Library: "https://cache.taucetiproject.org"), Library("cfsg", "AxiomMath/CFSG", ("CFSG", "CFSGWithCertificates", "Certificates", "Comparator"), "CFSG", "https://cfsg-downloads.axiommath.workers.dev/lake"), - # Supply STACKS_ARTIFACT_ENDPOINT and STACKS_REVISION_ENDPOINT until the - # publisher confirms its public URLs. Never guess a cache's provenance. - Library("Stacks", "AxiomMath/Stacks", ("Stacks", "StacksCore", "StacksFrontier"), "STACKS"), + Library("Stacks", "AxiomMath/Stacks", ("Stacks", "StacksCore", "StacksFrontier"), + "STACKS", "https://stacks-cache.axiommath.workers.dev/lake"), ) @@ -56,7 +55,7 @@ def unreadable(error: OSError) -> None: source_list = Path(temporary) / "paths.json" source_list.write_text(json.dumps(paths), encoding="utf-8") result = subprocess.run( - ["lean", "--run", str(SCRIPTS / "dependency_imports.lean"), str(source_list)], + ["lean", "-j2", "--run", str(SCRIPTS / "dependency_imports.lean"), str(source_list)], cwd=project, text=True, capture_output=True, check=False, ) if result.returncode: @@ -147,10 +146,10 @@ def prepare(project: Path, restore: bool) -> dict[str, str]: f"this project pins {toolchain}. Different dependency pins: {', '.join(mismatches) or 'none'}. " "Pin the same toolchain and Mathlib (and other transitive dependencies) as the library " "commit so its build cache applies.") - artifacts = os.environ.get(f"{library.prefix}_ARTIFACT_ENDPOINT", - f"{library.endpoint}/artifacts" if library.endpoint else "") - revisions = os.environ.get(f"{library.prefix}_REVISION_ENDPOINT", - f"{library.endpoint}/revisions" if library.endpoint else "") + artifacts = (os.environ.get(f"{library.prefix}_ARTIFACT_ENDPOINT") or + (f"{library.endpoint}/artifacts" if library.endpoint else "")) + revisions = (os.environ.get(f"{library.prefix}_REVISION_ENDPOINT") or + (f"{library.endpoint}/revisions" if library.endpoint else "")) if not artifacts or not revisions: raise RuntimeError(f"set {library.prefix}_ARTIFACT_ENDPOINT and " f"{library.prefix}_REVISION_ENDPOINT to the publisher's public cache URLs") diff --git a/tests/python/test_fetch_dependency_caches.py b/tests/python/test_fetch_dependency_caches.py index 49882c101..986fb8ede 100644 --- a/tests/python/test_fetch_dependency_caches.py +++ b/tests/python/test_fetch_dependency_caches.py @@ -55,9 +55,11 @@ def setUp(self): GITHUB_ENV="", RUNNER_TEMP=str(self.root)) def run_script(self, failures): + # Include Lean's parser startup and the deliberately exercised retry + # backoff, including on small hosted runners or a busy development host. return subprocess.run(["bash", str(SCRIPT), "--restore", str(self.project)], env=dict(self.env, FAIL_RESTORES=str(failures)), - capture_output=True, text=True, check=False, timeout=10) + capture_output=True, text=True, check=False, timeout=90) def test_retries_cache_only_restore_and_exports_wrapper_for_later_builds(self): result = self.run_script(1) @@ -167,13 +169,18 @@ def test_transitive_pin_mismatch_is_rejected_before_fetching(self): self.assertIn("Different dependency pins: TauCeti", result.stderr) self.assertFalse(self.calls.exists()) - def test_unconfigured_stacks_endpoint_fails_before_fetching(self): + def test_stacks_uses_published_endpoints_with_empty_workflow_overrides(self): self.add_library("Stacks") + self.env.update(STACKS_ARTIFACT_ENDPOINT="", STACKS_REVISION_ENDPOINT="") (self.project / "Main.lean").write_text("import Stacks\n") result = self.run_script(0) - self.assertNotEqual(result.returncode, 0) - self.assertIn("STACKS_ARTIFACT_ENDPOINT", result.stderr) - self.assertFalse(self.calls.exists()) + self.assertEqual(result.returncode, 0, result.stderr) + calls = [json.loads(line) for line in self.calls.read_text().splitlines()] + service = tomllib.loads(calls[0]["config"])["cache"]["service"][0] + self.assertEqual(service["artifactEndpoint"], + "https://stacks-cache.axiommath.workers.dev/lake/artifacts") + self.assertEqual(service["revisionEndpoint"], + "https://stacks-cache.axiommath.workers.dev/lake/revisions") def test_missing_checkout_fails_before_fetching(self): self.add_library("Stacks") From 5cdd5a22508c5828ebc4188f23dc32354036e396 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 13 Nov 2026 09:38:34 +0000 Subject: [PATCH 3/7] Support stable and release-candidate benchmark configurations --- .github/workflows/cache-restoration.yml | 27 ++- .github/workflows/ci.yml | 103 +++++++++- LeanEval/AlgebraicGeometry/Bezout.lean | 4 +- LeanEval/RepresentationTheory/SchurWeyl.lean | 11 +- LeanEval/Topology/Hurewicz.lean | 2 +- README.md | 33 +++- SECURITY.md | 11 ++ scripts/prepare_toolchain.py | 80 ++++++++ scripts/select_ci_problems.py | 7 +- scripts/select_submission_toolchain.py | 146 +++++++++++++++ supported-toolchains.json | 8 + tests/python/test_prepare_toolchain.py | 76 ++++++++ tests/python/test_select_ci_problems.py | 8 + .../test_select_submission_toolchain.py | 121 ++++++++++++ toolchains/v4.35.0/lake-manifest.json | 177 ++++++++++++++++++ toolchains/v4.35.0/lakefile.toml | 87 +++++++++ toolchains/v4.35.0/lean-toolchain | 1 + toolchains/v4.36.0-rc2/lake-manifest.json | 146 +++++++++++++++ toolchains/v4.36.0-rc2/lakefile.toml | 87 +++++++++ toolchains/v4.36.0-rc2/lean-toolchain | 1 + 20 files changed, 1119 insertions(+), 17 deletions(-) create mode 100644 scripts/prepare_toolchain.py create mode 100644 scripts/select_submission_toolchain.py create mode 100644 supported-toolchains.json create mode 100644 tests/python/test_prepare_toolchain.py create mode 100644 tests/python/test_select_submission_toolchain.py create mode 100644 toolchains/v4.35.0/lake-manifest.json create mode 100644 toolchains/v4.35.0/lakefile.toml create mode 100644 toolchains/v4.35.0/lean-toolchain create mode 100644 toolchains/v4.36.0-rc2/lake-manifest.json create mode 100644 toolchains/v4.36.0-rc2/lakefile.toml create mode 100644 toolchains/v4.36.0-rc2/lean-toolchain diff --git a/.github/workflows/cache-restoration.yml b/.github/workflows/cache-restoration.yml index cede9fae0..0ad778661 100644 --- a/.github/workflows/cache-restoration.yml +++ b/.github/workflows/cache-restoration.yml @@ -11,6 +11,9 @@ on: - tests/python/test_fetch_dependency_caches.py - .github/workflows/cache-restoration.yml - lean-toolchain + - supported-toolchains.json + - toolchains/** + - scripts/prepare_toolchain.py push: branches: [main] paths: @@ -22,12 +25,20 @@ on: - tests/python/test_fetch_dependency_caches.py - .github/workflows/cache-restoration.yml - lean-toolchain + - supported-toolchains.json + - toolchains/** + - scripts/prepare_toolchain.py permissions: contents: read jobs: - restore: + restore_toolchains: + name: restore (${{ matrix.configuration }}) + strategy: + fail-fast: false + matrix: + configuration: [rc, stable] runs-on: ubuntu-24.04 timeout-minutes: 10 steps: @@ -35,6 +46,9 @@ jobs: with: persist-credentials: false + - name: Select benchmark configuration + run: python scripts/prepare_toolchain.py "${{ matrix.configuration }}" --apply + - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: build: false @@ -50,3 +64,14 @@ jobs: export ELAN_TOOLCHAIN="$(cat lean-toolchain)" python -m unittest discover -v -s tests/python -p 'test_lake_cache_*.py' python -m unittest discover -v -s tests/python -p test_fetch_dependency_caches.py + + restore: + if: always() + needs: restore_toolchains + runs-on: ubuntu-24.04 + timeout-minutes: 2 + steps: + - name: Require both toolchain cache checks + env: + RESULT: ${{ needs.restore_toolchains.result }} + run: test "$RESULT" = success diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d2c53b6ba..2a17ff5a2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -57,7 +57,10 @@ jobs: # a pin they reject breaks every server-dispatched evaluation while this # repository's CI stays green (v4.35.0-rc3, 2026-09-30 to 2026-10-07). - name: Check the pipeline accepts the pinned toolchain - run: python scripts/check_pipeline_toolchain_contract.py + run: | + python scripts/check_pipeline_toolchain_contract.py + python scripts/check_pipeline_toolchain_contract.py \ + --toolchain-file toolchains/v4.35.0/lean-toolchain # Install the pinned Lean toolchain without building the project. The # dependency selector consumes a graph produced by Lean's header parser; @@ -189,12 +192,16 @@ jobs: - name: Run Python unit tests run: python -m unittest discover -s tests/python -p 'test_*.py' - security: - name: Security and scoring smoke tests + security_toolchains: + name: Security and scoring smoke tests (${{ matrix.configuration }}) needs: classify if: needs.classify.outputs.run_checks == 'true' runs-on: ubuntu-latest timeout-minutes: 60 + strategy: + fail-fast: false + matrix: + configuration: [rc, stable] steps: - name: Free up disk space # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04). @@ -215,6 +222,9 @@ jobs: fetch-depth: 0 persist-credentials: false + - name: Select benchmark configuration + run: python scripts/prepare_toolchain.py "${{ matrix.configuration }}" --apply + # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04). - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: @@ -258,6 +268,19 @@ jobs: - name: Run eval workflow smoke test run: lake exe lean-eval check-eval-workflow + security: + name: Security and scoring smoke tests + if: always() + needs: security_toolchains + runs-on: ubuntu-latest + timeout-minutes: 2 + steps: + - name: Require both toolchain sandbox and scoring checks + env: + RESULT: ${{ needs.security_toolchains.result }} + run: | + case "$RESULT" in success|skipped) ;; *) exit 1 ;; esac + catalog: name: Catalog validation (shard ${{ matrix.shard }}/${{ matrix.shard_count }}) needs: classify @@ -387,6 +410,75 @@ jobs: if-no-files-found: error retention-days: 1 + stable_catalog: + name: Stable catalog compilation (shard ${{ matrix.shard }}/${{ matrix.shard_count }}) + needs: classify + if: needs.classify.outputs.run_catalog == 'true' + runs-on: ubuntu-latest + timeout-minutes: 60 + strategy: + fail-fast: false + matrix: ${{ fromJSON(needs.classify.outputs.matrix) }} + steps: + - name: Free up disk space + # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04). + # Bump procedure: SECURITY.md > "Bumping pinned dependencies". + uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be + with: + tool-cache: false + android: true + dotnet: true + haskell: true + large-packages: true + docker-images: true + swap-storage: true + + # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30). + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + fetch-depth: 0 + persist-credentials: false + + - name: Select stable toolchain and dependency pins + run: python scripts/prepare_toolchain.py stable --apply + + # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04). + - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 + with: + use-mathlib-cache: true + build: false + test: false + lint: false + + - name: Fetch imported dependency build caches + env: + STACKS_ARTIFACT_ENDPOINT: ${{ vars.STACKS_ARTIFACT_ENDPOINT }} + STACKS_REVISION_ENDPOINT: ${{ vars.STACKS_REVISION_ENDPOINT }} + # Imported large libraries download their published oleans + # without compiling on a cache miss; see scripts/fetch_dependency_caches.sh. + run: bash scripts/fetch_dependency_caches.sh --restore . + + - name: Clear cached problem-module artifacts + run: | + set -euo pipefail + artifact_dir=.lake/build/lib/lean/LeanEval + if [ -d "$artifact_dir" ]; then + find "$artifact_dir" \( -type f -o -type l \) -delete + fi + + - name: Build problem modules without warnings + env: + MODULES: ${{ matrix.modules }} + SHARD_INDEX: ${{ matrix.shard }} + run: | + set -euo pipefail + IFS=',' read -r -a modules <<< "$MODULES" + module_args=() + for module in "${modules[@]}"; do + module_args+=(--module "$module") + done + lake exe lean-eval check-problem-build "${module_args[@]}" + catalog_inventory: name: Manifest inventory aggregate needs: [classify, catalog] @@ -446,7 +538,7 @@ jobs: verify: name: verify if: always() - needs: [classify, checks, security, catalog, catalog_inventory] + needs: [classify, checks, security, catalog, stable_catalog, catalog_inventory] runs-on: ubuntu-latest timeout-minutes: 2 steps: @@ -456,11 +548,12 @@ jobs: CHECKS_RESULT: ${{ needs.checks.result }} SECURITY_RESULT: ${{ needs.security.result }} CATALOG_RESULT: ${{ needs.catalog.result }} + STABLE_CATALOG_RESULT: ${{ needs.stable_catalog.result }} CATALOG_INVENTORY_RESULT: ${{ needs.catalog_inventory.result }} run: | set -euo pipefail for result in "$CLASSIFY_RESULT" "$CHECKS_RESULT" \ - "$SECURITY_RESULT" "$CATALOG_RESULT" \ + "$SECURITY_RESULT" "$CATALOG_RESULT" "$STABLE_CATALOG_RESULT" \ "$CATALOG_INVENTORY_RESULT"; do if [ "$result" != success ] && [ "$result" != skipped ]; then echo "A required CI branch ended with: $result" >&2 diff --git a/LeanEval/AlgebraicGeometry/Bezout.lean b/LeanEval/AlgebraicGeometry/Bezout.lean index 06ef53780..eaef7dfe1 100644 --- a/LeanEval/AlgebraicGeometry/Bezout.lean +++ b/LeanEval/AlgebraicGeometry/Bezout.lean @@ -43,11 +43,11 @@ def vanishingSet {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) : /-- A chosen index `i : Fin (n+1)` with `p.rep i ≠ 0`. -/ noncomputable def chartIndex {n : ℕ} (p : ProjSpace K n) : Fin (n + 1) := - Classical.choose (Function.ne_iff.mp p.rep_ne_zero) + Classical.choose (Function.ne_iff.mp p.out.property) lemma chartIndex_rep_ne_zero {n : ℕ} (p : ProjSpace K n) : Projectivization.rep p (chartIndex p) ≠ 0 := - Classical.choose_spec (Function.ne_iff.mp p.rep_ne_zero) + Classical.choose_spec (Function.ne_iff.mp p.out.property) /-- Affine cone coordinates of `p` on the chart `X_{chartIndex p} = 1`. -/ noncomputable def affineConeCoord {n : ℕ} (p : ProjSpace K n) : diff --git a/LeanEval/RepresentationTheory/SchurWeyl.lean b/LeanEval/RepresentationTheory/SchurWeyl.lean index e648b850b..58a9be361 100644 --- a/LeanEval/RepresentationTheory/SchurWeyl.lean +++ b/LeanEval/RepresentationTheory/SchurWeyl.lean @@ -28,13 +28,16 @@ def symAction (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] (k : toFun σ := (PiTensorProduct.reindex R (fun _ : Fin k => M) σ).toLinearMap map_one' := by ext x - simp only [LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, Function.comp_apply, - PiTensorProduct.reindex_tprod, one_apply_eq_self] + change PiTensorProduct.reindex R (fun _ : Fin k => M) 1 (PiTensorProduct.tprod R x) = + PiTensorProduct.tprod R x + simp only [PiTensorProduct.reindex_tprod] rfl map_mul' σ τ := by ext x - simp only [mul_apply_eq_comp, LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, - Function.comp_apply, PiTensorProduct.reindex_tprod] + change PiTensorProduct.reindex R (fun _ : Fin k => M) (σ * τ) (PiTensorProduct.tprod R x) = + PiTensorProduct.reindex R (fun _ : Fin k => M) σ + (PiTensorProduct.reindex R (fun _ : Fin k => M) τ (PiTensorProduct.tprod R x)) + simp only [PiTensorProduct.reindex_tprod] rfl /-- The general linear group `GL(V)` acts diagonally on `V^⊗k`: diff --git a/LeanEval/Topology/Hurewicz.lean b/LeanEval/Topology/Hurewicz.lean index 90c0c1367..0b6568de4 100644 --- a/LeanEval/Topology/Hurewicz.lean +++ b/LeanEval/Topology/Hurewicz.lean @@ -25,7 +25,7 @@ abelianization of `π₁(X, x)`. -/ @[eval_problem] theorem hurewicz_h1_abelianization (X : Type) [TopologicalSpace X] [PathConnectedSpace X] (x : X) : - Nonempty (Additive (Group.Abelianization (FundamentalGroup X x)) ≃+ + Nonempty (Additive ((FundamentalGroup X x) ⧸ commutator (FundamentalGroup X x)) ≃+ (IntegralHomology 1 X : Type)) := by sorry diff --git a/README.md b/README.md index 1ae5d0e44..ef665eb35 100644 --- a/README.md +++ b/README.md @@ -10,6 +10,31 @@ tooling generates one comparator workspace per problem under `generated/`. A submission is scored entirely by comparator results: a problem counts as solved iff comparator accepts the submitted solution. +LeanEval supports **Lean v4.35.0** and **Lean v4.36.0-rc2**. The latter is the +default checkout. Each configuration in `supported-toolchains.json` pins its own +Mathlib, TauCeti, and transitive dependencies. CI requires the shared problem +statements to compile on both toolchains without unexpected warnings; it does +not compare their elaborated meanings across dependency versions. + +To work on the stable configuration in an isolated directory: + +```bash +python scripts/prepare_toolchain.py stable --destination /tmp/lean-eval-stable +cd /tmp/lean-eval-stable +lake exe cache get +cache_env="$(bash scripts/fetch_dependency_caches.sh --restore .)" && eval "$cache_env" +lake exe lean-eval generate --problem two_plus_two +lake exe lean-eval start-problem two_plus_two +``` + +Use `rc` instead of `stable` for the default configuration. Existing build outputs +are excluded from these copies. After selecting a configuration, regenerate each +workspace you use so its pins and extracted statements match that configuration. +The submission service reads the closest `lean-toolchain` at or above each +submitted workspace and selects the corresponding approved configuration. Omit +the file to use the default. Submit workspaces for different toolchains separately. +Result verification receipts and archive sidecars record the selected toolchain and exact benchmark commit. + The main user-facing entrypoint is: ```bash @@ -226,9 +251,11 @@ and restores only the imported modules and their transitive dependencies. It use Each library must match the workspace's Lean toolchain and all transitive dependency pins. Unused libraries require no artifact downloads. -LeanEval currently uses Lean **v4.36.0-rc2**. The public CFSG pin still uses -v4.35.0-rc3, and the public Stacks pin uses v4.35.0. Their imports will fail the -cache compatibility check until matching upstream builds are published. The helper +The public CFSG pin still uses v4.35.0-rc3. Stacks uses v4.35.0 with Mathlib +`56a00585`, while LeanEval's stable configuration uses Mathlib `07406378` to +match TauCeti's stable release. These library imports fail the cache compatibility +check until matching dependency builds are published, including the Mathlib pin. +Unused solution libraries do not prevent evaluation on either toolchain. The helper uses the published [CFSG cache](https://cfsg-downloads.axiommath.workers.dev/lake/lake-cache-get-fast.sh) and [Stacks cache](https://stacks-cache.axiommath.workers.dev/lake/lake-cache-get-fast.sh) endpoints by default. Set `STACKS_ARTIFACT_ENDPOINT` and `STACKS_REVISION_ENDPOINT` diff --git a/SECURITY.md b/SECURITY.md index 9bc3bd6be..cb80c7a83 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -122,6 +122,17 @@ in both benchmark and submission installers. Review the actual sandbox behavior, not just the reported version. No standalone comparator/exporter/NanoDa build or Landrun pin is required by this benchmark. +`supported-toolchains.json` selects only benchmark-owned configurations under +`toolchains/`. Keep the default configuration identical to the root Lake files. +Each configuration has separate package checkouts and build outputs. Source +`lean-toolchain` files request a configuration; they cannot authorize arbitrary +toolchains, dependency pins, Lake code, or build commands. Selection reads the +archived tar stream without extracting or executing submission code. The archive +lane retains invalid requests; evaluation rejects them after archival. Regenerate +selected pristine workspaces from trusted sources before overlaying solver files. +CI checks compilation under both supported configurations, without asserting +equivalence of their elaborated problem statements. + The generator rejects Lean Pool, CFSG, and Stacks imports in trusted statements and helpers while making their pinned source available to solutions. Cache preparation parses submission headers without elaborating them and restores only diff --git a/scripts/prepare_toolchain.py b/scripts/prepare_toolchain.py new file mode 100644 index 000000000..4a44b2fb2 --- /dev/null +++ b/scripts/prepare_toolchain.py @@ -0,0 +1,80 @@ +#!/usr/bin/env python3 +"""Select a benchmark-owned toolchain configuration in an isolated checkout. + +Use --destination to create a separate working copy, or --apply in a fresh CI +checkout before fetching dependencies. Regenerate selected workspaces afterwards; +generated statements and build outputs must come from the selected configuration. +""" +from __future__ import annotations + +import argparse +import json +from pathlib import Path +import shutil +import sys + + +ROOT = Path(__file__).resolve().parents[1] +FILES = ("lean-toolchain", "lakefile.toml", "lake-manifest.json") + + +def configurations(root: Path) -> tuple[str, dict[str, Path]]: + data = json.loads((root / "supported-toolchains.json").read_text()) + result = {} + for toolchain, relative in data["configurations"].items(): + path = (root / relative).resolve() + if not path.is_relative_to(root.resolve()): + raise ValueError("toolchain configuration escapes the benchmark") + if (path / "lean-toolchain").read_text().strip() != toolchain: + raise ValueError(f"toolchain configuration disagrees with its pin: {toolchain}") + for name in FILES: + if (path / name).is_symlink() or not (path / name).is_file(): + raise ValueError(f"missing regular configuration file: {path / name}") + result[toolchain] = path + if data["default"] not in result or data["stable"] not in result: + raise ValueError("default or stable toolchain has no configuration") + return data["default"], result + + +def prepare(root: Path, toolchain: str, destination: Path | None = None) -> Path: + default, supported = configurations(root) + stable = json.loads((root / "supported-toolchains.json").read_text())["stable"] + toolchain = {"stable": stable, "default": default, + "rc": default}.get(toolchain, toolchain) + if toolchain not in supported: + raise ValueError(f"unsupported toolchain {toolchain!r}; choose {', '.join(supported)}") + # Read everything before mutation, including when the chosen configuration + # is the root itself. Build artifacts are never reused between toolchains. + contents = {name: (supported[toolchain] / name).read_bytes() for name in FILES} + target = root if destination is None else destination.resolve() + if destination is None: + if (root / ".lake").exists() or (root / ".lake").is_symlink(): + raise ValueError("--apply requires a fresh checkout without .lake; use --destination") + else: + if target.exists(): + raise ValueError(f"destination already exists: {target}") + if target.is_relative_to(root.resolve()) and ".lake" not in target.relative_to(root).parts: + raise ValueError("an in-tree destination must be under .lake") + shutil.copytree(root, target, ignore=shutil.ignore_patterns( + ".git", ".lake", ".cache", "build", "workspaces", "__pycache__")) + for name, content in contents.items(): + (target / name).write_bytes(content) + return target + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("toolchain") + mode = parser.add_mutually_exclusive_group(required=True) + mode.add_argument("--destination", type=Path) + mode.add_argument("--apply", action="store_true") + args = parser.parse_args() + try: + print(prepare(ROOT, args.toolchain, args.destination)) + except (OSError, ValueError, KeyError) as error: + parser.exit(1, f"prepare_toolchain: {error}\n") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/select_ci_problems.py b/scripts/select_ci_problems.py index 178800bff..21699ca54 100644 --- a/scripts/select_ci_problems.py +++ b/scripts/select_ci_problems.py @@ -186,6 +186,10 @@ def is_full_catalog_sentinel(path: str) -> bool: or path == ".github/workflows/ci.yml" or path == "manifests/tags.toml" or path == "scripts/select_ci_problems.py" + or path == "scripts/prepare_toolchain.py" + or path == "scripts/select_submission_toolchain.py" + or path == "supported-toolchains.json" + or path.startswith("toolchains/") or path in {"lakefile.toml", "lake-manifest.json", "lean-toolchain", "solution-dependencies.json"} ) @@ -205,7 +209,8 @@ def select( changed_paths = [path for change in changes for path in change.paths] source_changed = any( - path.startswith(("LeanEval/", "EvalTools/", "templates/", "manifests/")) + path.startswith(("LeanEval/", "EvalTools/", "templates/", "manifests/", "toolchains/")) + or path in {"supported-toolchains.json", "scripts/prepare_toolchain.py"} or path in {"lakefile.toml", "lake-manifest.json", "lean-toolchain", "solution-dependencies.json"} for path in changed_paths ) diff --git a/scripts/select_submission_toolchain.py b/scripts/select_submission_toolchain.py new file mode 100644 index 000000000..e6984496c --- /dev/null +++ b/scripts/select_submission_toolchain.py @@ -0,0 +1,146 @@ +#!/usr/bin/env python3 +"""Read toolchain requests from archived source without extracting or executing it. + +The closest lean-toolchain at or above each submitted workspace selects an +approved benchmark configuration. Missing pins use the default. One archive +must select one toolchain. Archive mode retains invalid requests using the +default; evaluation rejects them after the source has been durably archived. +""" +from __future__ import annotations + +import argparse +from pathlib import Path, PurePosixPath +import subprocess +import sys +import tarfile +import tomllib + +from prepare_toolchain import ROOT, configurations, prepare + + +class ToolchainRequestError(ValueError): + """Archived source cannot select an approved evaluation configuration.""" + + +def source_requests(archive: Path, root: Path, problem: str | None = None) -> dict[str, str | None]: + known = {p.stem for p in (root / "manifests/problems").glob("*.toml")} + if problem is not None: + if problem not in known: + raise ValueError(f"unknown problem: {problem}") + known = {problem} + pins: dict[PurePosixPath, str | ValueError] = {} + workspaces: dict[PurePosixPath, str] = {} + submissions: dict[PurePosixPath, bytes | None] = {} + # Sequential traversal also handles compressed archives without creating + # a second extracted copy alongside the encrypted archive job's source. + seen = set() + with tarfile.open(archive, mode="r|gz") as source: + for member in source: + path = PurePosixPath(member.name) + if path.is_absolute() or ".." in path.parts: + raise ValueError("source archive contains an escaping path") + if path.name not in {"lean-toolchain", "lakefile.toml", "Submission.lean"}: + continue + if path in seen: + raise ValueError(f"duplicate source configuration: {path}") + seen.add(path) + if not member.isfile(): + if path.name == "lean-toolchain": + pins[path.parent] = ValueError(f"lean-toolchain must be a regular file: {path}") + continue + handle = source.extractfile(member) + if path.name == "lean-toolchain": + if member.size > 256: + pins[path.parent] = ValueError(f"oversized lean-toolchain: {path}") + continue + try: + pins[path.parent] = handle.read().decode("ascii").strip() + except UnicodeError: + pins[path.parent] = ValueError(f"lean-toolchain is not ASCII: {path}") + elif path.name == "lakefile.toml": + if member.size > 1024 * 1024: + continue + try: + name = tomllib.loads(handle.read().decode("utf-8")).get("name") + except (ValueError, UnicodeError): + continue + if isinstance(name, str) and name in known: + workspaces[path.parent] = name + else: + # Stubs are small. Larger submissions can never equal a + # pristine stub, so do not retain their contents in memory. + submissions[path.parent] = handle.read(65537) + result = {} + for directory, name in workspaces.items(): + if directory not in submissions: + continue + stub = root / "generated" / name / "Submission.lean" + if stub.is_file() and submissions[directory] == stub.read_bytes(): + continue + requested = next((pins[parent] for parent in [directory, *directory.parents] + if parent in pins), None) + if isinstance(requested, ValueError): + raise requested + if name in result and result[name] != requested: + raise ValueError(f"multiple toolchains requested for {name}") + result[name] = requested + return result + + +def select(archive: Path, root: Path, problem: str | None = None) -> tuple[str, list[str]]: + default, supported = configurations(root) + try: + requests = source_requests(archive, root, problem) + except Exception as error: + # TOML and archive readers can also raise RecursionError or resource + # errors on malformed source. No source parser failure may block its + # archival, and evaluation treats it as a terminal input rejection. + raise ToolchainRequestError(str(error)) from error + requested = {pin if pin is not None else default for pin in requests.values()} + if not requested: + requested = {default} + if len(requested) != 1: + raise ToolchainRequestError("one submission must use one toolchain; submit the workspaces separately") + toolchain = requested.pop() + if toolchain not in supported: + raise ToolchainRequestError(f"unsupported requested toolchain {toolchain!r}; choose {', '.join(supported)}") + return toolchain, sorted(requests) + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--source-tar", required=True, type=Path) + parser.add_argument("--problem") + parser.add_argument("--archive", action="store_true") + parser.add_argument("--expected") + parser.add_argument("--apply", action="store_true") + parser.add_argument("--regenerate", action="store_true") + args = parser.parse_args() + try: + try: + toolchain, problems = select(args.source_tar, ROOT, args.problem) + except ToolchainRequestError as error: + if not args.archive: + raise + print(f"Retaining invalid toolchain request for evaluation to reject: {error}", file=sys.stderr) + toolchain, problems = configurations(ROOT)[0], [] + if args.expected is not None and args.expected != toolchain: + raise ValueError("source toolchain disagrees with the archived evaluation toolchain") + if args.apply: + prepare(ROOT, toolchain) + if args.regenerate: + if (ROOT / "lean-toolchain").read_text().strip() != toolchain: + raise ValueError("select the requested configuration before regenerating") + for problem in problems: + subprocess.run(["lake", "exe", "lean-eval", "generate", "--problem", problem], + cwd=ROOT, check=True, stdout=sys.stderr) + print(toolchain) + except ToolchainRequestError as error: + parser.exit(3, f"select_submission_toolchain: {error}\n") + except (OSError, ValueError, UnicodeError, tarfile.TarError, subprocess.CalledProcessError) as error: + parser.exit(1, f"select_submission_toolchain: {error}\n") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/supported-toolchains.json b/supported-toolchains.json new file mode 100644 index 000000000..c009fc34b --- /dev/null +++ b/supported-toolchains.json @@ -0,0 +1,8 @@ +{ + "default": "leanprover/lean4:v4.36.0-rc2", + "configurations": { + "leanprover/lean4:v4.36.0-rc2": "toolchains/v4.36.0-rc2", + "leanprover/lean4:v4.35.0": "toolchains/v4.35.0" + }, + "stable": "leanprover/lean4:v4.35.0" +} diff --git a/tests/python/test_prepare_toolchain.py b/tests/python/test_prepare_toolchain.py new file mode 100644 index 000000000..b2e566aab --- /dev/null +++ b/tests/python/test_prepare_toolchain.py @@ -0,0 +1,76 @@ +from __future__ import annotations + +import importlib.util +import json +from pathlib import Path +import tempfile +import tomllib +import unittest + + +ROOT = Path(__file__).resolve().parents[2] +SPEC = importlib.util.spec_from_file_location("prepare_toolchain", ROOT / "scripts/prepare_toolchain.py") +MODULE = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(MODULE) + + +class PrepareToolchainTests(unittest.TestCase): + def test_published_configurations_have_matching_dependency_pins(self): + default, profiles = MODULE.configurations(ROOT) + self.assertEqual(default, (ROOT / "lean-toolchain").read_text().strip()) + self.assertEqual(set(profiles), {"leanprover/lean4:v4.35.0", default}) + for name in MODULE.FILES: + self.assertEqual((profiles[default] / name).read_bytes(), (ROOT / name).read_bytes()) + for profile in profiles.values(): + lakefile = tomllib.loads((profile / "lakefile.toml").read_text()) + packages = {p["name"].strip("«»"): p for p in json.loads( + (profile / "lake-manifest.json").read_text())["packages"]} + for dependency in lakefile["require"]: + self.assertEqual(dependency["rev"], packages[dependency["name"]]["rev"]) + + def fixture(self, root): + for relative, pin in [(".", "leanprover/lean4:v4.36.0-rc2"), + ("stable", "leanprover/lean4:v4.35.0")]: + profile = root / relative + profile.mkdir(exist_ok=True) + (profile / "lean-toolchain").write_text(pin + "\n") + (profile / "lakefile.toml").write_text(relative) + (profile / "lake-manifest.json").write_text(relative) + (root / "supported-toolchains.json").write_text(json.dumps({ + "default": "leanprover/lean4:v4.36.0-rc2", "stable": "leanprover/lean4:v4.35.0", + "configurations": { + "leanprover/lean4:v4.36.0-rc2": ".", "leanprover/lean4:v4.35.0": "stable"}})) + + def test_isolated_copy_selects_stable_and_excludes_build_state(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) / "benchmark" + root.mkdir() + self.fixture(root) + (root / ".lake").mkdir() + (root / ".lake/secret-cache").write_text("old artifacts") + destination = root / ".lake/stable-copy" + MODULE.prepare(root, "stable", destination) + self.assertEqual((destination / "lakefile.toml").read_text(), "stable") + self.assertFalse((destination / ".lake").exists()) + self.assertEqual((root / "lakefile.toml").read_text(), ".") + with self.assertRaisesRegex(ValueError, "already exists"): + MODULE.prepare(root, "stable", destination) + with self.assertRaisesRegex(ValueError, "fresh checkout"): + MODULE.prepare(root, "stable") + + def test_unsupported_toolchains_and_escaping_configurations_are_rejected(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + self.fixture(root) + with self.assertRaisesRegex(ValueError, "unsupported"): + MODULE.prepare(root, "leanprover/lean4:nightly") + registry = root / "supported-toolchains.json" + value = json.loads(registry.read_text()) + value["configurations"][value["default"]] = "../outside" + registry.write_text(json.dumps(value)) + with self.assertRaisesRegex(ValueError, "escapes"): + MODULE.prepare(root, "stable") + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/python/test_select_ci_problems.py b/tests/python/test_select_ci_problems.py index 5f7c14efe..21b577229 100644 --- a/tests/python/test_select_ci_problems.py +++ b/tests/python/test_select_ci_problems.py @@ -82,6 +82,14 @@ def test_solution_dependency_change_regenerates_every_workspace(self): self.assertEqual(selection.mode, "full") self.assertTrue(selection.source_changed) + def test_toolchain_configuration_changes_compile_the_full_catalog(self): + for path in ["supported-toolchains.json", "toolchains/v4.35.0/lake-manifest.json", + "scripts/prepare_toolchain.py", "scripts/select_submission_toolchain.py"]: + with self.subTest(path=path): + selection = self.select((Change("M", (path,)),)) + self.assertEqual(selection.mode, "full") + self.assertEqual(selection.problems, ("a", "b", "b_second", "c")) + def test_tag_registry_change_is_a_full_catalog_sentinel(self): selection = self.select((Change("M", ("manifests/tags.toml",)),)) self.assertEqual(selection.mode, "full") diff --git a/tests/python/test_select_submission_toolchain.py b/tests/python/test_select_submission_toolchain.py new file mode 100644 index 000000000..12a5fb64d --- /dev/null +++ b/tests/python/test_select_submission_toolchain.py @@ -0,0 +1,121 @@ +from __future__ import annotations + +import importlib.util +import io +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tarfile +import tempfile +import unittest +from unittest import mock + + +ROOT = Path(__file__).resolve().parents[2] +sys.path.insert(0, str(ROOT / "scripts")) +SPEC = importlib.util.spec_from_file_location("select_submission_toolchain", + ROOT / "scripts/select_submission_toolchain.py") +MODULE = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(MODULE) + + +class SelectSubmissionToolchainTests(unittest.TestCase): + def setUp(self): + temporary = tempfile.TemporaryDirectory() + self.addCleanup(temporary.cleanup) + self.root = Path(temporary.name) + (self.root / "manifests/problems").mkdir(parents=True) + for problem in ("a", "b"): + (self.root / f"manifests/problems/{problem}.toml").write_text("") + (self.root / f"generated/{problem}").mkdir(parents=True) + (self.root / f"generated/{problem}/Submission.lean").write_text("-- stub\n") + for relative, pin in [("rc", "v4.36.0-rc2"), ("stable", "v4.35.0")]: + profile = self.root / relative + profile.mkdir() + for name in ["lean-toolchain", "lakefile.toml", "lake-manifest.json"]: + (profile / name).write_text("leanprover/lean4:" + pin if name == "lean-toolchain" else "{}") + (self.root / "supported-toolchains.json").write_text(json.dumps({ + "default": "leanprover/lean4:v4.36.0-rc2", "stable": "leanprover/lean4:v4.35.0", + "configurations": { + "leanprover/lean4:v4.36.0-rc2": "rc", "leanprover/lean4:v4.35.0": "stable"}})) + + def archive(self, files): + archive = self.root / "source.tar.gz" + with tarfile.open(archive, "w:gz") as output: + for name, value in files: + member = tarfile.TarInfo(name) + if value is None: + member.type = tarfile.SYMTYPE + member.linkname = "/etc/passwd" + output.addfile(member) + else: + data = value.encode() + member.size = len(data) + output.addfile(member, io.BytesIO(data)) + return archive + + def workspace(self, problem="a", prefix="source/generated/a"): + return [(prefix + "/lakefile.toml", f'name = "{problem}"'), + (prefix + "/Submission.lean", "-- proof\n")] + + def test_root_pin_and_nearest_workspace_pin_select_approved_configurations(self): + files = [("source/lean-toolchain", "leanprover/lean4:v4.35.0")] + self.workspace() + selected, problems = MODULE.select(self.archive(files), self.root) + self.assertEqual(selected, "leanprover/lean4:v4.35.0") + self.assertEqual(problems, ["a"]) + files.append(("source/generated/a/lean-toolchain", "leanprover/lean4:v4.36.0-rc2")) + self.assertEqual(MODULE.select(self.archive(files), self.root)[0], + "leanprover/lean4:v4.36.0-rc2") + + def test_pristine_workspaces_and_other_selected_problems_do_not_choose_toolchains(self): + files = self.workspace() + [("source/generated/a/lean-toolchain", "leanprover/lean4:v4.35.0")] + files += self.workspace("b", "source/generated/b") + files += [("source/generated/b/lean-toolchain", "leanprover/lean4:v4.36.0-rc2")] + archive = self.archive(files) + with self.assertRaisesRegex(ValueError, "one toolchain"): + MODULE.select(archive, self.root) + self.assertEqual(MODULE.select(archive, self.root, "a")[0], "leanprover/lean4:v4.35.0") + files = [(path, "-- stub\n" if path == "source/generated/b/Submission.lean" else content) + for path, content in files] + self.assertEqual(MODULE.select(self.archive(files), self.root)[1], ["a"]) + + def test_unsupported_pins_escaping_paths_symlinks_and_duplicates_fail_closed(self): + cases = [self.workspace() + [("source/lean-toolchain", "leanprover/lean4:nightly")], + [("../lean-toolchain", "ignored")], self.workspace() + [("source/lean-toolchain", None)], + [("source/lean-toolchain", "a"), ("source/lean-toolchain", "b")], + self.workspace() + [("source/lean-toolchain", "a" * 257)]] + for files in cases: + with self.subTest(files=files), self.assertRaises(ValueError): + MODULE.select(self.archive(files), self.root) + + def test_archive_retains_unsupported_requests_but_evaluation_rejects_them(self): + scripts = self.root / "scripts" + scripts.mkdir() + for name in ["prepare_toolchain.py", "select_submission_toolchain.py"]: + shutil.copyfile(ROOT / "scripts" / name, scripts / name) + archive = self.archive(self.workspace() + [ + ("source/lean-toolchain", "leanprover/lean4:nightly")]) + command = [sys.executable, str(scripts / "select_submission_toolchain.py"), + "--source-tar", str(archive)] + archived = subprocess.run([*command, "--archive"], capture_output=True, text=True) + self.assertEqual(archived.returncode, 0, archived.stderr) + self.assertEqual(archived.stdout.strip(), "leanprover/lean4:v4.36.0-rc2") + evaluated = subprocess.run([*command, "--expected", archived.stdout.strip()], + capture_output=True, text=True) + self.assertNotEqual(evaluated.returncode, 0) + self.assertIn("unsupported requested toolchain", evaluated.stderr) + + def test_parser_recursion_is_an_input_rejection_and_unused_symlinks_are_ignored(self): + with mock.patch.object(MODULE, "source_requests", side_effect=RecursionError("nested TOML")): + with self.assertRaises(MODULE.ToolchainRequestError): + MODULE.select(self.root / "source.tar.gz", self.root) + files = self.workspace() + [("source/lean-toolchain", "leanprover/lean4:v4.35.0"), + ("source/vendor/lakefile.toml", None), + ("source/vendor/lean-toolchain", None)] + self.assertEqual(MODULE.select(self.archive(files), self.root)[0], "leanprover/lean4:v4.35.0") + + +if __name__ == "__main__": + unittest.main() diff --git a/toolchains/v4.35.0/lake-manifest.json b/toolchains/v4.35.0/lake-manifest.json new file mode 100644 index 000000000..50c8e82ba --- /dev/null +++ b/toolchains/v4.35.0/lake-manifest.json @@ -0,0 +1,177 @@ +{ + "version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "074063781836922cb02701cd12943c9f51731afa", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "074063781836922cb02701cd12943c9f51731afa", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4a174c490d8707121c4a9290800489f105d85e07", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.35.0", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover/lean-eval-generator.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0b8cc2d141710a18515c53448f006c971dd8eeb4", + "name": "\u00ablean-eval-generator\u00bb", + "manifestFile": "lake-manifest.json", + "inputRev": "0b8cc2d141710a18515c53448f006c971dd8eeb4", + "inherited": false, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/TauCetiProject/TauCeti", + "type": "git", + "subDir": null, + "scope": "", + "rev": "1f9b4414105d86e487a4ac4c3d3397076a44d0d2", + "name": "TauCeti", + "manifestFile": "lake-manifest.json", + "inputRev": "1f9b4414105d86e487a4ac4c3d3397076a44d0d2", + "inherited": false, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/AxiomMath/Stacks.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c496df0d9beea9deaeabcea8492605f9a0a2313b", + "name": "Stacks", + "manifestFile": "lake-manifest.json", + "inputRev": "c496df0d9beea9deaeabcea8492605f9a0a2313b", + "inherited": false, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/AxiomMath/CFSG.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33", + "name": "cfsg", + "manifestFile": "lake-manifest.json", + "inputRev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33", + "inherited": false, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/Vilin97/lean-pool.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f", + "name": "\u00ablean-pool\u00bb", + "manifestFile": "lake-manifest.json", + "inputRev": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f", + "inherited": false, + "configFile": "lakefile.toml" + } + ], + "name": "\u00ablean-eval\u00bb", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/toolchains/v4.35.0/lakefile.toml b/toolchains/v4.35.0/lakefile.toml new file mode 100644 index 000000000..8be7b072e --- /dev/null +++ b/toolchains/v4.35.0/lakefile.toml @@ -0,0 +1,87 @@ +name = "lean-eval" +defaultTargets = ["LeanEval"] +# Generated benchmark statements retain legacy visibility rules. +allowNonModules = true + +[leanOptions] +autoImplicit = false + +# Available to generated solutions only. Generation rejects statement imports +# from lean-pool; keep this before Mathlib so Mathlib owns shared pins. +[[require]] +name = "lean-pool" +git = "https://github.com/Vilin97/lean-pool.git" +rev = "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f" + +# Large solution libraries. Their caches are fetched only when imported. +# Keep these before TauCeti and Mathlib so the benchmark owns shared pins. +# Their published pins currently predate this toolchain; cache preparation +# rejects imports until the publishers provide matching builds (see README). +[[require]] +name = "cfsg" +git = "https://github.com/AxiomMath/CFSG.git" +rev = "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33" + +[[require]] +name = "Stacks" +git = "https://github.com/AxiomMath/Stacks.git" +rev = "c496df0d9beea9deaeabcea8492605f9a0a2313b" + +# TauCeti supplies the definitions in the classification of finite simple groups +# problem. It is listed before Mathlib because Lake takes shared transitive +# dependencies (batteries, aesop, ...) from the later require, and those must be +# Mathlib's. The toolchain and the Mathlib rev below must be exactly the ones the +# pinned TauCeti commit uses, so that TauCeti's published build outputs apply; +# scripts/fetch_dependency_caches.sh checks this and fetches them. +[[require]] +name = "TauCeti" +git = "https://github.com/TauCetiProject/TauCeti" +rev = "1f9b4414105d86e487a4ac4c3d3397076a44d0d2" + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "074063781836922cb02701cd12943c9f51731afa" + +[[require]] +name = "lean-eval-generator" +git = "https://github.com/leanprover/lean-eval-generator.git" +rev = "0b8cc2d141710a18515c53448f006c971dd8eeb4" + +[[lean_lib]] +name = "LeanEval" + +[[lean_lib]] +name = "EvalTools" + +[[lean_exe]] +name = "extract_theorem" +root = "EvalTools.ExtractTheorem" + +[[lean_exe]] +name = "eval_inventory" +root = "EvalTools.ProblemInventory" + +[[lean_exe]] +name = "lean-eval" +root = "EvalTools.Main" + +[[lean_exe]] +name = "test_validate_submission" +srcDir = "tests/lean" +root = "EvalToolsTests.ValidateSubmissionTest" + +[[lean_exe]] +name = "test_check_comparator_installation" +srcDir = "tests/lean" +root = "EvalToolsTests.CheckComparatorInstallationTest" + +[[lean_exe]] +name = "test_generate" +srcDir = "tests/lean" +root = "EvalToolsTests.GenerateTest" + +[[lean_exe]] +name = "test_module_coverage" +srcDir = "tests/lean" +root = "EvalToolsTests.ModuleCoverageTest" diff --git a/toolchains/v4.35.0/lean-toolchain b/toolchains/v4.35.0/lean-toolchain new file mode 100644 index 000000000..a6aff065d --- /dev/null +++ b/toolchains/v4.35.0/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.35.0 diff --git a/toolchains/v4.36.0-rc2/lake-manifest.json b/toolchains/v4.36.0-rc2/lake-manifest.json new file mode 100644 index 000000000..50817ff4e --- /dev/null +++ b/toolchains/v4.36.0-rc2/lake-manifest.json @@ -0,0 +1,146 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover/lean-eval-generator.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0b8cc2d141710a18515c53448f006c971dd8eeb4", + "name": "«lean-eval-generator»", + "manifestFile": "lake-manifest.json", + "inputRev": "0b8cc2d141710a18515c53448f006c971dd8eeb4", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/TauCetiProject/TauCeti", + "type": "git", + "subDir": null, + "scope": "", + "rev": "be86813dc92e6bac8614c2c2dd34572145df09c0", + "name": "TauCeti", + "manifestFile": "lake-manifest.json", + "inputRev": "be86813dc92e6bac8614c2c2dd34572145df09c0", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/AxiomMath/Stacks.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c496df0d9beea9deaeabcea8492605f9a0a2313b", + "name": "Stacks", + "manifestFile": "lake-manifest.json", + "inputRev": "c496df0d9beea9deaeabcea8492605f9a0a2313b", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/AxiomMath/CFSG.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33", + "name": "cfsg", + "manifestFile": "lake-manifest.json", + "inputRev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/Vilin97/lean-pool.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f", + "name": "«lean-pool»", + "manifestFile": "lake-manifest.json", + "inputRev": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c61286b7b63cbfd563b28e11e81d0a18233a044a", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e5d5639bedc7feecfbcb98e30b3bf26463d9f722", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "16259c0d07d61ee37d999d05b5cf96338b8daa11", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "7d11bfa88558f8d3d90afdf6bd877ed70001498d", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b0256621cb88178e9ad932a53633077b3029e621", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4af7237d146261353907b06a01b6f3fc06cfa067", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.36.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "«lean-eval»", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/toolchains/v4.36.0-rc2/lakefile.toml b/toolchains/v4.36.0-rc2/lakefile.toml new file mode 100644 index 000000000..5e17c52ac --- /dev/null +++ b/toolchains/v4.36.0-rc2/lakefile.toml @@ -0,0 +1,87 @@ +name = "lean-eval" +defaultTargets = ["LeanEval"] +# Generated benchmark statements retain legacy visibility rules. +allowNonModules = true + +[leanOptions] +autoImplicit = false + +# Available to generated solutions only. Generation rejects statement imports +# from lean-pool; keep this before Mathlib so Mathlib owns shared pins. +[[require]] +name = "lean-pool" +git = "https://github.com/Vilin97/lean-pool.git" +rev = "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f" + +# Large solution libraries. Their caches are fetched only when imported. +# Keep these before TauCeti and Mathlib so the benchmark owns shared pins. +# Their published pins currently predate this toolchain; cache preparation +# rejects imports until the publishers provide matching builds (see README). +[[require]] +name = "cfsg" +git = "https://github.com/AxiomMath/CFSG.git" +rev = "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33" + +[[require]] +name = "Stacks" +git = "https://github.com/AxiomMath/Stacks.git" +rev = "c496df0d9beea9deaeabcea8492605f9a0a2313b" + +# TauCeti supplies the definitions in the classification of finite simple groups +# problem. It is listed before Mathlib because Lake takes shared transitive +# dependencies (batteries, aesop, ...) from the later require, and those must be +# Mathlib's. The toolchain and the Mathlib rev below must be exactly the ones the +# pinned TauCeti commit uses, so that TauCeti's published build outputs apply; +# scripts/fetch_dependency_caches.sh checks this and fetches them. +[[require]] +name = "TauCeti" +git = "https://github.com/TauCetiProject/TauCeti" +rev = "be86813dc92e6bac8614c2c2dd34572145df09c0" + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "2ddf59c8f14245864e6c0ed227a2dab76b9efea2" + +[[require]] +name = "lean-eval-generator" +git = "https://github.com/leanprover/lean-eval-generator.git" +rev = "0b8cc2d141710a18515c53448f006c971dd8eeb4" + +[[lean_lib]] +name = "LeanEval" + +[[lean_lib]] +name = "EvalTools" + +[[lean_exe]] +name = "extract_theorem" +root = "EvalTools.ExtractTheorem" + +[[lean_exe]] +name = "eval_inventory" +root = "EvalTools.ProblemInventory" + +[[lean_exe]] +name = "lean-eval" +root = "EvalTools.Main" + +[[lean_exe]] +name = "test_validate_submission" +srcDir = "tests/lean" +root = "EvalToolsTests.ValidateSubmissionTest" + +[[lean_exe]] +name = "test_check_comparator_installation" +srcDir = "tests/lean" +root = "EvalToolsTests.CheckComparatorInstallationTest" + +[[lean_exe]] +name = "test_generate" +srcDir = "tests/lean" +root = "EvalToolsTests.GenerateTest" + +[[lean_exe]] +name = "test_module_coverage" +srcDir = "tests/lean" +root = "EvalToolsTests.ModuleCoverageTest" diff --git a/toolchains/v4.36.0-rc2/lean-toolchain b/toolchains/v4.36.0-rc2/lean-toolchain new file mode 100644 index 000000000..0fc433692 --- /dev/null +++ b/toolchains/v4.36.0-rc2/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.36.0-rc2 From c3dc11bee60ad5156267047d747aa6b716d046e7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 13 Nov 2026 09:41:44 +0000 Subject: [PATCH 4/7] Normalize implicit default toolchains when combining source workspaces --- scripts/select_submission_toolchain.py | 9 ++++++--- tests/python/test_select_submission_toolchain.py | 6 ++++++ 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/scripts/select_submission_toolchain.py b/scripts/select_submission_toolchain.py index e6984496c..8f073f102 100644 --- a/scripts/select_submission_toolchain.py +++ b/scripts/select_submission_toolchain.py @@ -22,7 +22,8 @@ class ToolchainRequestError(ValueError): """Archived source cannot select an approved evaluation configuration.""" -def source_requests(archive: Path, root: Path, problem: str | None = None) -> dict[str, str | None]: +def source_requests(archive: Path, root: Path, default: str, + problem: str | None = None) -> dict[str, str | None]: known = {p.stem for p in (root / "manifests/problems").glob("*.toml")} if problem is not None: if problem not in known: @@ -81,7 +82,9 @@ def source_requests(archive: Path, root: Path, problem: str | None = None) -> di if parent in pins), None) if isinstance(requested, ValueError): raise requested - if name in result and result[name] != requested: + previous = result.get(name) + if name in result and (default if previous is None else previous) != ( + default if requested is None else requested): raise ValueError(f"multiple toolchains requested for {name}") result[name] = requested return result @@ -90,7 +93,7 @@ def source_requests(archive: Path, root: Path, problem: str | None = None) -> di def select(archive: Path, root: Path, problem: str | None = None) -> tuple[str, list[str]]: default, supported = configurations(root) try: - requests = source_requests(archive, root, problem) + requests = source_requests(archive, root, default, problem) except Exception as error: # TOML and archive readers can also raise RecursionError or resource # errors on malformed source. No source parser failure may block its diff --git a/tests/python/test_select_submission_toolchain.py b/tests/python/test_select_submission_toolchain.py index 12a5fb64d..5162a7f1f 100644 --- a/tests/python/test_select_submission_toolchain.py +++ b/tests/python/test_select_submission_toolchain.py @@ -81,6 +81,12 @@ def test_pristine_workspaces_and_other_selected_problems_do_not_choose_toolchain for path, content in files] self.assertEqual(MODULE.select(self.archive(files), self.root)[1], ["a"]) + def test_an_implicit_and_explicit_default_are_the_same_configuration(self): + files = self.workspace() + self.workspace("a", "source/another-a") + files.append(("source/another-a/lean-toolchain", "leanprover/lean4:v4.36.0-rc2")) + self.assertEqual(MODULE.select(self.archive(files), self.root), + ("leanprover/lean4:v4.36.0-rc2", ["a"])) + def test_unsupported_pins_escaping_paths_symlinks_and_duplicates_fail_closed(self): cases = [self.workspace() + [("source/lean-toolchain", "leanprover/lean4:nightly")], [("../lean-toolchain", "ignored")], self.workspace() + [("source/lean-toolchain", None)], From bace2286676342f7b1d068ca69c827bf81de42fc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 13 Nov 2026 13:04:11 +0000 Subject: [PATCH 5/7] Parse the CI import graph without materializing package dependencies --- .github/workflows/ci.yml | 6 +-- EvalTools/CIImportGraph.lean | 2 +- EvalTools/ModuleCoverage.lean | 61 +----------------------------- EvalTools/ProblemSources.lean | 71 +++++++++++++++++++++++++++++++++++ 4 files changed, 76 insertions(+), 64 deletions(-) create mode 100644 EvalTools/ProblemSources.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2a17ff5a2..7bf701e2e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -76,9 +76,9 @@ jobs: - name: Export Lean import graph run: | set -euo pipefail - mkdir -p .ci - lake build EvalTools.CIImportGraph - lake env lean --run EvalTools/CIImportGraph.lean > .ci/import-graph.json + mkdir -p .ci/EvalTools + lean -o .ci/EvalTools/ProblemSources.olean EvalTools/ProblemSources.lean + LEAN_PATH="$PWD/.ci" lean --run EvalTools/CIImportGraph.lean > .ci/import-graph.json - name: Select affected catalog problems id: changes diff --git a/EvalTools/CIImportGraph.lean b/EvalTools/CIImportGraph.lean index 2b10c9f3f..cb677b03e 100644 --- a/EvalTools/CIImportGraph.lean +++ b/EvalTools/CIImportGraph.lean @@ -1,4 +1,4 @@ -import EvalTools.ModuleCoverage +import EvalTools.ProblemSources open Lean diff --git a/EvalTools/ModuleCoverage.lean b/EvalTools/ModuleCoverage.lean index 0666b70f0..342e96a82 100644 --- a/EvalTools/ModuleCoverage.lean +++ b/EvalTools/ModuleCoverage.lean @@ -1,4 +1,4 @@ -import Lean +import EvalTools.ProblemSources import EvalTools.Markers open Lean @@ -9,26 +9,6 @@ open LeanEvalGenerator.Core set_option autoImplicit false -/-- Directory holding the trusted problem sources, relative to the repository -root. Its module prefix is the directory name. -/ -def problemSourceRelativePath : System.FilePath := "LeanEval" - -/-- A `.lean` file under `LeanEval/`, together with the modules its header -imports. - -Module identity is a `Name`, not a string: `LeanEval/Foo/Bar.lean` is -`LeanEval.Foo.Bar` while `LeanEval/Foo.Bar.lean` is `LeanEval.«Foo.Bar»`, and -flattening either to text would conflate two distinct files. -/ -structure ProblemSourceModule where - /-- Fully qualified module name, for example - `LeanEval.Geometry.JacobianChallenge`. -/ - name : Name - /-- Path of the file, relative to the repository root. -/ - path : String - /-- The modules named in the file's `import` header. -/ - imports : Array Name - deriving Inhabited, Repr - private def sourcesByName (sources : Array ProblemSourceModule) : Std.HashMap Name ProblemSourceModule := sources.foldl (fun m source => m.insert source.name source) ∅ @@ -55,45 +35,6 @@ def unreachableModules (sources : Array ProblemSourceModule) (roots : Array Name sources.filterMap fun source => if reached.contains source.name then none else some source.name -/-- Recursively collect the `.lean` files under `dir`, reading each header for -its imports. `relDir` and `modulePrefix` describe `dir` itself. -/ -private partial def collectSourceModules (dir : System.FilePath) (relDir : String) - (modulePrefix : Name) : IO (Array ProblemSourceModule) := do - let entries := (← dir.readDir).qsort fun a b => a.fileName < b.fileName - let mut out : Array ProblemSourceModule := #[] - for entry in entries do - let relPath := s!"{relDir}/{entry.fileName}" - -- `symlinkMetadata` rather than `isDir`: the latter follows links, so a - -- directory symlink could duplicate a subtree under a second module prefix, - -- or point at an ancestor and recurse forever. - match (← entry.path.symlinkMetadata).type with - | .symlink => - throw <| IO.userError - s!"`{relPath}` is a symbolic link. Problem sources must be regular files and \ - directories, so that a file's path determines its module name." - | .dir => - out := out ++ (← collectSourceModules entry.path relPath (modulePrefix.str entry.fileName)) - | _ => - if entry.path.extension == some "lean" then - let stem := (entry.fileName.dropEnd 5).toString - let header ← parseImports' (← IO.FS.readFile entry.path) entry.path.toString - out := out.push - { name := modulePrefix.str stem - path := relPath - imports := header.imports.map (·.module) } - return out - -/-- Load every source module under `LeanEval/`, using Lean's own module-header -parser to identify imports. This is shared by module-coverage validation and -the CI dependency selector so they cannot disagree about Lean import syntax. -/ -def loadProblemSourceModules (root : System.FilePath) : IO (Array ProblemSourceModule) := do - let sourceRoot := root / problemSourceRelativePath - unless ← sourceRoot.isDir do - throw <| IO.userError - s!"Problem source directory `{sourceRoot}` does not exist or is not a directory." - let prefixName := problemSourceRelativePath.toString - collectSourceModules sourceRoot prefixName (.str .anonymous prefixName) - /-- Fail unless every `.lean` file under `LeanEval/` is reachable from the manifest: either named by some entry's `module` field, or imported (directly or transitively) by a module that is. diff --git a/EvalTools/ProblemSources.lean b/EvalTools/ProblemSources.lean new file mode 100644 index 000000000..da4f11491 --- /dev/null +++ b/EvalTools/ProblemSources.lean @@ -0,0 +1,71 @@ +import Lean + +open Lean + +namespace EvalTools + +set_option autoImplicit false + +/-- Directory holding the trusted problem sources, relative to the repository +root. Its module prefix is the directory name. -/ +def problemSourceRelativePath : System.FilePath := "LeanEval" + +/-- A `.lean` file under `LeanEval/`, together with the modules its header +imports. + +Module identity is a `Name`, not a string: `LeanEval/Foo/Bar.lean` is +`LeanEval.Foo.Bar` while `LeanEval/Foo.Bar.lean` is `LeanEval.«Foo.Bar»`, and +flattening either to text would conflate two distinct files. -/ +structure ProblemSourceModule where + /-- Fully qualified module name, for example + `LeanEval.Geometry.JacobianChallenge`. -/ + name : Name + /-- Path of the file, relative to the repository root. -/ + path : String + /-- The modules named in the file's `import` header. -/ + imports : Array Name + deriving Inhabited, Repr + +/-- Recursively collect the `.lean` files under `dir`, reading each header for +its imports. `relDir` and `modulePrefix` describe `dir` itself. -/ +private partial def collectSourceModules (dir : System.FilePath) (relDir : String) + (modulePrefix : Name) : IO (Array ProblemSourceModule) := do + let entries := (← dir.readDir).qsort fun a b => a.fileName < b.fileName + let mut out : Array ProblemSourceModule := #[] + for entry in entries do + let relPath := s!"{relDir}/{entry.fileName}" + -- `symlinkMetadata` rather than `isDir`: the latter follows links, so a + -- directory symlink could duplicate a subtree under a second module prefix, + -- or point at an ancestor and recurse forever. + match (← entry.path.symlinkMetadata).type with + | .symlink => + throw <| IO.userError + s!"`{relPath}` is a symbolic link. Problem sources must be regular files and \ + directories, so that a file's path determines its module name." + | .dir => + out := out ++ (← collectSourceModules entry.path relPath (modulePrefix.str entry.fileName)) + | _ => + if entry.path.extension == some "lean" then + let stem := (entry.fileName.dropEnd 5).toString + let (header, _, messages) ← Lean.Elab.parseImports (← IO.FS.readFile entry.path) + entry.path.toString + if messages.hasErrors then + throw <| IO.userError s!"Invalid import header in {relPath}: {← messages.toList.toArray.mapM (·.toString)}" + out := out.push + { name := modulePrefix.str stem + path := relPath + imports := header.map (·.module) } + return out + +/-- Load every source module under `LeanEval/`, using Lean's own module-header +parser to identify imports. This is shared by module-coverage validation and +the CI dependency selector so they cannot disagree about Lean import syntax. -/ +def loadProblemSourceModules (root : System.FilePath) : IO (Array ProblemSourceModule) := do + let sourceRoot := root / problemSourceRelativePath + unless ← sourceRoot.isDir do + throw <| IO.userError + s!"Problem source directory `{sourceRoot}` does not exist or is not a directory." + let prefixName := problemSourceRelativePath.toString + collectSourceModules sourceRoot prefixName (.str .anonymous prefixName) + +end EvalTools From 787927e9be87115a3cea6762ae9d1d9f41f4f834 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 13 Nov 2026 14:04:11 +0000 Subject: [PATCH 6/7] Keep CI package preparation within its validation deadlines --- .github/workflows/ci.yml | 17 ++++- SECURITY.md | 5 ++ scripts/prepare_ci_dependencies.py | 67 ++++++++++++++++++++ scripts/select_ci_problems.py | 1 + tests/python/test_prepare_ci_dependencies.py | 60 ++++++++++++++++++ tests/python/test_select_ci_problems.py | 3 +- 6 files changed, 151 insertions(+), 2 deletions(-) create mode 100644 scripts/prepare_ci_dependencies.py create mode 100644 tests/python/test_prepare_ci_dependencies.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7bf701e2e..3c0d9dc5e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -121,6 +121,9 @@ jobs: fetch-depth: 0 persist-credentials: false + - name: Prepare solution-only package metadata + run: python scripts/prepare_ci_dependencies.py + # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04). - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: @@ -225,6 +228,9 @@ jobs: - name: Select benchmark configuration run: python scripts/prepare_toolchain.py "${{ matrix.configuration }}" --apply + - name: Prepare solution-only package metadata + run: python scripts/prepare_ci_dependencies.py + # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04). - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: @@ -310,6 +316,9 @@ jobs: fetch-depth: 0 persist-credentials: false + - name: Prepare solution-only package metadata + run: python scripts/prepare_ci_dependencies.py + # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04). - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: @@ -442,6 +451,9 @@ jobs: - name: Select stable toolchain and dependency pins run: python scripts/prepare_toolchain.py stable --apply + - name: Prepare solution-only package metadata + run: python scripts/prepare_ci_dependencies.py + # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04). - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: @@ -484,7 +496,7 @@ jobs: needs: [classify, catalog] if: needs.classify.outputs.run_catalog == 'true' runs-on: ubuntu-latest - timeout-minutes: 15 + timeout-minutes: 30 steps: - name: Free up disk space # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04). @@ -504,6 +516,9 @@ jobs: with: persist-credentials: false + - name: Prepare solution-only package metadata + run: python scripts/prepare_ci_dependencies.py + # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04). - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: diff --git a/SECURITY.md b/SECURITY.md index cb80c7a83..0f04e17a3 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -137,6 +137,11 @@ The generator rejects Lean Pool, CFSG, and Stacks imports in trusted statements and helpers while making their pinned source available to solutions. Cache preparation parses submission headers without elaborating them and restores only registered library targets with `lake --no-build`. Maintain that separation. +Benchmark CI checks out only package metadata for the solution-only CFSG and +Stacks dependencies using `scripts/prepare_ci_dependencies.py`. Their real +pinned Lake configuration and manifests remain available; the generator's +statement-import prohibition remains enforced. Submission evaluation uses full +source checkouts and never invokes this CI-only preparation helper. Historical replay locks and instrumentation are versioned independently; do not silently change their verifier or metric semantics. diff --git a/scripts/prepare_ci_dependencies.py b/scripts/prepare_ci_dependencies.py new file mode 100644 index 000000000..6dc2d6e31 --- /dev/null +++ b/scripts/prepare_ci_dependencies.py @@ -0,0 +1,67 @@ +#!/usr/bin/env python3 +"""Materialize only package metadata for solution-only CFSG/Stacks CI dependencies. + +Trusted problem sources cannot import these packages. Their source trees are +therefore unnecessary for catalog generation, statement builds, and verifier +probes. Lake still reads their real, pinned package configuration and manifest. +This helper is for benchmark CI only; submission preparation uses full sources. +""" +from __future__ import annotations + +import argparse +import json +from pathlib import Path +import re +import subprocess +import sys + + +PACKAGES = frozenset({"cfsg", "Stacks"}) +METADATA = ("lakefile.toml", "lakefile.lean", "lake-manifest.json", "lean-toolchain") + + +def git(directory: Path, *arguments: str) -> None: + subprocess.run(["git", "-C", str(directory), *arguments], check=True) + + +def prepare(root: Path) -> None: + policy = json.loads((root / "solution-dependencies.json").read_text()) + allowed = {entry["name"] for entry in policy} + if not PACKAGES <= allowed: + raise ValueError("metadata-only packages must be forbidden in trusted statement imports") + manifest = json.loads((root / "lake-manifest.json").read_text()) + packages = {p["name"].strip("«»"): p for p in manifest["packages"]} + for name in sorted(PACKAGES): + package = packages[name] + revision = package["rev"] + if re.fullmatch(r"[0-9a-f]{40}", revision) is None: + raise ValueError(f"{name} is not pinned to an exact commit") + destination = root / ".lake/packages" / name + if destination.exists() or destination.is_symlink(): + raise ValueError(f"expected a fresh CI checkout; {destination} already exists") + destination.mkdir(parents=True) + git(destination, "init", "--quiet", "--initial-branch=main") + git(destination, "remote", "add", "origin", package["url"]) + git(destination, "sparse-checkout", "set", "--no-cone", + *("/" + name for name in METADATA)) + git(destination, "fetch", "--quiet", "--filter=tree:0", "--depth=1", "--no-tags", + "origin", revision) + git(destination, "checkout", "--quiet", "--detach", revision) + if not (destination / "lake-manifest.json").is_file(): + raise ValueError(f"{name} does not publish its dependency manifest") + print(f"Prepared {name} package metadata at {revision}") + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=Path(__file__).resolve().parents[1]) + args = parser.parse_args() + try: + prepare(args.root) + except (OSError, ValueError, KeyError, subprocess.CalledProcessError) as error: + parser.exit(1, f"prepare_ci_dependencies: {error}\n") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/select_ci_problems.py b/scripts/select_ci_problems.py index 21699ca54..85e439a85 100644 --- a/scripts/select_ci_problems.py +++ b/scripts/select_ci_problems.py @@ -187,6 +187,7 @@ def is_full_catalog_sentinel(path: str) -> bool: or path == "manifests/tags.toml" or path == "scripts/select_ci_problems.py" or path == "scripts/prepare_toolchain.py" + or path == "scripts/prepare_ci_dependencies.py" or path == "scripts/select_submission_toolchain.py" or path == "supported-toolchains.json" or path.startswith("toolchains/") diff --git a/tests/python/test_prepare_ci_dependencies.py b/tests/python/test_prepare_ci_dependencies.py new file mode 100644 index 000000000..4b28909ae --- /dev/null +++ b/tests/python/test_prepare_ci_dependencies.py @@ -0,0 +1,60 @@ +from __future__ import annotations + +import importlib.util +import json +from pathlib import Path +import subprocess +import tempfile +import unittest + + +ROOT = Path(__file__).resolve().parents[2] +SPEC = importlib.util.spec_from_file_location("prepare_ci_dependencies", + ROOT / "scripts/prepare_ci_dependencies.py") +MODULE = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(MODULE) + + +class PrepareCIDependenciesTests(unittest.TestCase): + def test_pinned_metadata_is_real_and_solution_sources_are_not_materialized(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + source = root / "source" + source.mkdir() + subprocess.run(["git", "init", "--quiet", "--initial-branch=main", str(source)], check=True) + subprocess.run(["git", "-C", str(source), "config", "uploadpack.allowFilter", "true"], check=True) + (source / "lakefile.toml").write_text('name = "example"\n') + (source / "lake-manifest.json").write_text('{"packages": []}\n') + (source / "lean-toolchain").write_text("leanprover/lean4:v4.35.0\n") + (source / "Example.lean").write_text("def largeSolutionLibrary := 42\n") + subprocess.run(["git", "-C", str(source), "add", "."], check=True) + subprocess.run(["git", "-C", str(source), "-c", "user.name=Tests", "-c", + "user.email=tests@example.invalid", "commit", "--quiet", "-m", "fixture"], + check=True) + revision = subprocess.check_output(["git", "-C", str(source), "rev-parse", "HEAD"], + text=True).strip() + (root / "solution-dependencies.json").write_text(json.dumps([ + {"name": name} for name in MODULE.PACKAGES])) + (root / "lake-manifest.json").write_text(json.dumps({"packages": [ + {"name": name, "url": str(source), "rev": revision} for name in MODULE.PACKAGES]})) + MODULE.prepare(root) + for name in MODULE.PACKAGES: + package = root / ".lake/packages" / name + self.assertEqual((package / "lakefile.toml").read_bytes(), + (source / "lakefile.toml").read_bytes()) + self.assertFalse((package / "Example.lean").exists()) + self.assertEqual(subprocess.check_output( + ["git", "-C", str(package), "rev-parse", "HEAD"], text=True).strip(), revision) + with self.assertRaisesRegex(ValueError, "fresh CI checkout"): + MODULE.prepare(root) + + def test_only_solution_only_packages_may_have_their_sources_omitted(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + (root / "solution-dependencies.json").write_text("[]") + with self.assertRaisesRegex(ValueError, "trusted statement imports"): + MODULE.prepare(root) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/python/test_select_ci_problems.py b/tests/python/test_select_ci_problems.py index 21b577229..a6d5a9ff3 100644 --- a/tests/python/test_select_ci_problems.py +++ b/tests/python/test_select_ci_problems.py @@ -84,7 +84,8 @@ def test_solution_dependency_change_regenerates_every_workspace(self): def test_toolchain_configuration_changes_compile_the_full_catalog(self): for path in ["supported-toolchains.json", "toolchains/v4.35.0/lake-manifest.json", - "scripts/prepare_toolchain.py", "scripts/select_submission_toolchain.py"]: + "scripts/prepare_toolchain.py", "scripts/select_submission_toolchain.py", + "scripts/prepare_ci_dependencies.py"]: with self.subTest(path=path): selection = self.select((Change("M", (path,)),)) self.assertEqual(selection.mode, "full") From 8c30522dbbe3e4ee4fd69a2042742ab878dd9770 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 13 Nov 2026 14:09:08 +0000 Subject: [PATCH 7/7] Preserve lightweight CI checkouts while using published artifact caches --- .github/workflows/ci.yml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3c0d9dc5e..c788bbd44 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -128,6 +128,10 @@ jobs: - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: use-mathlib-cache: true + # Keep the CI-only sparse package checkouts intact. Published + # Mathlib and TauCeti caches supply artifacts without restoring a + # previous job's multi-gigabyte source/package tree over them. + use-github-cache: false # Nothing here needs the whole library built, and building it would # compile TauCeti; the catalog shards build problem modules from its # cache. @@ -235,6 +239,10 @@ jobs: - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: use-mathlib-cache: true + # Keep the CI-only sparse package checkouts intact. Published + # Mathlib and TauCeti caches supply artifacts without restoring a + # previous job's multi-gigabyte source/package tree over them. + use-github-cache: false # Nothing here needs the whole library built, and building it would # compile TauCeti; the catalog shards build problem modules from its # cache. @@ -323,6 +331,10 @@ jobs: - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: use-mathlib-cache: true + # Keep the CI-only sparse package checkouts intact. Published + # Mathlib and TauCeti caches supply artifacts without restoring a + # previous job's multi-gigabyte source/package tree over them. + use-github-cache: false build: false test: false lint: false @@ -458,6 +470,10 @@ jobs: - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: use-mathlib-cache: true + # Keep the CI-only sparse package checkouts intact. Published + # Mathlib and TauCeti caches supply artifacts without restoring a + # previous job's multi-gigabyte source/package tree over them. + use-github-cache: false build: false test: false lint: false @@ -523,6 +539,10 @@ jobs: - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: use-mathlib-cache: true + # Keep the CI-only sparse package checkouts intact. Published + # Mathlib and TauCeti caches supply artifacts without restoring a + # previous job's multi-gigabyte source/package tree over them. + use-github-cache: false build: false test: false lint: false