@@ -24,8 +24,18 @@ permissions:
2424 actions : write # Write access to GitHub Actions
2525
2626env :
27- LEAN_EXPOSITION_REPO : LeanMachineLearning/exposition
28- LEAN_EXPOSITION_REF : main
27+ REFEREE_REPO : LeanMachineLearning/exposition
28+ # The referee release to use. Leave empty for the most recent one; set a tag (e.g. `v0.1.0`) to
29+ # pin the site generator, which is worth doing once the output is being read by anyone.
30+ #
31+ # A *release* rather than a run artifact on purpose: release assets of a public repository need no
32+ # authentication and never expire, while a cross-repository artifact download needs a PAT with
33+ # `actions:read` (a workflow's own GITHUB_TOKEN cannot reach another repository's artifacts) and
34+ # is deleted after 90 days.
35+ REFEREE_VERSION : " "
36+ # Kept as `exposition` rather than renamed to `referee` along with the tool: this path is the
37+ # published URL, and existing links to it would break.
38+ REFEREE_SITE_URL : https://leanmachinelearning.org/LML/exposition
2939
3040jobs :
3141 build_project :
@@ -59,29 +69,89 @@ jobs:
5969 run : |
6070 ./scripts/build_docs.sh
6171
62- name : Clone lean-exposition
72+ name : Download referee binary
6373 if : github.event_name == 'push'
74+ env :
75+ GH_TOKEN : ${{ secrets.GITHUB_TOKEN }}
6476 run : |
65- git clone --depth 1 --branch "$LEAN_EXPOSITION_REF" \
66- "https://github.com/$LEAN_EXPOSITION_REPO" /tmp/lean-exposition
77+ set -euo pipefail
78+ mkdir -p /tmp/referee
79+ gh release download ${REFEREE_VERSION:+"$REFEREE_VERSION"} \
80+ -R "$REFEREE_REPO" \
81+ --pattern 'referee-linux-x86_64-*.tar.gz' \
82+ --dir /tmp/referee --clobber
83+ tar -xzf /tmp/referee/referee-linux-x86_64-*.tar.gz -C /tmp/referee
84+ referee_bin=$(echo /tmp/referee/referee-linux-x86_64-*/referee)
85+ chmod +x "$referee_bin"
86+ echo "REFEREE_BIN=$referee_bin" >> "$GITHUB_ENV"
6787
68- name : Build exposition binary
88+ # `referee` is a Lean executable built with `supportInterpreter := true`, so it loads the
89+ # shared library of the toolchain it was compiled against and has to match this project's.
90+ # Checked here because the alternative is a link-time failure four steps later that says
91+ # nothing about the cause.
92+ want=$(tr -d '[:space:]' < lean-toolchain)
93+ got=$(jq -r .lean_toolchain "$(dirname "$referee_bin")/metadata.json" | tr -d '[:space:]')
94+ if [ "$want" != "$got" ]; then
95+ echo "::error::referee was built for $got but this project uses $want. Publish a \
96+ referee release from a matching toolchain, or pin REFEREE_VERSION to one."
97+ exit 1
98+ fi
99+
100+ # The previous run's collected data, so the site can say what changed since it. Optional in
101+ # every direction: the first run has nothing to download, a failed lookup is swallowed, and
102+ # `build-site` simply omits the Changes page when no baseline reaches it.
103+ - name : Fetch previous referee data for the revision diff
69104 if : github.event_name == 'push'
105+ continue-on-error : true
106+ env :
107+ GH_TOKEN : ${{ secrets.GITHUB_TOKEN }}
70108 run : |
71- cd /tmp/lean-exposition && lake build exposition
72- echo "EXPOSITION_BIN=/tmp/lean-exposition/.lake/build/bin/exposition" >> "$GITHUB_ENV"
109+ set -euo pipefail
110+ run_id=$(gh run list -R "$GITHUB_REPOSITORY" \
111+ --workflow "${{ github.workflow }}" --branch "${{ github.ref_name }}" \
112+ --status success --limit 1 --json databaseId --jq '.[0].databaseId // empty')
113+ [ -n "$run_id" ] || { echo "no earlier successful run; skipping the baseline"; exit 0; }
114+ gh run download "$run_id" -R "$GITHUB_REPOSITORY" \
115+ -n referee-data -D /tmp/referee-baseline
116+ echo "REFEREE_BASELINE=/tmp/referee-baseline/referee-data.json" >> "$GITHUB_ENV"
73117
74- name : Build exposition documentation
118+ name : Build the referee site
75119 if : github.event_name == 'push'
76120 run : |
77- lake env "$EXPOSITION_BIN" \
78- --root LeanMachineLearning \
79- --repo-url https://github.com/LeanMachineLearning/LML \
80- --site-url https://leanmachinelearning.org/LML/exposition \
81- --output ./exposition \
82- --exclude-lib LMLTutorial
83- mkdir -p home_page/exposition
84- cp -r exposition/html-multi/* home_page/exposition
121+ set -euo pipefail
122+ # The phase split: everything needing a Lean environment produces data, and rendering is a
123+ # pure function of that data. `--exclude-lib` applies to the three phases that import the
124+ # project, and to none of `build-site`, which reads only the JSON. `highlight-extracted`
125+ # is deliberately skipped — it re-elaborates every extracted file and costs more than the
126+ # rest of this job combined; without it the standalone files are still written and linked,
127+ # just not rendered inline.
128+ lake env "$REFEREE_BIN" collect \
129+ --root LeanMachineLearning --exclude-lib LMLTutorial --data referee-data.json
130+ lake env "$REFEREE_BIN" extract \
131+ --data referee-data.json --exclude-lib LMLTutorial --output ./referee-site
132+ lake env "$REFEREE_BIN" highlight \
133+ --data referee-data.json --output ./referee-site
134+ # `--trust` is an editorial claim, not a derived fact: it says whoever publishes this site
135+ # vouches for Mathlib and everything under it. Drop it and every upstream package counts
136+ # as unaudited; name more packages to vouch for more.
137+ "$REFEREE_BIN" build-site \
138+ --data referee-data.json \
139+ --output ./referee-site \
140+ --repo-url "https://github.com/$GITHUB_REPOSITORY" \
141+ --site-url "$REFEREE_SITE_URL" \
142+ --trust mathlib \
143+ ${REFEREE_BASELINE:+--baseline "$REFEREE_BASELINE"} \
144+ ${REFEREE_BASELINE:+--baseline-label "the previous build"}
145+
146+ # Kept as an artifact so the *next* run can diff against it. Also the thing to download when
147+ # you want to re-render the site locally without re-importing the project.
148+ - name : Upload referee data
149+ if : github.event_name == 'push'
150+ uses : actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
151+ with :
152+ name : referee-data
153+ path : referee-data.json
154+ retention-days : 90
85155
86156 - name : Compile blueprint and documentation
87157 uses : leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14
@@ -91,6 +161,16 @@ jobs:
91161 build-page : false
92162 deploy : false
93163
164+ # After the docs step, which writes into the same folder alongside `tutorial/` from
165+ # `build_docs.sh`. Those steps only ever add, so the order is not load-bearing — but copying
166+ # last keeps the referee output out of reach of anything else that writes there.
167+ - name : Add the referee site to the home page
168+ if : github.event_name == 'push'
169+ run : |
170+ set -euo pipefail
171+ mkdir -p home_page/exposition
172+ cp -r referee-site/html-multi/. home_page/exposition/
173+
94174name : " Upload website (API documentation, blueprint and any home page)"
95175 if : github.event_name == 'push'
96176 uses : actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5.0.0
0 commit comments