From 2432ea5134012a2d2324fdfb7509dbeeaec1b4a5 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 29 Jul 2026 13:23:36 +0200 Subject: [PATCH] update CI --- .github/workflows/blueprint.yml | 189 ++++++++++++++++++++++++++++---- 1 file changed, 166 insertions(+), 23 deletions(-) diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index 310a4464..118f416c 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/blueprint.yml @@ -16,12 +16,12 @@ concurrency: # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages permissions: - contents: read # Read access to repository contents + contents: write # Push the provenance ledger back to the branch (see the step that does) 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 - actions: write # Write access to GitHub Actions + actions: read # Read the previous run's artifact, for the referee revision diff env: REFEREE_REPO: LeanMachineLearning/exposition @@ -32,18 +32,47 @@ env: # authentication and never expire, while a cross-repository artifact download needs a PAT with # `actions:read` (a workflow's own GITHUB_TOKEN cannot reach another repository's artifacts) and # is deleted after 90 days. + # + # Must resolve to a release that has `collect --hashes` and the `provenance` subcommand, both of + # which this workflow now passes. v0.1.3 is the first that does; anything earlier fails with + # "Unknown or incomplete option". Empty resolves to the most recent release. REFEREE_VERSION: "" # Kept as `exposition` rather than renamed to `referee` along with the tool: this path is the # published URL, and existing links to it would break. REFEREE_SITE_URL: https://leanmachinelearning.org/LML/exposition + # The library that is exposed on the site, and the one excluded from every phase that imports the + # project. Named once here because `collect`, `extract`, `highlight` and the hash export all have + # to agree — a mismatch between the hashed set and the collected set makes `provenance` hard-fail. + REFEREE_ROOT: LeanMachineLearning + REFEREE_EXCLUDE_LIB: LMLTutorial + + # Generated data, deliberately *outside* the working tree. `provenance` records whether the tree + # was clean when it folded, via `git status --porcelain`, which counts untracked files — so + # leaving these where they land would permanently stamp the ledger as built from a dirty tree and + # make the site disclaim its own blame. + REFEREE_DATA: /tmp/referee-data/referee-data.json + REFEREE_HASHES: /tmp/referee-data/hashes.jsonl + + # The provenance ledger, committed to *this* repository rather than kept as an artifact: it is + # append-only and its whole value is that it remembers years of history, which a 90-day artifact + # cannot. Each run folds the current commit into it, so its resolution is this workflow's cadence + # — per commit, since this runs on every push to main. + REFEREE_PROVENANCE: provenance.json + + # `semantic_hash` supplies the rename-invariant hashes the ledger and the revision diff are keyed + # on. Leave the ref empty for the default branch; pin a tag or branch once the ledger matters, + # since a change in how it hashes reads as every declaration changing meaning at once. + SEMANTIC_HASH_REPO: https://github.com/mathlib-initiative/semantic_hash + SEMANTIC_HASH_REF: "" + jobs: build_project: runs-on: ubuntu-latest name: Build project steps: - name: Cleanup to free disk space - uses: jlumbroso/free-disk-space@main + uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be # v1.3.0 with: tool-cache: false android: true # saves approximately 12 GB @@ -54,8 +83,11 @@ jobs: swap-storage: false - name: Checkout project - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: + # Load-bearing for provenance, not just a convenience: the ledger's edit half is + # `git blame`, and at the default `fetch-depth: 1` blame attributes the entire library to + # the single fetched commit. fetch-depth: 0 # Fetch all history for all branches and tags - name: Build and lint project @@ -65,17 +97,13 @@ jobs: lint: true mk_all-check: true - - name: Build Verso Documentation - run: | - ./scripts/build_docs.sh - - name: Download referee binary if: github.event_name == 'push' env: GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} run: | set -euo pipefail - mkdir -p /tmp/referee + mkdir -p /tmp/referee "$(dirname "$REFEREE_DATA")" gh release download ${REFEREE_VERSION:+"$REFEREE_VERSION"} \ -R "$REFEREE_REPO" \ --pattern 'referee-linux-x86_64-*.tar.gz' \ @@ -97,9 +125,98 @@ jobs: exit 1 fi + # Built here rather than taken as a Lake dependency, for the same reason referee is downloaded + # rather than built: it loads this project's environment and refuses to run unless its own + # sysroot matches, so it has to be compiled against *this* toolchain, not the one it pins. + # Overwriting the pin is the whole patch. No dependencies beyond core, so this is ~1-2 min and + # the toolchain is already on the runner from the build step. + - name: Build semantic_hash + if: github.event_name == 'push' + run: | + set -euo pipefail + git clone --depth 1 ${SEMANTIC_HASH_REF:+--branch "$SEMANTIC_HASH_REF"} \ + "$SEMANTIC_HASH_REPO" /tmp/semantic_hash + cp lean-toolchain /tmp/semantic_hash/lean-toolchain + cd /tmp/semantic_hash + lake build semantic_hash + + # No `lake env`: it reads this project's LEAN_PATH itself from `--dir`. `--imports` takes the + # same roots `collect` exposes — `LeanMachineLearning` alone, which is also how `LMLTutorial` + # stays out of the hashed set without an exclusion flag of its own. It hashes the whole + # upstream cone, which is what makes the hashes deep enough to notice a Mathlib bump changing + # a statement underneath us, and `collect` keeps only the exposed declarations' entries. + - name: Export semantic hashes + if: github.event_name == 'push' + run: | + set -euo pipefail + /tmp/semantic_hash/.lake/build/bin/semantic_hash export \ + --dir . --imports "$REFEREE_ROOT" --output "$REFEREE_HASHES" + + # The phase split: everything needing a Lean environment produces data, and everything after + # is a pure function of that data. Collection is its own step because `provenance` has to run + # between it and the rendering. + - name: Collect referee data + if: github.event_name == 'push' + run: | + set -euo pipefail + lake env "$REFEREE_BIN" collect \ + --root "$REFEREE_ROOT" \ + --exclude-lib "$REFEREE_EXCLUDE_LIB" \ + --hashes "$REFEREE_HASHES" \ + --data "$REFEREE_DATA" + + # Needs a git working tree and no Lean environment at all, so it is a phase of its own. Runs + # before `extract`/`highlight`/`build_docs.sh`/docgen write into the tree, so that the + # cleanliness it records is the repository's and not this job's leftovers. + # + # Hard-fails rather than degrading, by design: it refuses to run on data collected without + # `--hashes`, because the ledger is append-only and a text-keyed one would record the mass + # false change of a toolchain upgrade permanently. A failure here means the hash export missed + # declarations `collect` exposes, which is worth stopping for. + # + # `--ref` is left off, so each revision is named by `git describe --tags --always` — a tag + # where there is one, else a short sha. Pass `--ref` explicitly to fold at release cadence + # instead ("changed between v0.2 and v0.3"). + - name: Fold this revision into the provenance ledger + if: github.event_name == 'push' + run: | + set -euo pipefail + # Dumped so that the tool's "working tree has uncommitted changes" warning, if it fires, + # comes with the reason attached rather than sending someone hunting for it. + echo "working tree at fold time:"; git status --porcelain + "$REFEREE_BIN" provenance \ + --data "$REFEREE_DATA" \ + --provenance "$REFEREE_PROVENANCE" + + # The ledger is only worth keeping if it survives the run that wrote it. Pushed with + # GITHUB_TOKEN, which by design does not trigger another workflow run, so this cannot loop + # back into itself. + # + # A rejected push is a warning and not a failure: the fold is idempotent per commit and the + # next run folds whatever it finds, so losing a race costs one revision of resolution rather + # than correctness — and it must not take the deployment down with it. + - name: Commit the provenance ledger + if: github.event_name == 'push' + run: | + set -euo pipefail + if git diff --quiet -- "$REFEREE_PROVENANCE" && + [ -z "$(git ls-files --others --exclude-standard -- "$REFEREE_PROVENANCE")" ]; then + echo "ledger unchanged (already folded at this commit); nothing to commit" + exit 0 + fi + git config user.name "github-actions[bot]" + git config user.email "41898282+github-actions[bot]@users.noreply.github.com" + git add "$REFEREE_PROVENANCE" + git commit -m "chore(referee): fold ${GITHUB_SHA:0:7} into the provenance ledger" + git push origin "HEAD:${GITHUB_REF_NAME}" || + echo "::warning::could not push the provenance ledger; the next run will fold this \ + revision together with the following one" + # The previous run's collected data, so the site can say what changed since it. Optional in # every direction: the first run has nothing to download, a failed lookup is swallowed, and - # `build-site` simply omits the Changes page when no baseline reaches it. + # `build-site` simply omits the Changes page when no baseline reaches it. Complementary to the + # ledger rather than replaced by it — the ledger says *when* a declaration last changed, the + # baseline shows the two statements side by side. - name: Fetch previous referee data for the revision diff if: github.event_name == 'push' continue-on-error: true @@ -113,35 +230,54 @@ jobs: [ -n "$run_id" ] || { echo "no earlier successful run; skipping the baseline"; exit 0; } gh run download "$run_id" -R "$GITHUB_REPOSITORY" \ -n referee-data -D /tmp/referee-baseline - echo "REFEREE_BASELINE=/tmp/referee-baseline/referee-data.json" >> "$GITHUB_ENV" + # Located rather than assumed: the artifact's internal layout follows whatever path was + # uploaded, and a wrong guess here would silently cost the Changes page on every run. + found=$(find /tmp/referee-baseline -name '*.json' | head -1) + [ -n "$found" ] || { echo "artifact holds no JSON; skipping the baseline"; exit 0; } + echo "REFEREE_BASELINE=$found" >> "$GITHUB_ENV" - name: Build the referee site if: github.event_name == 'push' run: | set -euo pipefail - # The phase split: everything needing a Lean environment produces data, and rendering is a - # pure function of that data. `--exclude-lib` applies to the three phases that import the - # project, and to none of `build-site`, which reads only the JSON. `highlight-extracted` - # is deliberately skipped — it re-elaborates every extracted file and costs more than the + # A baseline written by an older `collect` is rejected outright — the data file carries a + # format version and `build-site` treats a mismatch as fatal, not as something to degrade + # around. Dropped here instead: one run without a Changes page, and the next has one + # again, which beats failing the deployment over a stale artifact. + baseline="${REFEREE_BASELINE:-}" + if [ -n "$baseline" ] && + [ "$(jq -r .version "$baseline")" != "$(jq -r .version "$REFEREE_DATA")" ]; then + echo "::notice::baseline is collected-data version $(jq -r .version "$baseline") but \ + this build writes $(jq -r .version "$REFEREE_DATA"); skipping the revision diff" + baseline="" + fi + + # `--exclude-lib` goes only to `extract`, the one phase here that imports the project + # wholesale. `highlight` fans out to per-module workers driven by the data file, and + # `build-site` reads only the JSON, so neither needs it. `highlight-extracted` is + # deliberately skipped — it re-elaborates every extracted file and costs more than the # rest of this job combined; without it the standalone files are still written and linked, # just not rendered inline. - lake env "$REFEREE_BIN" collect \ - --root LeanMachineLearning --exclude-lib LMLTutorial --data referee-data.json lake env "$REFEREE_BIN" extract \ - --data referee-data.json --exclude-lib LMLTutorial --output ./referee-site + --data "$REFEREE_DATA" --exclude-lib "$REFEREE_EXCLUDE_LIB" --output ./referee-site lake env "$REFEREE_BIN" highlight \ - --data referee-data.json --output ./referee-site + --data "$REFEREE_DATA" --output ./referee-site # `--trust` is 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; name more packages to vouch for more. + # + # `--provenance` is read-only here: `build-site` never folds. It adds the "meaning + # unchanged since" line, the Browse column, the revision selector on the Changes page, and + # pins every source link to the commit the ledger was folded at instead of to `main`. "$REFEREE_BIN" build-site \ - --data referee-data.json \ + --data "$REFEREE_DATA" \ --output ./referee-site \ --repo-url "https://github.com/$GITHUB_REPOSITORY" \ --site-url "$REFEREE_SITE_URL" \ --trust mathlib \ - ${REFEREE_BASELINE:+--baseline "$REFEREE_BASELINE"} \ - ${REFEREE_BASELINE:+--baseline-label "the previous build"} + --provenance "$REFEREE_PROVENANCE" \ + ${baseline:+--baseline "$baseline"} \ + ${baseline:+--baseline-label "the previous build"} # Kept as an artifact so the *next* run can diff against it. Also the thing to download when # you want to re-render the site locally without re-importing the project. @@ -150,9 +286,16 @@ jobs: uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 with: name: referee-data - path: referee-data.json + path: ${{ env.REFEREE_DATA }} retention-days: 90 + # Unconditional, unlike the referee steps: on a pull request this is the check that the + # tutorial still builds. Placed after the provenance fold so that `home_page/` and + # `LMLTutorial/_out/` do not exist yet when the ledger records whether the tree was clean. + - name: Build Verso Documentation + run: | + ./scripts/build_docs.sh + - name: Compile blueprint and documentation uses: leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14 with: