Repository navigation
Enable queue validation and independent project metadata #6179
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: Documentation | |
| on: | |
| merge_group: | |
| types: [checks_requested] | |
| push: | |
| branches: | |
| - main | |
| paths: | |
| - '**/*.lean' | |
| - 'LeanPool/projects/**' | |
| - 'LeanPool/projects.yml' | |
| - 'lakefile.toml' | |
| - 'lake-manifest.json' | |
| - 'lean-toolchain' | |
| - 'docbuild/**' | |
| - 'python/lean_pool/exposition/**' | |
| - 'python/lean_pool/quality.py' | |
| - 'python/lean_pool/validation_cache.py' | |
| - 'python/lean_pool/ci_artifacts.py' | |
| - 'python/lean_pool/ci_cache.py' | |
| - 'python/lean_pool/rebase_fastpath.py' | |
| - 'scripts/exposition/**' | |
| - '.github/workflows/docs.yml' | |
| pull_request: | |
| branches: | |
| - main | |
| workflow_dispatch: | |
| inputs: | |
| preview: | |
| description: "Generate full documentation for this branch on demand" | |
| type: boolean | |
| required: false | |
| default: false | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| # PR updates should supersede stale work, but the first main build after a | |
| # toolchain bump must be allowed to finish and seed the new caches. | |
| cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| actions: read | |
| jobs: | |
| # Fail cheap consistency checks before either multi-hour documentation job | |
| # starts. In particular, a stale generated root should not spend runner time | |
| # building documentation that cannot be merged. | |
| preflight: | |
| runs-on: ubuntu-latest | |
| name: Documentation preflight | |
| outputs: | |
| build_revision: ${{ steps.build-identity.outputs.revision }} | |
| readme_only: ${{ steps.scope.outputs.readme_only }} | |
| rebase_only: ${{ steps.rebase.outputs.rebase_only }} | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| - name: Install Python tooling runtime | |
| uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff | |
| with: | |
| enable-cache: true | |
| - name: Identify compiled Lean sources | |
| id: build-identity | |
| run: | | |
| set -euo pipefail | |
| revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision) | |
| echo "revision=$revision" >> "$GITHUB_OUTPUT" | |
| - name: Detect README-only change | |
| id: scope | |
| env: | |
| BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| EVENT_NAME: ${{ github.event_name }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }} | |
| run: | | |
| set -euo pipefail | |
| readme_only=false | |
| if [ "$EVENT_NAME" = "pull_request" ]; then | |
| files="$(git diff --name-only "$BASE_SHA"..."$HEAD_SHA")" | |
| if [ "$files" = "README.md" ]; then | |
| readme_only=true | |
| fi | |
| fi | |
| echo "readme_only=$readme_only" >> "$GITHUB_OUTPUT" | |
| echo "README-only change: $readme_only" | |
| - name: Verify prior documentation preflight for a content-only rebase | |
| id: rebase | |
| if: github.event_name == 'pull_request' && steps.scope.outputs.readme_only != 'true' | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| PR_NUMBER: ${{ github.event.pull_request.number }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }} | |
| BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| run: | | |
| decision=$(PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath decide \ | |
| --workflow docs.yml --repository "$REPOSITORY" --number "$PR_NUMBER" \ | |
| --head "$HEAD_SHA" --base "$BASE_SHA") | |
| echo "rebase_only=$(echo "$decision" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["eligible"]).lower())')" >> "$GITHUB_OUTPUT" | |
| echo "$decision" | |
| # docbuild deliberately reuses the root workspace's compiled artifacts. | |
| # Fail before restoring anything if those workspaces ever diverge. | |
| - name: Check documentation workspace compatibility | |
| if: steps.scope.outputs.readme_only != 'true' | |
| run: | | |
| set -euo pipefail | |
| if ! cmp lean-toolchain docbuild/lean-toolchain; then | |
| echo "::error::Root and documentation workspaces use different Lean toolchains." | |
| exit 1 | |
| fi | |
| root_mathlib=$(jq -r '.packages[] | select(.name == "mathlib") | .rev' lake-manifest.json) | |
| docs_mathlib=$(jq -r '.packages[] | select(.name == "mathlib") | .rev' docbuild/lake-manifest.json) | |
| if [ -z "$root_mathlib" ] || [ "$root_mathlib" = "null" ]; then | |
| echo "::error::Root lake-manifest.json has no Mathlib revision." | |
| exit 1 | |
| fi | |
| if [ -z "$docs_mathlib" ] || [ "$docs_mathlib" = "null" ]; then | |
| echo "::error::docbuild/lake-manifest.json has no Mathlib revision." | |
| exit 1 | |
| fi | |
| if [ "$root_mathlib" != "$docs_mathlib" ]; then | |
| echo "::error::Root Mathlib revision $root_mathlib does not match docbuild ($docs_mathlib)." | |
| exit 1 | |
| fi | |
| # 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' && steps.rebase.outputs.rebase_only != 'true' | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Install Lean | |
| if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| # A package directory from a restored cache does not prove that its | |
| # oleans match the current manifest. `cache get` is incremental, so run it | |
| # unconditionally and then verify the checkout revision. | |
| - name: Install and verify Mathlib cache | |
| if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' | |
| 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: Check generated roots | |
| if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' | |
| run: ~/.elan/bin/lake exe mk_all --check | |
| - name: Check regenerated LeanPool root without Lean | |
| if: steps.rebase.outputs.rebase_only == 'true' | |
| run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath check-index | |
| # Runs in parallel with the doc-gen4 build; its (small) artifact is merged | |
| # into the Pages tree by the `deploy` job. Restores the root build cache but | |
| # never saves it — Lean Action CI owns that cache, while the documentation | |
| # jobs own doc-gen's separate caches. | |
| exposition: | |
| # 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' && | |
| ((github.ref == 'refs/heads/main' && github.event_name != 'pull_request') || | |
| (github.event_name == 'workflow_dispatch' && inputs.preview)) | |
| runs-on: ubuntu-latest | |
| name: Build exposition site | |
| permissions: | |
| contents: read | |
| actions: write | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| - 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') }}-${{ needs.preflight.outputs.build_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' | |
| 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. | |
| 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 | |
| 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: Prune old copies of project extraction cache | |
| if: steps.extraction-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| CACHE_KEY: ${{ steps.extraction-cache.outputs.cache-primary-key }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_cache prune | |
| --repository "$REPOSITORY" --key "$CACHE_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: | |
| enable-cache: true | |
| - name: Generate site | |
| 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: Upload exposition artifact | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: exposition-site | |
| path: exposition-site | |
| if-no-files-found: error | |
| retention-days: 3 | |
| # Mathlib dominates a cold doc-gen bootstrap. Give it a separate job and | |
| # persist the verified SQLite checkpoint immediately, before any pool module | |
| # can consume the remainder of GitHub's six-hour job limit. | |
| mathlib_doc_info: | |
| needs: preflight | |
| if: >- | |
| needs.preflight.outputs.readme_only != 'true' && | |
| ((github.ref == 'refs/heads/main' && github.event_name != 'pull_request') || | |
| (github.event_name == 'workflow_dispatch' && inputs.preview)) | |
| runs-on: ubuntu-latest | |
| name: Build Mathlib documentation data | |
| permissions: | |
| contents: read | |
| actions: write | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| - 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') }} | |
| # 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 | |
| with: | |
| path: | | |
| docbuild/.lake/build | |
| .lake/packages/doc-gen4 | |
| .lake/packages/leansqlite | |
| .lake/packages/UnicodeBasic | |
| .lake/packages/BibtexQuery | |
| .lake/packages/MD4Lean | |
| key: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }} | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Install and verify 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 | |
| # Lake materializes the exact dependencies in docbuild/lake-manifest.json; | |
| # do not run `lake update`, which can re-resolve and rewrite that lockfile. | |
| - name: Build Mathlib documentation data | |
| run: cd docbuild && ~/.elan/bin/lake build Mathlib:docInfo | |
| - name: Validate Mathlib documentation checkpoint | |
| run: | | |
| set -euo pipefail | |
| test -s docbuild/.lake/build/api-docs.db | |
| test -n "$(find docbuild/.lake/build/doc-data -type f -name 'Mathlib*.doc' -print -quit)" | |
| python3 - <<'PY' | |
| import sqlite3 | |
| with sqlite3.connect("docbuild/.lake/build/api-docs.db") as connection: | |
| checkpoint = connection.execute("PRAGMA wal_checkpoint(TRUNCATE)").fetchone() | |
| integrity = connection.execute("PRAGMA quick_check").fetchone() | |
| if checkpoint is None or checkpoint[0] != 0: | |
| raise SystemExit(f"SQLite WAL checkpoint failed: {checkpoint!r}") | |
| if integrity != ("ok",): | |
| raise SystemExit(f"SQLite quick_check failed: {integrity!r}") | |
| PY | |
| # PR caches remain scoped to refs/pull/N/merge, so saving here safely | |
| # hands the cold checkpoint to this workflow's downstream job and reruns. | |
| - name: Save Mathlib documentation checkpoint | |
| if: steps.mathlib-doc-cache.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| docbuild/.lake/build | |
| .lake/packages/doc-gen4 | |
| .lake/packages/leansqlite | |
| .lake/packages/UnicodeBasic | |
| .lake/packages/BibtexQuery | |
| .lake/packages/MD4Lean | |
| key: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }} | |
| - name: Prune old copies of mathlib documentation checkpoint | |
| if: steps.mathlib-doc-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| CACHE_KEY: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_cache prune | |
| --repository "$REPOSITORY" --key "$CACHE_KEY" | |
| build: | |
| needs: | |
| - preflight | |
| - mathlib_doc_info | |
| if: >- | |
| needs.preflight.outputs.readme_only != 'true' && | |
| ((github.ref == 'refs/heads/main' && github.event_name != 'pull_request') || | |
| (github.event_name == 'workflow_dispatch' && inputs.preview)) | |
| runs-on: ubuntu-latest | |
| name: Build doc-gen4 site | |
| permissions: | |
| contents: read | |
| actions: write | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| - 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') }}-${{ needs.preflight.outputs.build_revision }} | |
| restore-keys: | | |
| 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 | |
| # Mathlib-only checkpoint used by the conditional fallback below. | |
| - name: Restore pool documentation checkpoint | |
| id: pool-doc-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| docbuild/.lake/build | |
| .lake/packages/doc-gen4 | |
| .lake/packages/leansqlite | |
| .lake/packages/UnicodeBasic | |
| .lake/packages/BibtexQuery | |
| .lake/packages/MD4Lean | |
| key: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }} | |
| restore-keys: | | |
| DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}- | |
| - name: Restore Mathlib documentation checkpoint | |
| if: steps.pool-doc-cache.outputs.cache-matched-key == '' | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| docbuild/.lake/build | |
| .lake/packages/doc-gen4 | |
| .lake/packages/leansqlite | |
| .lake/packages/UnicodeBasic | |
| .lake/packages/BibtexQuery | |
| .lake/packages/MD4Lean | |
| key: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }} | |
| fail-on-cache-miss: true | |
| - 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' | |
| 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 | |
| # single job instead of unsafe parallel shards. | |
| - name: Build documentation data | |
| run: cd docbuild && ~/.elan/bin/lake build LeanPool:docInfo | |
| - name: Validate pool documentation checkpoint | |
| run: | | |
| set -euo pipefail | |
| test -s docbuild/.lake/build/api-docs.db | |
| test -n "$(find docbuild/.lake/build/doc-data -type f -name 'LeanPool*.doc' -print -quit)" | |
| python3 - <<'PY' | |
| import sqlite3 | |
| with sqlite3.connect("docbuild/.lake/build/api-docs.db") as connection: | |
| checkpoint = connection.execute("PRAGMA wal_checkpoint(TRUNCATE)").fetchone() | |
| integrity = connection.execute("PRAGMA quick_check").fetchone() | |
| if checkpoint is None or checkpoint[0] != 0: | |
| raise SystemExit(f"SQLite WAL checkpoint failed: {checkpoint!r}") | |
| if integrity != ("ok",): | |
| raise SystemExit(f"SQLite quick_check failed: {integrity!r}") | |
| PY | |
| - name: Save pool documentation checkpoint | |
| if: steps.pool-doc-cache.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| docbuild/.lake/build | |
| .lake/packages/doc-gen4 | |
| .lake/packages/leansqlite | |
| .lake/packages/UnicodeBasic | |
| .lake/packages/BibtexQuery | |
| .lake/packages/MD4Lean | |
| key: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }} | |
| - name: Prune old copies of pool documentation checkpoint | |
| if: steps.pool-doc-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main' | |
| continue-on-error: true | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| CACHE_KEY: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.ci_cache prune | |
| --repository "$REPOSITORY" --key "$CACHE_KEY" | |
| - name: Build documentation | |
| run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs | |
| - name: Validate documentation site | |
| run: | | |
| set -euo pipefail | |
| test -s docbuild/.lake/build/doc/index.html | |
| test -s docbuild/.lake/build/doc/LeanPool.html | |
| test -s docbuild/.lake/build/doc/declarations/declaration-data.bmp | |
| - name: Remove cached exposition | |
| if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request' | |
| run: rm -rf docbuild/.lake/build/doc/exposition | |
| - name: Upload documentation artifact | |
| if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request' | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: documentation-site | |
| path: docbuild/.lake/build/doc | |
| if-no-files-found: error | |
| retention-days: 3 | |
| # Main bootstrap runs are intentionally not cancelled because they may be | |
| # the only producer of a new compatibility cache. If main advanced while a | |
| # run was building, retain those caches but never enter the Pages environment | |
| # or deploy stale HTML. | |
| deployment_freshness: | |
| needs: | |
| - exposition | |
| - build | |
| if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request' | |
| runs-on: ubuntu-latest | |
| name: Check deployment freshness | |
| outputs: | |
| deploy: ${{ steps.check.outputs.deploy }} | |
| steps: | |
| - name: Compare with latest Documentation run | |
| id: check | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| run: | | |
| set -euo pipefail | |
| latest_run=$(gh api --method GET \ | |
| "repos/${GITHUB_REPOSITORY}/actions/workflows/docs.yml/runs" \ | |
| -f branch=main -F exclude_pull_requests=true -F per_page=1 \ | |
| --jq '.workflow_runs[0].run_number') | |
| if ! [[ "$latest_run" =~ ^[0-9]+$ ]]; then | |
| echo "::error::Could not determine the latest Documentation run on main." | |
| exit 1 | |
| fi | |
| if (( latest_run > GITHUB_RUN_NUMBER )); then | |
| echo "deploy=false" >> "$GITHUB_OUTPUT" | |
| echo "::notice::Skipping superseded Documentation run $GITHUB_RUN_NUMBER; main has run $latest_run." | |
| else | |
| echo "deploy=true" >> "$GITHUB_OUTPUT" | |
| fi | |
| # 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: | |
| needs: | |
| - exposition | |
| - build | |
| - deployment_freshness | |
| if: needs.deployment_freshness.outputs.deploy == 'true' | |
| runs-on: ubuntu-latest | |
| name: Deploy documentation | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| steps: | |
| - name: Download documentation artifact | |
| uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 | |
| with: | |
| name: documentation-site | |
| path: site | |
| - name: Download exposition artifact | |
| uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 | |
| with: | |
| name: exposition-site | |
| path: site/exposition | |
| - name: Validate assembled Pages tree | |
| run: | | |
| set -euo pipefail | |
| test -s site/index.html | |
| test -s site/exposition/index.html | |
| test -s site/exposition/decls/index.html | |
| test -s site/exposition/assets/landing.js | |
| test -s site/exposition/data/decls.json | |
| jq -e --arg commit "$GITHUB_SHA" ' | |
| .commit == $commit | |
| and (.projects | length > 0) | |
| and (.totals.projects == (.projects | length)) | |
| and (.totals.decls > 0) | |
| ' site/exposition/data/index.json > /dev/null | |
| first_project=$(jq -r '.projects[0].slug' site/exposition/data/index.json) | |
| test -s "site/exposition/p/${first_project}/index.html" | |
| mkdir -p site/deployments | |
| printf '%s\n' "$GITHUB_SHA" > "site/deployments/${GITHUB_SHA}.txt" | |
| - name: Configure Pages | |
| uses: actions/configure-pages@983d7736d9b0ae728b81ab479565c72886d7745b | |
| - name: Upload Pages artifact | |
| uses: actions/upload-pages-artifact@7b1f4a764d45c48632c6b24a0339c27f5614fb0b | |
| with: | |
| path: site | |
| # Narrow the race between the gate job and the irreversible deployment. | |
| # Comparing workflow runs (rather than raw main HEAD) deliberately ignores | |
| # newer commits that do not match this workflow's path filters. | |
| - name: Recheck deployment freshness | |
| id: final-freshness | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| run: | | |
| set -euo pipefail | |
| latest_run=$(gh api --method GET \ | |
| "repos/${GITHUB_REPOSITORY}/actions/workflows/docs.yml/runs" \ | |
| -f branch=main -F exclude_pull_requests=true -F per_page=1 \ | |
| --jq '.workflow_runs[0].run_number') | |
| if ! [[ "$latest_run" =~ ^[0-9]+$ ]]; then | |
| echo "::error::Could not determine the latest Documentation run on main." | |
| exit 1 | |
| fi | |
| if (( latest_run > GITHUB_RUN_NUMBER )); then | |
| echo "deploy=false" >> "$GITHUB_OUTPUT" | |
| echo "::notice::Skipping superseded Documentation run $GITHUB_RUN_NUMBER; main has run $latest_run." | |
| else | |
| echo "deploy=true" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Deploy Pages | |
| id: deployment | |
| if: steps.final-freshness.outputs.deploy == 'true' | |
| uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128 | |
| - name: Verify deployed site | |
| if: steps.final-freshness.outputs.deploy == 'true' | |
| env: | |
| PAGE_URL: ${{ steps.deployment.outputs.page_url }} | |
| run: | | |
| curl --fail --silent --show-error \ | |
| --retry 30 --retry-delay 10 --retry-all-errors --retry-max-time 300 \ | |
| --output deployed-commit.txt \ | |
| "${PAGE_URL%/}/deployments/${GITHUB_SHA}.txt" | |
| cmp "site/deployments/${GITHUB_SHA}.txt" deployed-commit.txt | |
| curl --fail --silent --show-error \ | |
| --retry 30 --retry-delay 10 --retry-all-errors --retry-max-time 300 \ | |
| --output /dev/null \ | |
| "${PAGE_URL%/}/exposition/index.html" |