CI: build the referee site with referee-site, with the evidence store… #120
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: Build | |
| on: | |
| push: | |
| branches: | |
| - main # Trigger on pushes to the default branch | |
| pull_request: | |
| branches: | |
| - main | |
| workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface | |
| # Cancel previous runs if a new commit is pushed to the same PR or branch | |
| concurrency: | |
| group: ${{ github.ref }} # Group runs by the ref (branch or PR) | |
| cancel-in-progress: true # Cancel any ongoing runs in the same group | |
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages | |
| permissions: | |
| contents: write # The dataset's release, and the provenance ledger's branch (the referee site step) | |
| pages: write # Write access to GitHub Pages | |
| id-token: write # Write access to ID tokens | |
| issues: write # Write access to issues | |
| pull-requests: write # Write access to pull requests | |
| jobs: | |
| build_project: | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - name: Cleanup to free disk space | |
| uses: jlumbroso/free-disk-space@ceedf095f4ec1a097402bc6bd80831f2e1a6fde6 # v1.3.0 | |
| with: | |
| tool-cache: false | |
| android: true # saves approximately 12 GB | |
| dotnet: false | |
| haskell: false | |
| large-packages: false | |
| docker-images: false | |
| swap-storage: false | |
| - name: Checkout project | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| # Load-bearing for provenance, not just a convenience: the provenance ledger dates what | |
| # changed with git, and at the default `fetch-depth: 1` the whole library would date from | |
| # the single fetched commit. | |
| fetch-depth: 0 # Fetch all history for all branches and tags | |
| - name: Build and lint project | |
| uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0 | |
| with: | |
| build: true | |
| build-args: "--wfail" | |
| lint: true | |
| mk_all-check: true | |
| # The referee site, by referee-site (LeanTrustBuilders). The action extracts the dataset with | |
| # the newest trust-extract release for this project's lean-toolchain (there is one for each | |
| # toolchain Mathlib moves to) and publishes it as the release `dataset-<commit12>`; records | |
| # the build in the provenance ledger, on the branch `trust-ledger`; and builds the site | |
| # against the previous build, with the reviews of the evidence store | |
| # LeanMachineLearning/LML-evidence and of the stores it imports. | |
| # | |
| # Pinned to a tag: referee-site's releases pin the evidence-core and evidence-store releases | |
| # they were tested with, so this build changes only when the tag here does. | |
| - name: Build the referee site | |
| id: referee | |
| if: github.event_name == 'push' | |
| uses: LeanTrustBuilders/referee-site@v0.12.0 | |
| with: | |
| root: LeanMachineLearning | |
| # An editorial claim, not a derived fact: it says whoever publishes this site vouches for | |
| # Mathlib and everything under it. Drop it and every upstream package counts as unaudited. | |
| trust: mathlib | |
| # The dataset follows dependencies into Mathlib and Lean core, so that the site shows | |
| # what LML rests on there, and the reviews of those declarations in imported stores. | |
| extract-args: --upstream-closure term | |
| # Lean's kernel checks that each declaration's dependency closure is all it needs, proofs | |
| # included (seconds on this library). | |
| check: meaning term | |
| evidence: LeanMachineLearning/LML-evidence | |
| # Unconditional, unlike the referee step: on a pull request this is the check that the | |
| # tutorial still builds. Placed after the referee step, which extracts the dataset, so that | |
| # `home_page/` and `LMLTutorial/_out/` do not exist yet when the dataset records whether the | |
| # tree was clean. | |
| - name: Build Verso Documentation | |
| run: | | |
| ./scripts/build_docs.sh | |
| - name: Build API documentation | |
| uses: leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14 | |
| with: | |
| homepage: home_page | |
| blueprint: false | |
| build-page: false | |
| deploy: false | |
| # After the docs step, which writes into the same folder alongside `tutorial/` from | |
| # `build_docs.sh`. Those steps only ever add, so the order is not load-bearing — but copying | |
| # last keeps the referee output out of reach of anything else that writes there. | |
| - name: Add the referee site to the home page | |
| if: github.event_name == 'push' | |
| run: | | |
| set -euo pipefail | |
| mkdir -p home_page/exposition | |
| cp -r "${{ steps.referee.outputs.site }}/." home_page/exposition/ | |
| - name: "Upload website (API documentation and home page)" | |
| if: github.event_name == 'push' | |
| uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5.0.0 | |
| with: | |
| path: home_page/ | |
| - name: Deploy to GitHub Pages | |
| if: github.event_name == 'push' | |
| id: deployment | |
| uses: actions/deploy-pages@368f82528645a54fb793d4d04e342629a3f51346 # v5.0.1 |