Repository navigation
Refresh generated project statistics and attribution #101
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Exposition Verify | |
| # Compiles a minimal Lean file for every project card's main_declarations | |
| # (the exposition's "Minimal Lean file" feature) and fails if any does not | |
| # elaborate. Runs weekly, on demand, and on PRs touching the exposition | |
| # pipeline — not on every content merge (the docs.yml exposition job stays | |
| # fast; this is the correctness gate for the builder itself). | |
| on: | |
| merge_group: | |
| types: [checks_requested] | |
| schedule: | |
| - cron: '40 6 * * 1' | |
| workflow_dispatch: | |
| pull_request: | |
| branches: | |
| - main | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| actions: read | |
| jobs: | |
| scope: | |
| runs-on: ubuntu-latest | |
| outputs: | |
| applicable: ${{ steps.scope.outputs.applicable }} | |
| steps: | |
| - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| persist-credentials: false | |
| - id: scope | |
| env: | |
| EVENT: ${{ github.event_name }} | |
| BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| run: | | |
| applicable=true | |
| if [ "$EVENT" = merge_group ] || [ "$EVENT" = pull_request ]; then | |
| applicable=false | |
| if [ "$EVENT" = pull_request ]; then | |
| files=$(git diff --name-only "$BASE"...HEAD) | |
| else | |
| files=$(git diff --name-only "$BASE"..HEAD) | |
| fi | |
| if printf '%s\n' "$files" | grep -Eq '^(python/lean_pool/(exposition/|ci_artifacts.py$)|scripts/exposition/|.github/workflows/exposition-verify.yml$)'; then | |
| applicable=true | |
| fi | |
| fi | |
| echo "applicable=$applicable" >> "$GITHUB_OUTPUT" | |
| # Waiting for another workflow must not consume the six-hour runner window | |
| # needed by extraction and real minimal-file verification. | |
| build-ready: | |
| needs: scope | |
| if: needs.scope.outputs.applicable == 'true' && github.event_name == 'pull_request' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| persist-credentials: false | |
| - name: Wait for 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 wait | |
| --head "$BUILD_HEAD" --event "$BUILD_EVENT" --wait-seconds 18000 | |
| verify: | |
| needs: [scope, build-ready] | |
| if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false') | |
| runs-on: ubuntu-latest | |
| name: Verify minimal Lean files | |
| steps: | |
| - name: Require successful change classification | |
| env: | |
| SCOPE_RESULT: ${{ needs.scope.result }} | |
| APPLICABLE: ${{ needs.scope.outputs.applicable }} | |
| BUILD_READY_RESULT: ${{ needs.build-ready.result }} | |
| EVENT: ${{ github.event_name }} | |
| run: | | |
| if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then | |
| echo "::error::Change classification failed; required validation cannot be skipped." | |
| exit 1 | |
| fi | |
| case "$EVENT:$BUILD_READY_RESULT" in | |
| pull_request:success|merge_group:skipped|schedule:skipped|workflow_dispatch:skipped) ;; | |
| *) | |
| echo "::error::Build preparation failed; required validation cannot be skipped." | |
| exit 1 | |
| ;; | |
| esac | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| - name: Identify compiled Lean sources | |
| id: build-identity | |
| run: echo "revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)" >> "$GITHUB_OUTPUT" | |
| # 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 dependencies | |
| id: dependency-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Restore pool build | |
| id: pool-build | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ steps.build-identity.outputs.revision }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Install Mathlib cache | |
| run: | | |
| set -euo pipefail | |
| ~/.elan/bin/lake exe cache get | |
| expected=$(jq -r '.packages[] | select(.name == "mathlib") | .rev' lake-manifest.json) | |
| actual=$(git -C .lake/packages/mathlib rev-parse HEAD) | |
| if [ "$actual" != "$expected" ]; then | |
| echo "::error::Mathlib checkout $actual does not match lake-manifest.json ($expected)." | |
| exit 1 | |
| fi | |
| - name: Reuse matching Lean CI build | |
| if: steps.pool-build.outputs.cache-hit != 'true' && github.event_name != 'merge_group' | |
| 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" | |
| --pull-request-artifact --wait-seconds 0 | |
| - name: Install uv | |
| uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff | |
| with: | |
| enable-cache: true | |
| - name: Reuse successful queued PR builds | |
| if: github.event_name == 'merge_group' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| BASE_SHA: ${{ github.event.merge_group.base_sha }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha }} | |
| run: >- | |
| PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build | |
| --base "$BASE_SHA" --head "$HEAD_SHA" | |
| - name: Build pool | |
| run: ~/.elan/bin/lake build LeanPool | |
| - name: Build Mathlib aggregate | |
| run: ~/.elan/bin/lake build Mathlib | |
| - 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/Extract.lean', 'scripts/exposition/extract-all.sh', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-${{ github.sha }}-${{ github.run_id }}-${{ github.run_attempt }} | |
| restore-keys: | | |
| Exposition-v1-${{ runner.os }}-${{ hashFiles('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') }}- | |
| - name: Extract declarations | |
| env: | |
| LEAN_CMD: /home/runner/.elan/bin/lean | |
| EXTRACT_JOBS: "2" | |
| run: >- | |
| ~/.elan/bin/lake env bash scripts/exposition/extract-all.sh | |
| exposition-dump.jsonl exposition-commands.jsonl | |
| - name: Save project extraction cache | |
| # Preserve completed projects if a sibling fails or the job is cancelled. | |
| if: always() && steps.extraction-cache.outcome == 'success' && 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: Generate site data | |
| run: | | |
| cd python | |
| uv sync --locked | |
| uv run python -m lean_pool.exposition \ | |
| --dump ../exposition-dump.jsonl \ | |
| --commands ../exposition-commands.jsonl \ | |
| --repo-root .. \ | |
| --out ../exposition-site \ | |
| --commit ${{ github.sha }} | |
| - name: Verify minimal files | |
| run: | | |
| # `lake env` must run from the workspace root; from python/ it | |
| # resolves no workspace and hands `lean` an empty LEAN_PATH, which | |
| # fails every target at `import Mathlib`. | |
| LEAN_PATH="$(~/.elan/bin/lake env printenv LEAN_PATH)" | |
| export LEAN_PATH | |
| cd python | |
| uv run python -m lean_pool.exposition.verify \ | |
| --site ../exposition-site \ | |
| --repo-root .. \ | |
| --out ../exposition-verify \ | |
| --jobs 2 \ | |
| --lean /home/runner/.elan/bin/lean \ | |
| --baseline 214 | |
| - name: Upload verification report | |
| if: always() | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: exposition-verify-report | |
| path: | | |
| exposition-verify/report.json | |
| retention-days: 30 |