Skip to content

Update CI #201

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RemyDegenne merged 2 commits into from
Jul 29, 2026
Merged

Update CI #201

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2432ea5
update CI
RemyDegenne Jul 29, 2026
9741706
Merge remote-tracking branch 'origin/main' into blueprint
RemyDegenne Jul 29, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
189 changes: 166 additions & 23 deletions .github/workflows/blueprint.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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' \
Expand All @@ -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
Expand All @@ -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.
Expand All @@ -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:
Expand Down