From 00da301b930c5f3afa62b79ec0e0db424c6a5d72 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 17 Sep 2026 15:23:45 -0700 Subject: [PATCH 1/4] Fix attribution metadata after project removals --- NOTICE | 8 +------- NOTICE.extra.yml | 8 -------- 2 files changed, 1 insertion(+), 15 deletions(-) diff --git a/NOTICE b/NOTICE index 923072afc6..b11476906e 100644 --- a/NOTICE +++ b/NOTICE @@ -142,6 +142,7 @@ Apache License, Version 2.0, and are redistributed here under the same license. https://github.com/lyfar/gkp-carry-lean LeanPool/Odlyzko https://github.com/ImperialCollegeLondon/FLT LeanPool/OrderPQ https://github.com/wupr/order-p-q + LeanPool/PDL https://github.com/m4lvin/lean4-pdl LeanPool/PFR https://github.com/teorth/pfr LeanPool/PebblingLean https://github.com/pachterlab/P_2026_2 LeanPool/PentagonalNumberTheorem https://github.com/wwylele/PentagonalNumberTheorem @@ -284,9 +285,6 @@ MIT permission notice that follows them. "Copyright (c) 2026" with no name; the repository owner of record is "SamuelSchlesinger". - LeanPool/SpecialNumbers https://github.com/provables/special-numbers - Copyright (c) 2024 Walter Moreira, Joe Stubbs - LeanPool/SteinhausThreeGap https://github.com/dkunert/three-gap-theorem-lean Copyright (c) 2026 Dirk Kunert @@ -324,10 +322,6 @@ Projects relicensed by their original author These projects were relicensed by their sole author before import. LeanPool/Clawristotle https://github.com/Vilin97/Clawristotle - LeanPool/ForwardEuler https://github.com/Vilin97/forward_euler - Originally distributed without a license file, then placed under the - Apache License, Version 2.0, by its sole author. - LeanPool/GrothendieckVanishing https://github.com/Vilin97/Clawristotle Originally distributed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International license, then diff --git a/NOTICE.extra.yml b/NOTICE.extra.yml index a9ff63f2c9..9e9f9758e3 100644 --- a/NOTICE.extra.yml +++ b/NOTICE.extra.yml @@ -59,11 +59,6 @@ FormalizationOfBoundedArithmetic: template text "Copyright (c) [year] [fullname]"; the repository owner of record is "ruplet". -ForwardEuler: - relicensed: |- - Originally distributed without a license file, then placed under the - Apache License, Version 2.0, by its sole author. - GrothendieckVanishing: relicensed: |- Originally distributed under the Creative Commons @@ -131,9 +126,6 @@ Shannon1948Formalization: "Copyright (c) 2026" with no name; the repository owner of record is "SamuelSchlesinger". -SpecialNumbers: - note: Copyright (c) 2024 Walter Moreira, Joe Stubbs - SteinhausThreeGap: note: Copyright (c) 2026 Dirk Kunert From 9f4bf5dea0d030c74020ceba534ca3dbb98374c3 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 17 Sep 2026 15:23:45 -0700 Subject: [PATCH 2/4] Cache exposition extraction and share Lean builds with docs --- .github/workflows/challenge-verify.yml | 14 +- .github/workflows/docs.yml | 115 +++++++--- .github/workflows/exposition-verify.yml | 53 ++++- .github/workflows/lean_action_ci.yml | 117 ++++++++--- .github/workflows/proof-profile.yml | 37 ++-- python/ci-performance.md | 73 +++++++ python/lean_pool/ci_artifacts.py | 203 ++++++++++++++++++ python/lean_pool/exposition/extract.py | 267 ++++++++++++++++++++++++ python/tests/test_ci_artifacts.py | 173 +++++++++++++++ python/tests/test_ci_cache_contract.py | 41 ++++ python/tests/test_exposition_extract.py | 178 ++++++++++++++++ scripts/exposition/extract-all.sh | 57 +---- 12 files changed, 1195 insertions(+), 133 deletions(-) create mode 100644 python/ci-performance.md create mode 100644 python/lean_pool/ci_artifacts.py create mode 100644 python/lean_pool/exposition/extract.py create mode 100644 python/tests/test_ci_artifacts.py create mode 100644 python/tests/test_ci_cache_contract.py create mode 100644 python/tests/test_exposition_extract.py diff --git a/.github/workflows/challenge-verify.yml b/.github/workflows/challenge-verify.yml index 92a938072d..04516ecf18 100644 --- a/.github/workflows/challenge-verify.yml +++ b/.github/workflows/challenge-verify.yml @@ -65,16 +65,22 @@ jobs: - name: Load tool pins run: cat scripts/challenge/pins.env | grep -E '^[A-Z0-9_]+=' >> "$GITHUB_ENV" - - name: Restore caches + - name: Restore Lean dependencies + id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore pool build + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - name: Install Lean uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 8cedb8e931..8d6b9c9ca0 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -13,6 +13,8 @@ on: - 'lean-toolchain' - 'docbuild/**' - 'python/lean_pool/exposition/**' + - 'python/lean_pool/ci_artifacts.py' + - 'scripts/exposition/**' - '.github/workflows/docs.yml' pull_request: branches: @@ -32,6 +34,8 @@ on: - 'lean-toolchain' - 'docbuild/**' - 'python/lean_pool/exposition/**' + - 'python/lean_pool/ci_artifacts.py' + - 'scripts/exposition/**' - '.github/workflows/notice.yml' - '.github/workflows/docs.yml' workflow_dispatch: @@ -106,21 +110,17 @@ jobs: exit 1 fi - # This is deliberately identical to Lean Action CI's cache lookup (key, - # paths, and ordering). Documentation can therefore start from the - # root build that CI already produced instead of compiling the - # entire pool again under a separate cache namespace. - - name: Restore Lean build cache + # Preflight needs the toolchain and dependencies, not the pool build. + # Stable dependencies are shared with CI without a new copy per commit. + - name: Restore Lean dependencies + id: dependency-cache if: steps.scope.outputs.readme_only != 'true' uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} - name: Install Lean if: steps.scope.outputs.readme_only != 'true' @@ -154,12 +154,9 @@ jobs: # never saves it — Lean Action CI owns that cache, while the documentation # jobs own doc-gen's separate caches. exposition: - # On a cold toolchain boundary, Mathlib docInfo gives Lean Action CI time - # to seed the new root cache before this job restores it. Without that - # boundary, exposition's pool rebuild plus extraction approached six hours. - needs: - - preflight - - mathlib_doc_info + # Exposition consumes compiled Lean, not doc-gen's Mathlib SQLite data. + # Reuse the matching CI artifact directly instead of waiting for docInfo. + needs: preflight if: needs.preflight.outputs.readme_only != 'true' runs-on: ubuntu-latest name: Build exposition site @@ -167,16 +164,22 @@ jobs: - name: Checkout project uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd - - name: Restore Lean build cache + - name: Restore Lean dependencies + id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore pool build + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - name: Install Lean uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 @@ -196,9 +199,27 @@ jobs: exit 1 fi + - name: Reuse matching Lean CI build + env: + GH_TOKEN: ${{ github.token }} + BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }} + BUILD_EVENT: ${{ github.event_name }} + run: >- + PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore + --head "$BUILD_HEAD" --event "$BUILD_EVENT" + - name: Build pool run: ~/.elan/bin/lake build LeanPool + - name: Restore project extraction cache + id: extraction-cache + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/exposition-cache/v1 + key: Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-${{ github.sha }} + restore-keys: | + Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}- + - name: Extract declarations # Per-project environments (see extract-all.sh); 2-way parallel to # stay inside the runner's memory. @@ -209,6 +230,25 @@ jobs: ~/.elan/bin/lake env bash scripts/exposition/extract-all.sh exposition-dump.jsonl exposition-commands.jsonl + - name: Save project extraction cache + if: steps.extraction-cache.outputs.cache-hit != 'true' + uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/exposition-cache/v1 + key: ${{ steps.extraction-cache.outputs.cache-primary-key }} + + - name: Upload extraction timings and logs + if: always() + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: exposition-extraction-diagnostics + path: | + .lake/exposition-timings.json + .lake/exposition-cache/v1/**/extract.log + .lake/exposition-cache/v1/**/failed.log + include-hidden-files: true + retention-days: 7 + - name: Install uv uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff with: @@ -245,19 +285,17 @@ jobs: - name: Checkout project uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd - - name: Restore Lean build cache + - name: Restore Lean dependencies + id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} - # Only doc-gen's own state is cached here. Root oleans stay in the - # Lean Action cache above, so the two namespaces do not duplicate them. + # Mathlib's compiled artifacts come from the dependency cache; doc-gen's + # SQLite data and extra dependencies have their own checkpoint. - name: Restore Mathlib documentation checkpoint id: mathlib-doc-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -337,16 +375,22 @@ jobs: - name: Checkout project uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd - - name: Restore Lean build cache + - name: Restore Lean dependencies + id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore pool build + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- # Prefer the latest complete docInfo database from this compatibility # boundary. On a cold boundary, the preceding job has just produced the @@ -398,6 +442,15 @@ jobs: exit 1 fi + - name: Reuse matching Lean CI build + env: + GH_TOKEN: ${{ github.token }} + BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }} + BUILD_EVENT: ${{ github.event_name }} + run: >- + PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore + --head "$BUILD_HEAD" --event "$BUILD_EVENT" + # This incrementally extends either a previous pool checkpoint or the # Mathlib checkpoint produced by the preceding job. doc-gen serializes # writes through one WAL database, so these targets intentionally share a @@ -501,7 +554,7 @@ jobs: echo "deploy=true" >> "$GITHUB_OUTPUT" fi - # The two expensive sites build in parallel after the Mathlib checkpoint. + # The two expensive sites build independently after preflight. # Let the dependency graph join them instead of racing one job against a # polling timeout. If either build fails, no incomplete tree is deployed. deploy: diff --git a/.github/workflows/exposition-verify.yml b/.github/workflows/exposition-verify.yml index 75521f71dc..eca9d1b3a2 100644 --- a/.github/workflows/exposition-verify.yml +++ b/.github/workflows/exposition-verify.yml @@ -15,6 +15,7 @@ on: - main paths: - 'python/lean_pool/exposition/**' + - 'python/lean_pool/ci_artifacts.py' - 'scripts/exposition/**' - '.github/workflows/exposition-verify.yml' @@ -24,6 +25,7 @@ concurrency: permissions: contents: read + actions: read jobs: verify: @@ -36,16 +38,22 @@ jobs: # Match Lean Action CI's cache lookup exactly. This workflow only needs # compiled Lean artifacts; restoring doc-gen output here used to make a # broad fallback pull an incompatible cache after every toolchain bump. - - name: Restore Lean build cache + - name: Restore Lean dependencies + id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore pool build + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - name: Install Lean uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 @@ -65,9 +73,27 @@ jobs: exit 1 fi + - name: Reuse matching Lean CI build + env: + GH_TOKEN: ${{ github.token }} + BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }} + BUILD_EVENT: ${{ github.event_name }} + run: >- + PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore + --head "$BUILD_HEAD" --event "$BUILD_EVENT" + - name: Build pool run: ~/.elan/bin/lake build LeanPool + - name: Restore project extraction cache + id: extraction-cache + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/exposition-cache/v1 + key: Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-${{ github.sha }} + restore-keys: | + Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}- + - name: Extract declarations env: LEAN_CMD: /home/runner/.elan/bin/lean @@ -76,6 +102,25 @@ jobs: ~/.elan/bin/lake env bash scripts/exposition/extract-all.sh exposition-dump.jsonl exposition-commands.jsonl + - name: Save project extraction cache + if: steps.extraction-cache.outputs.cache-hit != 'true' + uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/exposition-cache/v1 + key: ${{ steps.extraction-cache.outputs.cache-primary-key }} + + - name: Upload extraction timings and logs + if: always() + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: exposition-extraction-diagnostics + path: | + .lake/exposition-timings.json + .lake/exposition-cache/v1/**/extract.log + .lake/exposition-cache/v1/**/failed.log + include-hidden-files: true + retention-days: 7 + - name: Install uv uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff with: diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 8d7c980596..4c126a3eea 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -6,8 +6,7 @@ name: Lean Action CI # - `skip`: an exact README-only change. It still reports the # protected `Build project` check without spending hours rebuilding Lean. # - `single`: the classic one-job pipeline. This is the fast path for the -# common case — a PR that adds or edits a project or three — and is -# byte-for-byte the pre-sharding behavior. +# common case — a PR that adds or edits a project or three. # - `sharded`: for the runs that take hours serially (cold cache, # toolchain/manifest bump, refactors touching many projects), the dirty # projects are bin-packed into parallel `shard` build jobs. Pool projects @@ -35,6 +34,7 @@ on: - 'Challenge/challenges.yml' - 'python/lean_pool/challenge.py' - 'python/lean_pool/quality.py' + - 'python/lean_pool/ci_artifacts.py' - 'python/pyproject.toml' - 'python/uv.lock' - 'scripts/nolints-style.txt' @@ -61,6 +61,7 @@ on: - 'Challenge/challenges.yml' - 'python/lean_pool/challenge.py' - 'python/lean_pool/quality.py' + - 'python/lean_pool/ci_artifacts.py' - 'python/pyproject.toml' - 'python/uv.lock' - 'scripts/nolints-style.txt' @@ -106,13 +107,10 @@ jobs: uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: lookup-only: true - path: | - ~/.elan - .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - name: Plan the build id: plan @@ -157,7 +155,7 @@ jobs: echo "matrix=$(echo "$plan" | python3 -c 'import json,sys; print(json.dumps(json.load(sys.stdin)["matrix"]))')" } >> "$GITHUB_OUTPUT" - # The classic pipeline, unchanged — the fast path for ordinary PRs. + # The single-job pipeline is the fast path for ordinary PRs. build: needs: plan if: needs.plan.outputs.mode == 'single' @@ -169,17 +167,24 @@ jobs: with: fetch-depth: 0 - - name: Restore caches - id: cache + # Keep the large toolchain/Mathlib cache independent of per-commit builds. + - name: Restore Lean dependencies + id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore pool build + id: cache + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - name: Install Lean uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 @@ -220,6 +225,20 @@ jobs: - name: Build challenges and solutions run: ./scripts/ci/build-challenges.sh + # Publish once compilation succeeds, so docs can overlap the later + # linters/quality checks without compiling the same PR a second time. + - name: Package build for documentation + run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack + + - name: Share build with documentation + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: lean-pool-build + path: lean-pool-build.tar.gz + if-no-files-found: error + compression-level: 0 + retention-days: 1 + - name: Lint run: | ~/.elan/bin/lake exe runLinter LeanPool @@ -238,15 +257,21 @@ jobs: uv sync --locked uv run python -m lean_pool.quality --repo .. - - name: Save caches - if: always() && github.ref == 'refs/heads/main' + - name: Save Lean dependencies + if: always() && github.ref == 'refs/heads/main' && steps.dependency-cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Save pool build + if: always() && github.ref == 'refs/heads/main' + uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} shard: needs: plan @@ -266,16 +291,22 @@ jobs: with: fetch-depth: 0 - - name: Restore caches + - name: Restore Lean dependencies + id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore pool build + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - name: Install Lean uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 @@ -353,16 +384,22 @@ jobs: with: fetch-depth: 0 - - name: Restore caches + - name: Restore Lean dependencies + id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore pool build + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - name: Install Lean uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 @@ -422,6 +459,20 @@ jobs: - name: Build challenges and solutions run: ./scripts/ci/build-challenges.sh + # Publish once compilation succeeds, so docs can overlap the later + # linters/quality checks without compiling the same PR a second time. + - name: Package build for documentation + run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack + + - name: Share build with documentation + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: lean-pool-build + path: lean-pool-build.tar.gz + if-no-files-found: error + compression-level: 0 + retention-days: 1 + - name: Lint run: | ~/.elan/bin/lake exe runLinter LeanPool @@ -440,15 +491,21 @@ jobs: uv sync --locked uv run python -m lean_pool.quality --repo .. - - name: Save caches - if: always() && github.ref == 'refs/heads/main' + - name: Save Lean dependencies + if: always() && github.ref == 'refs/heads/main' && steps.dependency-cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Save pool build + if: always() && github.ref == 'refs/heads/main' + uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} # Single overall verdict under the check name the one-job workflow used, # so nothing watching "Build project" needs to change. diff --git a/.github/workflows/proof-profile.yml b/.github/workflows/proof-profile.yml index 2e633900f7..3653d41d6b 100644 --- a/.github/workflows/proof-profile.yml +++ b/.github/workflows/proof-profile.yml @@ -162,13 +162,10 @@ jobs: uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: lookup-only: true - path: | - ~/.elan - .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ steps.pr.outputs.head_sha }} + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ steps.pr.outputs.head_sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - name: Determine new and modified Lean files id: files @@ -288,16 +285,22 @@ jobs: fetch-depth: 0 persist-credentials: false - - name: Restore caches + - name: Restore Lean dependencies + id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ needs.plan.outputs.head_sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore pool build + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.head_sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - name: Install Lean uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 @@ -405,16 +408,22 @@ jobs: fetch-depth: 0 persist-credentials: false - - name: Restore caches + - name: Restore Lean dependencies + id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | ~/.elan .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ needs.plan.outputs.head_sha }} + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore pool build + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.head_sha }} restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - name: Install Lean uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 diff --git a/python/ci-performance.md b/python/ci-performance.md new file mode 100644 index 0000000000..37aa5cf8cf --- /dev/null +++ b/python/ci-performance.md @@ -0,0 +1,73 @@ +# Lean and documentation CI performance + +The September 17 investigation found two recurring costs: exposition extraction +ran for 137–146 minutes on every run, and evicted documentation checkpoints added +about 88 minutes for Mathlib and 94–101 minutes for pool documentation data. +Two per-commit Lean caches were about 5 GiB each against a 10 GB cache limit. +HTML rendering itself took about four minutes. + +Examples: [warm main run](https://github.com/Vilin97/lean-pool/actions/runs/35231792853), +[cold main run](https://github.com/Vilin97/lean-pool/actions/runs/35253856245), +[project PR run](https://github.com/Vilin97/lean-pool/actions/runs/35263858983). + +## Cache ownership + +Lean CI saves the toolchain and pinned dependencies under `LeanDependencies-v1`, +keyed by OS, toolchain, and dependency manifest. The separate `LeanPoolBuild-v1` +cache contains only `.lake/build`, with the build configuration and commit in +its key. All consumers use the same paths and compatibility keys. Preflight and +Mathlib documentation restore only dependencies. Existing `Lake-` caches expire +normally; the first run after this migration must seed the new namespaces. + +Documentation retains its separate, integrity-checked SQLite checkpoints. They +still depend on available cache capacity; this change reduces duplicate data +instead of changing the repository's paid storage limit. + +## Reusing the current CI build + +After compilation, both single and sharded CI publish one `lean-pool-build` +artifact with one-day retention. Docs look up the Lean CI run for their exact +event and head SHA, wait up to two hours for its compiled output, and verify a +manifest containing the Git tree and build-input hashes before installing it. +The tree comparison also distinguishes different PR merge bases. + +No matching run, missing/expired artifacts, API failures, or a mismatched tree +fall back to the regular Lake build. Documentation still invokes Lake, which +checks traces and builds any missing targets. Exposition can start after +preflight without waiting for Mathlib's unrelated docInfo database. The existing +warning, lint, quality, minimal-file, and documentation validation steps remain. + +## Incremental exposition extraction + +`lake env bash scripts/exposition/extract-all.sh` still runs each project in its +own Lean environment to preserve parser/notation isolation. Outputs are cached +under `.lake/exposition-cache/v1///`. Each key covers: + +- All Lean sources under the project, including its entry module. +- Local transitive imports from the entry module's Lake `.setup.json` inventory. +- The toolchain, dependency manifest, Lake configuration, extractor, and driver. + +Run after `lake build LeanPool` so compiler inventories reflect the current +source tree. A missing or malformed inventory conservatively hashes the entire +pool. Both JSONL files must pass validation before publication, and their hashes +are checked on reuse. Changed projects are extracted again; deleted projects +are omitted when the outputs are assembled in sorted project order. Obsolete +project generations are removed before saving the CI cache. + +To bypass cached results for a comparison: + +```sh +lake env bash scripts/exposition/extract-all.sh fresh-dump.jsonl fresh-commands.jsonl --refresh +``` + +CI uploads `exposition-extraction-diagnostics`, containing per-project wall times, +cache-hit flags, and extraction logs. Local timings are in +`.lake/exposition-timings.json`; failed process logs are retained next to the +project's cache generations. This makes cold-run hotspots measurable without +changing extraction semantics or skipping projects. + +The local SumDifferenceExponent smoke test produced identical SHA-256 hashes +for both output files on cold extraction, cache reuse, and forced refresh. +Cache reuse took under a millisecond, versus 5–13 seconds for extraction on that +machine. This is a small-project correctness check, not a whole-pool timing claim. +Measure full-run savings after the main-branch extraction cache has been seeded. diff --git a/python/lean_pool/ci_artifacts.py b/python/lean_pool/ci_artifacts.py new file mode 100644 index 0000000000..900113dd96 --- /dev/null +++ b/python/lean_pool/ci_artifacts.py @@ -0,0 +1,203 @@ +"""Share the current Lean CI build with documentation without sharing mutable caches. + +Only the matching Lean Action CI run is queried. A source-tree/configuration +manifest is verified before any artifact is installed; Lake still checks its +normal build traces afterwards. Missing or incompatible artifacts fall back to +the ordinary documentation build. +""" + +from __future__ import annotations + +import argparse +import hashlib +import io +import json +import logging +import os +import shutil +import subprocess +import tarfile +import tempfile +import time +import zipfile +from pathlib import Path, PurePosixPath +from urllib.parse import urlencode + +LOGGER = logging.getLogger(__name__) +ARTIFACT_NAME = "lean-pool-build" +ARCHIVE_NAME = "lean-pool-build.tar.gz" +MANIFEST_NAME = "build-manifest.json" + + +def _file_digest(path: Path) -> str: + with path.open("rb") as stream: + return hashlib.file_digest(stream, "sha256").hexdigest() + + +def build_identity(root: Path) -> dict: + """Identify the checkout tree and pinned build inputs, including merge checkouts.""" + tree = subprocess.check_output( + ["git", "rev-parse", "HEAD^{tree}"], cwd=root, text=True + ).strip() + return { + "version": 1, + "tree": tree, + "inputs": { + name: _file_digest(root / name) + for name in ("lean-toolchain", "lakefile.toml", "lake-manifest.json") + }, + } + + +def pack_build(root: Path, destination: Path) -> None: + """Package the completed root build; toolchains and dependencies stay in caches.""" + subprocess.run(["git", "diff", "--exit-code", "HEAD", "--"], cwd=root, check=True) + payload = json.dumps(build_identity(root)).encode() + manifest = tarfile.TarInfo(MANIFEST_NAME) + manifest.size = len(payload) + with tarfile.open( + destination, "w:gz", compresslevel=1, dereference=True + ) as archive: + archive.addfile(manifest, io.BytesIO(payload)) + archive.add(root / ".lake/build", arcname=".lake/build") + + +def restore_build(root: Path, archive_path: Path) -> bool: + """Validate identity and archive paths before replacing the root build.""" + with tarfile.open(archive_path, "r:gz") as archive: + manifest = archive.extractfile(MANIFEST_NAME) + if manifest is None or json.load(manifest) != build_identity(root): + LOGGER.info( + "CI build has a different source tree or configuration; rebuilding" + ) + return False + members = [ + member for member in archive.getmembers() if member.name != MANIFEST_NAME + ] + for member in members: + path = PurePosixPath(member.name) + if ( + path.parts[:2] != (".lake", "build") + or ".." in path.parts + or not (member.isfile() or member.isdir()) + ): + raise ValueError(f"Unexpected build archive member: {member.name}") + if not any(member.isfile() for member in members): + raise ValueError("Empty Lean build artifact") + with tempfile.TemporaryDirectory(prefix="lean-ci-build-") as temporary: + archive.extractall(temporary, members=members, filter="data") + destination = root / ".lake/build" + if destination.exists(): + shutil.rmtree(destination) + shutil.copytree(Path(temporary) / ".lake/build", destination) + LOGGER.info("Restored Lean CI build for the current source tree") + return True + + +def github_json(endpoint: str) -> dict: + """Read GitHub metadata through the runner's authenticated CLI.""" + return json.loads(subprocess.check_output(["gh", "api", endpoint], timeout=60)) + + +def matching_run(repository: str, head: str, event: str) -> dict | None: + """Select the latest Lean CI attempt for this event and exact head revision.""" + query = urlencode({"head_sha": head, "event": event, "per_page": 10}) + endpoint = f"repos/{repository}/actions/workflows/lean_action_ci.yml/runs?{query}" + runs = github_json(endpoint)["workflow_runs"] + return max(runs, key=lambda run: run["id"]) if runs else None + + +def wait_for_artifact(repository: str, run: dict, wait_seconds: int) -> int | None: + """Wait for compiled output without waiting for later lint/quality stages.""" + deadline = time.monotonic() + wait_seconds + endpoint = f"repos/{repository}/actions/runs/{run['id']}" + while True: + artifacts = github_json(f"{endpoint}/artifacts?per_page=100")["artifacts"] + matches = [ + artifact + for artifact in artifacts + if artifact["name"] == ARTIFACT_NAME and not artifact["expired"] + ] + if matches: + return max(matches, key=lambda artifact: artifact["id"])["id"] + status = github_json(endpoint) + if status["status"] == "completed" or time.monotonic() >= deadline: + return None + time.sleep(min(20, max(0, deadline - time.monotonic()))) + + +def download_build(root: Path, repository: str, artifact: int) -> bool: + """Download the archive and validate it before installing any build files.""" + with tempfile.TemporaryDirectory(prefix="lean-ci-download-") as temporary: + directory = Path(temporary) + zipped = directory / "artifact.zip" + with zipped.open("wb") as output: + subprocess.run( + ["gh", "api", f"repos/{repository}/actions/artifacts/{artifact}/zip"], + stdout=output, + check=True, + timeout=600, + ) + with zipfile.ZipFile(zipped) as archive: + if archive.namelist() != [ARCHIVE_NAME]: + raise ValueError("Unexpected files in Lean CI artifact") + with archive.open(ARCHIVE_NAME) as source: + with (directory / ARCHIVE_NAME).open("wb") as destination: + shutil.copyfileobj(source, destination) + return restore_build(root, directory / ARCHIVE_NAME) + + +def reuse_build(root: Path, repository: str, head: str, event: str, wait: int) -> bool: + """Best-effort reuse; unavailable CI never removes the regular Lake build step.""" + try: + run = matching_run(repository, head, event) + if run is None: + LOGGER.info("No matching Lean CI run; using the regular Lake build") + return False + LOGGER.info("Looking for compiled output from %s", run["html_url"]) + artifact = wait_for_artifact(repository, run, wait) + if artifact is None: + LOGGER.info( + "No completed build artifact available; using the regular Lake build" + ) + return False + return download_build(root, repository, artifact) + except ( + subprocess.SubprocessError, + OSError, + ValueError, + KeyError, + tarfile.TarError, + zipfile.BadZipFile, + ): + LOGGER.exception("Could not reuse CI output; using the regular Lake build") + return False + + +def main() -> None: + """Package a successful build or restore the matching workflow's compiled output.""" + parser = argparse.ArgumentParser(description=__doc__) + commands = parser.add_subparsers(dest="command", required=True) + pack = commands.add_parser("pack") + pack.add_argument("--output", type=Path, default=Path(ARCHIVE_NAME)) + restore = commands.add_parser("restore") + restore.add_argument("--repository", default=os.environ.get("GITHUB_REPOSITORY")) + restore.add_argument("--head", required=True) + restore.add_argument("--event", required=True) + restore.add_argument("--wait-seconds", type=int, default=7200) + arguments = parser.parse_args() + logging.basicConfig(level=logging.INFO, format="ci-artifacts: %(message)s") + if arguments.command == "pack": + pack_build(Path.cwd(), arguments.output) + else: + reuse_build( + Path.cwd(), + arguments.repository, + arguments.head, + arguments.event, + arguments.wait_seconds, + ) + + +if __name__ == "__main__": + main() diff --git a/python/lean_pool/exposition/extract.py b/python/lean_pool/exposition/extract.py new file mode 100644 index 0000000000..2f27991bbd --- /dev/null +++ b/python/lean_pool/exposition/extract.py @@ -0,0 +1,267 @@ +"""Cache isolated, per-project Lean extraction and assemble deterministic JSONL. + +Run after ``lake build LeanPool``, inside ``lake env``. Lake's setup files +provide the transitive import inventory; missing inventories conservatively +invalidate against the whole pool instead of risking stale dependency data. +""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import logging +import os +import shutil +import subprocess +import tempfile +import time +from concurrent.futures import ThreadPoolExecutor +from dataclasses import asdict, dataclass +from pathlib import Path + +from lean_pool.exposition.source_text import SourceFile, module_skeleton + +LOGGER = logging.getLogger(__name__) +OUTPUTS = ("declarations.jsonl", "commands.jsonl") +GLOBAL_INPUTS = ( + "lean-toolchain", + "lake-manifest.json", + "lakefile.toml", + "scripts/exposition/Extract.lean", + "scripts/exposition/extract-all.sh", + "python/lean_pool/exposition/extract.py", + "python/lean_pool/exposition/source_text.py", +) + + +def file_digest(path: Path) -> str: + """Hash a file without loading large extraction outputs into memory.""" + with path.open("rb") as stream: + return hashlib.file_digest(stream, "sha256").hexdigest() + + +def projects(root: Path) -> list[str]: + """Read the generated index, including module-system import modifiers.""" + source = SourceFile.from_text((root / "LeanPool.lean").read_text()) + names = sorted( + {name.split(".")[1] for name in module_skeleton(source).local_imports} + ) + if not names or any( + not (root / f"LeanPool/{name}.lean").is_file() for name in names + ): + raise ValueError("LeanPool.lean must import existing project entry modules") + return names + + +def project_sources(root: Path, project: str) -> set[Path]: + """Include project sources and all local transitive imports recorded by Lake.""" + sources = {root / f"LeanPool/{project}.lean"} + sources.update((root / "LeanPool" / project).rglob("*.lean")) + setup = root / f".lake/build/ir/LeanPool/{project}.setup.json" + try: + inventory = json.loads(setup.read_text()) + if inventory["name"] != f"LeanPool.{project}": + raise ValueError("wrong module in setup file") + imports = inventory["importArts"] + if not isinstance(imports, dict): + raise ValueError("invalid import inventory") + for module in imports: + path = root / (module.replace(".", "/") + ".lean") + if path.is_file(): + sources.add(path) + elif module.startswith("LeanPool."): + raise ValueError(f"missing imported source: {module}") + except (OSError, ValueError, KeyError, TypeError): + LOGGER.warning( + "%s: no usable Lake import inventory; hashing the whole pool", project + ) + sources.update((root / "LeanPool").rglob("*.lean")) + sources.add(root / "LeanPool.lean") + return sources + + +def fingerprint(root: Path, project: str, digests: dict[Path, str]) -> str: + """Hash source contents, dependencies, build configuration, and extractor code.""" + paths = project_sources(root, project) | {root / name for name in GLOBAL_INPUTS} + inputs = {} + for path in sorted(paths): + if path not in digests: + digests[path] = file_digest(path) + inputs[path.relative_to(root).as_posix()] = digests[path] + return hashlib.sha256(json.dumps(inputs, sort_keys=True).encode()).hexdigest() + + +def cache_valid(directory: Path, expected: str) -> bool: + """Reject partial, corrupt, and incompatible cached output pairs.""" + try: + manifest = json.loads((directory / "manifest.json").read_text()) + return manifest["fingerprint"] == expected and all( + file_digest(directory / name) == manifest["outputs"][name] + for name in OUTPUTS + ) + except (OSError, ValueError, KeyError, TypeError): + return False + + +def validate_output(path: Path, required: set[str]) -> None: + """Require complete JSONL records before publishing an extraction to the cache.""" + with path.open() as stream: + for line in stream: + record = json.loads(line) + if not isinstance(record, dict) or not required <= record.keys(): + raise ValueError(f"Invalid extraction record in {path}") + if not line.endswith("\n"): + raise ValueError(f"Unterminated extraction record in {path}") + + +@dataclass +class Extraction: + """Result and timing of one isolated project extraction.""" + + project: str + directory: Path + cached: bool + seconds: float + + +def extract_project( + root: Path, cache: Path, project: str, digest: str, lean: str, refresh: bool +) -> Extraction: + """Reuse a verified output pair or run Lean in this project's own environment.""" + started = time.monotonic() + directory = cache / project / digest + if not refresh and cache_valid(directory, digest): + return Extraction(project, directory, True, time.monotonic() - started) + directory.parent.mkdir(parents=True, exist_ok=True) + with tempfile.TemporaryDirectory( + prefix="extract-", dir=directory.parent + ) as temporary: + staging = Path(temporary) + command = [lean, "--run", "scripts/exposition/Extract.lean"] + command += [str(staging / name) for name in OUTPUTS] + [f"LeanPool.{project}"] + try: + with (staging / "extract.log").open("w") as log: + subprocess.run(command, cwd=root, stdout=log, stderr=log, check=True) + validate_output(staging / OUTPUTS[0], {"id", "m"}) + validate_output(staging / OUTPUTS[1], {"m", "c"}) + except (subprocess.CalledProcessError, OSError, ValueError): + shutil.copyfile(staging / "extract.log", directory.parent / "failed.log") + LOGGER.exception( + "%s failed; log: %s", project, directory.parent / "failed.log" + ) + raise + manifest = {"fingerprint": digest, "outputs": {}} + manifest["outputs"] = {name: file_digest(staging / name) for name in OUTPUTS} + (staging / "manifest.json").write_text(json.dumps(manifest) + "\n") + if directory.exists(): + shutil.rmtree(directory) + staging.replace(directory) + elapsed = time.monotonic() - started + LOGGER.info("%s: extracted in %.1fs", project, elapsed) + return Extraction(project, directory, False, elapsed) + + +def combine(results: list[Extraction], destinations: tuple[Path, Path]) -> None: + """Concatenate in project order, publishing only after every extraction succeeds.""" + for name, destination in zip(OUTPUTS, destinations, strict=True): + destination.parent.mkdir(parents=True, exist_ok=True) + with tempfile.NamedTemporaryFile( + dir=destination.parent, delete=False + ) as output: + temporary = Path(output.name) + try: + for result in results: + with (result.directory / name).open("rb") as source: + shutil.copyfileobj(source, output) + output.close() + temporary.replace(destination) + finally: + temporary.unlink(missing_ok=True) + + +def prune_cache(cache: Path, results: list[Extraction]) -> None: + """Save only current projects and their current generation in the CI cache.""" + retained = {result.directory for result in results} + for path in cache.iterdir(): + if path.is_dir(): + for generation in path.iterdir(): + if generation.is_dir() and generation not in retained: + shutil.rmtree(generation) + if path.name not in {result.project for result in results}: + shutil.rmtree(path) + + +def run_extraction( + root: Path, + cache: Path, + destinations: tuple[Path, Path], + jobs: int = 2, + lean: str = "lean", + refresh: bool = False, +) -> list[Extraction]: + """Extract every indexed project, reusing only matching content-addressed data.""" + if jobs < 1: + raise ValueError("jobs must be positive") + names = projects(root) + digests: dict[Path, str] = {} + fingerprints = {name: fingerprint(root, name, digests) for name in names} + LOGGER.info("Extracting %d projects (%d at a time)", len(names), jobs) + with ThreadPoolExecutor(max_workers=jobs) as executor: + futures = [ + executor.submit( + extract_project, root, cache, name, fingerprints[name], lean, refresh + ) + for name in names + ] + results = [future.result() for future in futures] + combine(results, destinations) + prune_cache(cache, results) + return results + + +def main() -> None: + """Run extraction from the repository root with Lean's environment available.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "declarations", nargs="?", type=Path, default=Path("exposition-dump.jsonl") + ) + parser.add_argument( + "commands", nargs="?", type=Path, default=Path("exposition-commands.jsonl") + ) + parser.add_argument("--cache", type=Path, default=Path(".lake/exposition-cache/v1")) + parser.add_argument( + "--jobs", type=int, default=int(os.environ.get("EXTRACT_JOBS", "2")) + ) + parser.add_argument("--lean", default=os.environ.get("LEAN_CMD", "lean")) + parser.add_argument( + "--refresh", action="store_true", help="Re-extract even valid cache hits" + ) + arguments = parser.parse_args() + logging.basicConfig(level=logging.INFO, format="exposition: %(message)s") + started = time.monotonic() + results = run_extraction( + Path.cwd(), + arguments.cache.resolve(), + (arguments.declarations, arguments.commands), + arguments.jobs, + arguments.lean, + arguments.refresh, + ) + report = { + "seconds": time.monotonic() - started, + "projects": [asdict(item) for item in results], + } + Path(".lake/exposition-timings.json").write_text( + json.dumps(report, default=str, indent=2) + "\n" + ) + LOGGER.info( + "Finished in %.1fs; %d/%d cache hits", + report["seconds"], + sum(item.cached for item in results), + len(results), + ) + + +if __name__ == "__main__": + main() diff --git a/python/tests/test_ci_artifacts.py b/python/tests/test_ci_artifacts.py new file mode 100644 index 0000000000..30a739d807 --- /dev/null +++ b/python/tests/test_ci_artifacts.py @@ -0,0 +1,173 @@ +"""Validate exact-tree build reuse and safe fallback for unavailable artifacts.""" + +from __future__ import annotations + +import io +import json +import subprocess +import tarfile +from pathlib import Path + +import pytest + +from lean_pool import ci_artifacts + + +@pytest.fixture +def repository(tmp_path: Path) -> Path: + """Create a committed source tree with an ignored synthetic Lake build.""" + for name in ("lean-toolchain", "lakefile.toml", "lake-manifest.json"): + (tmp_path / name).write_text(name) + (tmp_path / ".gitignore").write_text(".lake/\n*.tar.gz\n") + (tmp_path / ".lake/build/lib/lean").mkdir(parents=True) + (tmp_path / ".lake/build/lib/lean/LeanPool.olean").write_bytes(b"compiled") + for command in ( + ["init", "-q"], + ["add", "."], + [ + "-c", + "user.name=Test", + "-c", + "user.email=test@example.com", + "commit", + "-qm", + "initial", + ], + ): + subprocess.run(["git", *command], cwd=tmp_path, check=True) + return tmp_path + + +def test_build_round_trip(repository: Path) -> None: + """Matching output replaces the old build completely, including removed modules.""" + archive = repository / "build.tar.gz" + ci_artifacts.pack_build(repository, archive) + output = repository / ".lake/build/lib/lean/LeanPool.olean" + output.write_bytes(b"old") + stale = output.with_name("Removed.olean") + stale.touch() + assert ci_artifacts.restore_build(repository, archive) + assert output.read_bytes() == b"compiled" + assert not stale.exists() + + +def test_mismatched_configuration_preserves_current_build(repository: Path) -> None: + """An incompatible toolchain never replaces the fallback build.""" + archive = repository / "build.tar.gz" + ci_artifacts.pack_build(repository, archive) + (repository / "lean-toolchain").write_text("other version") + assert not ci_artifacts.restore_build(repository, archive) + assert ( + repository / ".lake/build/lib/lean/LeanPool.olean" + ).read_bytes() == b"compiled" + + +def test_mismatched_tree_preserves_current_build(repository: Path) -> None: + """A different source tree cannot reuse a same-toolchain artifact.""" + archive = repository / "build.tar.gz" + ci_artifacts.pack_build(repository, archive) + (repository / "Added.lean").write_text("-- new source\n") + subprocess.run(["git", "add", "Added.lean"], cwd=repository, check=True) + subprocess.run( + [ + "git", + "-c", + "user.name=Test", + "-c", + "user.email=test@example.com", + "commit", + "-qm", + "change", + ], + cwd=repository, + check=True, + ) + assert not ci_artifacts.restore_build(repository, archive) + + +def test_pack_rejects_dirty_checkout(repository: Path) -> None: + """The producer cannot label modified build inputs with the committed tree.""" + (repository / "lakefile.toml").write_text("changed options") + with pytest.raises(subprocess.CalledProcessError): + ci_artifacts.pack_build(repository, repository / "build.tar.gz") + + +@pytest.mark.parametrize( + ("name", "kind"), + [ + ("../escape", tarfile.REGTYPE), + ("/tmp/escape", tarfile.REGTYPE), + (".lake/build/../../escape", tarfile.REGTYPE), + ("LeanPool.lean", tarfile.REGTYPE), + (".lake/build/link", tarfile.SYMTYPE), + (".lake/build/link", tarfile.LNKTYPE), + ], +) +def test_unexpected_archive_member_rejected(repository: Path, name: str, kind) -> None: + """No archive path, symlink, or hardlink can escape the build directory.""" + destination = repository / "build.tar.gz" + with tarfile.open(destination, "w:gz") as archive: + payload = json.dumps(ci_artifacts.build_identity(repository)).encode() + manifest = tarfile.TarInfo(ci_artifacts.MANIFEST_NAME) + manifest.size = len(payload) + archive.addfile(manifest, io.BytesIO(payload)) + member = tarfile.TarInfo(name) + member.type = kind + member.linkname = "../../../escape" + archive.addfile(member) + with pytest.raises(ValueError, match="Unexpected build archive member"): + ci_artifacts.restore_build(repository, destination) + assert (repository / ".lake/build/lib/lean/LeanPool.olean").exists() + + +def test_missing_run_falls_back(repository: Path, monkeypatch) -> None: + """Docs-only changes and disabled CI retain the regular Lake build path.""" + monkeypatch.setattr(ci_artifacts, "matching_run", lambda *args: None) + assert not ci_artifacts.reuse_build(repository, "owner/repo", "head", "push", 0) + + +def test_api_error_falls_back(repository: Path, monkeypatch) -> None: + """Artifact API errors are an optimization miss rather than a docs failure.""" + + def unavailable(*args): + raise subprocess.CalledProcessError(1, "gh") + + monkeypatch.setattr(ci_artifacts, "matching_run", unavailable) + assert not ci_artifacts.reuse_build(repository, "owner/repo", "head", "push", 0) + + +def test_matching_run_queries_exact_head_and_event(monkeypatch) -> None: + """Concurrent PR/push runs cannot accidentally select another workflow's outputs.""" + endpoints = [] + + def response(endpoint): + endpoints.append(endpoint) + return {"workflow_runs": [{"id": 1}, {"id": 5}]} + + monkeypatch.setattr(ci_artifacts, "github_json", response) + assert ci_artifacts.matching_run("owner/repo", "abc123", "pull_request") == { + "id": 5 + } + assert "lean_action_ci.yml/runs?head_sha=abc123&event=pull_request&" in endpoints[0] + + +@pytest.mark.parametrize("status", ["completed", "in_progress"]) +def test_wait_ends_on_completed_run_or_deadline(monkeypatch, status: str) -> None: + """Missing artifacts cannot cause an unbounded wait.""" + + def response(endpoint): + return {"artifacts": []} if "/artifacts?" in endpoint else {"status": status} + + monkeypatch.setattr(ci_artifacts, "github_json", response) + assert ci_artifacts.wait_for_artifact("owner/repo", {"id": 1}, 0) is None + + +def test_artifact_available_before_quality_finishes(monkeypatch) -> None: + """Compilation output can be consumed while later checks are still running.""" + + def response(endpoint): + assert "/artifacts?" in endpoint + return {"artifacts": [{"id": 8, "name": "lean-pool-build", "expired": False}]} + + monkeypatch.setattr(ci_artifacts, "github_json", response) + assert ci_artifacts.wait_for_artifact("owner/repo", {"id": 1}, 0) == 8 diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py new file mode 100644 index 0000000000..76a9e99387 --- /dev/null +++ b/python/tests/test_ci_cache_contract.py @@ -0,0 +1,41 @@ +"""Keep shared cache producers and consumers compatible across CI workflows.""" + +from __future__ import annotations + +from pathlib import Path + +import yaml + +WORKFLOWS = Path(__file__).resolve().parents[2] / ".github/workflows" + + +def test_shared_cache_paths_and_keys_match() -> None: + """Cache versions include paths, so consumers must match the producer's contract.""" + contracts = {} + producers = {} + for path in WORKFLOWS.glob("*.yml"): + workflow = yaml.safe_load(path.read_text()) + for job in workflow.get("jobs", {}).values(): + for step in job.get("steps", []): + if not step.get("uses", "").startswith("actions/cache/"): + continue + settings = step.get("with", {}) + key = settings.get("key", "") + if key.startswith("LeanDependencies-v1-"): + category = "dependencies" + identity = key + elif key.startswith("LeanPoolBuild-v1-"): + category = "build" + identity = key.rsplit("-${{", 1)[0] + "-" + if "restore-keys" in settings: + assert settings["restore-keys"].strip() == identity + else: + continue + paths = tuple(settings["path"].strip().splitlines()) + contract = (identity, paths) + assert contracts.setdefault(category, contract) == contract, path + if step["uses"].startswith("actions/cache/save@"): + producers[category] = True + assert set(producers) == set(contracts) == {"dependencies", "build"} + assert contracts["dependencies"][1] == ("~/.elan", ".lake/packages") + assert contracts["build"][1] == (".lake/build",) diff --git a/python/tests/test_exposition_extract.py b/python/tests/test_exposition_extract.py new file mode 100644 index 0000000000..71594d7144 --- /dev/null +++ b/python/tests/test_exposition_extract.py @@ -0,0 +1,178 @@ +"""Exercise incremental extraction, invalidation, and failure publication rules.""" + +from __future__ import annotations + +import json +import subprocess +import sys +from pathlib import Path + +import pytest + +from lean_pool.exposition.extract import GLOBAL_INPUTS, OUTPUTS, run_extraction + + +@pytest.fixture +def repository(tmp_path: Path) -> Path: + """Create two projects and a fake Lean process producing valid extractor JSONL.""" + for name in GLOBAL_INPUTS: + path = tmp_path / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text("configuration\n") + (tmp_path / "LeanPool").mkdir() + (tmp_path / "LeanPool.lean").write_text( + "public import LeanPool.B\nimport LeanPool.A\n" + ) + for project in ("A", "B"): + (tmp_path / f"LeanPool/{project}.lean").write_text(f"-- {project}\n") + _inventory(tmp_path, project, {}) + executable = tmp_path / "lean" + executable.write_text( + f"#!{sys.executable}\n" + "import json, pathlib, sys\n" + "_, _, _, declarations, commands, module = sys.argv\n" + "with open('calls', 'a') as log: log.write(module + '\\n')\n" + "if pathlib.Path('fail').exists(): raise SystemExit(1)\n" + "source = pathlib.Path(module.replace('.', '/') + '.lean').read_text()\n" + "data = {'id': module + '.theorem', 'm': module, 'source': source}\n" + "pathlib.Path(declarations).write_text(json.dumps(data) + '\\n')\n" + "commands_data = json.dumps({'m': module, 'c': []})\n" + "pathlib.Path(commands).write_text(commands_data + '\\n')\n" + ) + executable.chmod(0o755) + return tmp_path + + +def _inventory(root: Path, project: str, imports: dict) -> None: + path = root / f".lake/build/ir/LeanPool/{project}.setup.json" + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(json.dumps({"name": f"LeanPool.{project}", "importArts": imports})) + + +def _run(root: Path, refresh: bool = False): + return run_extraction( + root, + root / ".lake/exposition-cache/v1", + tuple(root / name for name in OUTPUTS), + lean=str(root / "lean"), + refresh=refresh, + ) + + +def _outputs(root: Path) -> tuple[bytes, ...]: + return tuple((root / name).read_bytes() for name in OUTPUTS) + + +def test_warm_cache_and_refresh_match_cold_outputs(repository: Path) -> None: + """Warm builds skip Lean completely; forced extraction produces identical data.""" + assert not any(item.cached for item in _run(repository)) + expected = _outputs(repository) + assert [json.loads(line)["m"] for line in expected[0].splitlines()] == [ + "LeanPool.A", + "LeanPool.B", + ] + assert all(item.cached for item in _run(repository)) + assert len((repository / "calls").read_text().splitlines()) == 2 + assert _outputs(repository) == expected + assert not any(item.cached for item in _run(repository, refresh=True)) + assert _outputs(repository) == expected + + +def test_edit_only_reextracts_affected_project(repository: Path) -> None: + """A project source edit invalidates that project without repeating its siblings.""" + _run(repository) + (repository / "LeanPool/A.lean").write_text("-- changed\n") + assert [item.cached for item in _run(repository)] == [False, True] + expected = _outputs(repository) + _run(repository, refresh=True) + assert _outputs(repository) == expected + + +def test_transitive_import_invalidates_consumer(repository: Path) -> None: + """Cross-project dependencies come from the compiler's transitive inventory.""" + _inventory(repository, "B", {"LeanPool.A": {"olean": "irrelevant"}}) + _run(repository) + (repository / "LeanPool/A.lean").write_text("-- changed dependency\n") + assert not any(item.cached for item in _run(repository)) + + +@pytest.mark.parametrize("name", GLOBAL_INPUTS) +def test_global_input_invalidates_every_project(repository: Path, name: str) -> None: + """Toolchain, configuration, dependency pins, and extractor edits invalidate all.""" + _run(repository) + (repository / name).write_text("changed configuration\n") + assert not any(item.cached for item in _run(repository)) + + +@pytest.mark.parametrize("contents", [None, "broken", "{}", '{"name": "wrong"}']) +def test_missing_inventory_conservatively_hashes_pool( + repository: Path, contents +) -> None: + """Older cache formats never silently miss a cross-project dependency.""" + path = repository / ".lake/build/ir/LeanPool/B.setup.json" + if contents is None: + path.unlink() + else: + path.write_text(contents) + _run(repository) + (repository / "LeanPool/A.lean").write_text("-- changed\n") + assert not any(item.cached for item in _run(repository)) + + +def test_deleted_project_disappears_from_outputs_and_cache(repository: Path) -> None: + """Assembly uses the current index, never stale cached project names.""" + _run(repository) + (repository / "LeanPool.lean").write_text("import LeanPool.B\n") + (repository / "LeanPool/A.lean").unlink() + assert [item.project for item in _run(repository)] == ["B"] + assert b"LeanPool.A" not in _outputs(repository)[0] + assert not (repository / ".lake/exposition-cache/v1/A").exists() + + +@pytest.mark.parametrize("name", [*OUTPUTS, "manifest.json"]) +def test_corrupt_cache_reextracts_project(repository: Path, name: str) -> None: + """Both outputs and their manifest must be intact to reuse a project.""" + results = _run(repository) + expected = _outputs(repository) + (results[0].directory / name).write_text("corrupt") + assert [item.cached for item in _run(repository)] == [False, True] + assert _outputs(repository) == expected + + +def test_failed_extraction_keeps_published_output_and_diagnostics( + repository: Path, +) -> None: + """A failed process cannot publish a truncated aggregate or a successful cache.""" + _run(repository) + expected = _outputs(repository) + (repository / "fail").touch() + (repository / "LeanPool/A.lean").write_text("-- changed\n") + with pytest.raises(subprocess.CalledProcessError): + _run(repository) + assert _outputs(repository) == expected + assert (repository / ".lake/exposition-cache/v1/A/failed.log").exists() + (repository / "fail").unlink() + assert [item.cached for item in _run(repository)] == [False, True] + + +def test_invalid_jsonl_is_not_cached(repository: Path) -> None: + """A zero exit code with malformed extraction output is still a failed run.""" + executable = repository / "lean" + executable.write_text( + executable.read_text().replace("json.dumps(data)", "'broken'") + ) + with pytest.raises(ValueError): + _run(repository) + assert not (repository / OUTPUTS[0]).exists() + assert not list( + (repository / ".lake/exposition-cache/v1").glob("*/*/manifest.json") + ) + + +def test_additional_source_invalidates_project(repository: Path) -> None: + """Adding a module changes the project key even before the inventory mentions it.""" + _run(repository) + directory = repository / "LeanPool/A" + directory.mkdir() + (directory / "New.lean").write_text("-- new module\n") + assert [item.cached for item in _run(repository)] == [False, True] diff --git a/scripts/exposition/extract-all.sh b/scripts/exposition/extract-all.sh index d5c3e2d94e..f7f9ca1fd4 100755 --- a/scripts/exposition/extract-all.sh +++ b/scripts/exposition/extract-all.sh @@ -1,52 +1,9 @@ #!/usr/bin/env bash -# Per-project exposition extraction driver. -# -# Each project is extracted against its own environment (Mathlib + that -# project only). A whole-pool environment would superpose every project's -# parser extensions, and a foreign notation can turn an identifier used by -# another project (ε, s, …) into a keyword token — parse-error recovery -# then silently truncates re-parsed commands. Lean never builds against -# such a superposition, and neither do we. -# -# Usage: [LEAN_CMD=lean] [EXTRACT_JOBS=N] extract-all.sh -# Run from the repository root with LEAN_PATH set (e.g. via `lake env`). +# Keep each project's parser environment isolated: combining projects would +# superpose their notation extensions and silently change command parsing. +# The Python driver caches each environment's output and assembles the JSONL. +# Usage: [LEAN_CMD=lean] [EXTRACT_JOBS=N] extract-all.sh [dump.jsonl] [commands.jsonl] +# Run from the repository root inside `lake env`. set -euo pipefail - -out_dump="${1:-exposition-dump.jsonl}" -out_cmds="${2:-exposition-commands.jsonl}" -jobs="${EXTRACT_JOBS:-2}" -lean_cmd="${LEAN_CMD:-lean}" -workdir="$(mktemp -d)" - -# Project roots: the second component of every module the index imports. -projects="$(sed -n 's/^import LeanPool\.//p' LeanPool.lean | cut -d. -f1 | sort -u)" -count="$(printf '%s\n' "$projects" | wc -l | tr -d ' ')" -echo "exposition: extracting $count projects ($jobs at a time)" - -extract_failed=0 -printf '%s\n' "$projects" | xargs -P "$jobs" -I '{}' sh -c ' - "$1" --run scripts/exposition/Extract.lean \ - "$2/dump-$3.jsonl" "$2/cmds-$3.jsonl" "LeanPool.$3" \ - > "$2/log-$3.txt" 2>&1 || { echo "$3" >> "$2/FAILED"; } -' extract "$lean_cmd" "$workdir" '{}' || extract_failed=1 - -if [ -f "$workdir/FAILED" ] || [ "$extract_failed" -ne 0 ]; then - echo "exposition: extraction FAILED for:" >&2 - cat "$workdir/FAILED" 2>/dev/null >&2 || true - while read -r project; do - echo "--- $project ---" >&2 - tail -15 "$workdir/log-$project.txt" >&2 || true - done < "$workdir/FAILED" - echo "exposition: work dir kept at $workdir" >&2 - exit 1 -fi - -: > "$out_dump" -: > "$out_cmds" -for project in $projects; do - cat "$workdir/dump-$project.jsonl" >> "$out_dump" - cat "$workdir/cmds-$project.jsonl" >> "$out_cmds" -done -rm -rf "$workdir" -echo "exposition: wrote $(wc -l < "$out_dump" | tr -d ' ') declarations to $out_dump" -echo "exposition: wrote $(wc -l < "$out_cmds" | tr -d ' ') module command tables to $out_cmds" +export PYTHONPATH="$PWD/python${PYTHONPATH:+:$PYTHONPATH}" +exec python3 -m lean_pool.exposition.extract "$@" From f905ee6251a56ea6cac5d78041be8142202196ca Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 17 Sep 2026 15:25:28 -0700 Subject: [PATCH 3/4] Save stable dependencies only after successful installation --- .github/workflows/lean_action_ci.yml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 4c126a3eea..253f6b8d06 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -199,6 +199,7 @@ jobs: enable-cache: true - name: Install Mathlib cache + id: mathlib-cache run: | if [ ! -d ".lake/packages/mathlib" ]; then ~/.elan/bin/lake exe cache get @@ -258,7 +259,7 @@ jobs: uv run python -m lean_pool.quality --repo .. - name: Save Lean dependencies - if: always() && github.ref == 'refs/heads/main' && steps.dependency-cache.outputs.cache-hit != 'true' + if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | @@ -316,6 +317,7 @@ jobs: use-mathlib-cache: false - name: Install Mathlib cache + id: mathlib-cache run: | if [ ! -d ".lake/packages/mathlib" ]; then ~/.elan/bin/lake exe cache get @@ -414,6 +416,7 @@ jobs: enable-cache: true - name: Install Mathlib cache + id: mathlib-cache run: | if [ ! -d ".lake/packages/mathlib" ]; then ~/.elan/bin/lake exe cache get @@ -492,7 +495,7 @@ jobs: uv run python -m lean_pool.quality --repo .. - name: Save Lean dependencies - if: always() && github.ref == 'refs/heads/main' && steps.dependency-cache.outputs.cache-hit != 'true' + if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | From 2de83bac8673bb2f3c3fee62e1c079f2dfdf862f Mon Sep 17 00:00:00 2001 From: Vilin97 automation Date: Fri, 18 Sep 2026 07:33:36 -0700 Subject: [PATCH 4/4] Reject empty exposition extraction output An extractor that exits successfully but writes no records must not be published or cached: every indexed project declares at least one result and one module, so an empty JSONL file is a silent extraction failure. Co-Authored-By: Claude Fable 5.1 --- python/lean_pool/exposition/extract.py | 8 +++++++- python/tests/test_exposition_extract.py | 17 +++++++++++++++++ 2 files changed, 24 insertions(+), 1 deletion(-) diff --git a/python/lean_pool/exposition/extract.py b/python/lean_pool/exposition/extract.py index 2f27991bbd..89c3bf6450 100644 --- a/python/lean_pool/exposition/extract.py +++ b/python/lean_pool/exposition/extract.py @@ -105,7 +105,8 @@ def cache_valid(directory: Path, expected: str) -> bool: def validate_output(path: Path, required: set[str]) -> None: - """Require complete JSONL records before publishing an extraction to the cache.""" + """Require complete, nonempty JSONL before publishing an extraction to the cache.""" + records = 0 with path.open() as stream: for line in stream: record = json.loads(line) @@ -113,6 +114,11 @@ def validate_output(path: Path, required: set[str]) -> None: raise ValueError(f"Invalid extraction record in {path}") if not line.endswith("\n"): raise ValueError(f"Unterminated extraction record in {path}") + records += 1 + if records == 0: + # Every project declares at least one result and one module, so an + # empty file means the extractor silently produced nothing. + raise ValueError(f"Empty extraction output in {path}") @dataclass diff --git a/python/tests/test_exposition_extract.py b/python/tests/test_exposition_extract.py index 71594d7144..c170575800 100644 --- a/python/tests/test_exposition_extract.py +++ b/python/tests/test_exposition_extract.py @@ -169,6 +169,23 @@ def test_invalid_jsonl_is_not_cached(repository: Path) -> None: ) +def test_empty_extraction_is_not_cached(repository: Path) -> None: + """A successful exit with no records is a failed extraction, never a cache entry.""" + executable = repository / "lean" + executable.write_text( + executable.read_text().replace( + "pathlib.Path(declarations).write_text(json.dumps(data) + '\\n')", + "pathlib.Path(declarations).write_text('')", + ) + ) + with pytest.raises(ValueError, match="Empty extraction output"): + _run(repository) + assert not (repository / OUTPUTS[0]).exists() + assert not list( + (repository / ".lake/exposition-cache/v1").glob("*/*/manifest.json") + ) + + def test_additional_source_invalidates_project(repository: Path) -> None: """Adding a module changes the project key even before the inventory mentions it.""" _run(repository)