From a1f75fa32005f50308579759d9ff3cc5f2afd0dd Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 3 Oct 2026 11:28:05 +0200 Subject: [PATCH] CI: the referee site by referee-site (LeanTrustBuilders), with the evidence store LML-evidence Replaces LeanMachineLearning/exposition@v4.35.0-rc2, whose binary only reads Lean 4.35.0-rc2. The action takes the newest trust-extract release for the project's toolchain, publishes the dataset as the release dataset-, keeps the provenance ledger on the branch trust-ledger, and shows the reviews of LeanMachineLearning/LML-evidence and of the stores it imports. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/build.yml | 43 ++++++++++++++++++++----------------- .gitignore | 1 - 2 files changed, 23 insertions(+), 21 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 671b09cf..08be6056 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -16,12 +16,11 @@ concurrency: # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages permissions: - contents: write # Push the provenance ledger to its own branch (the referee action does) + 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 - actions: read # Read the previous run's artifact, for the referee revision diff jobs: build_project: @@ -42,10 +41,9 @@ jobs: - name: Checkout project 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. The action would unshallow the checkout itself, but fetching - # it here saves that second round trip. + # 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 @@ -56,31 +54,36 @@ jobs: lint: true mk_all-check: true - # The whole Referee pipeline: the binary and its toolchain check, semantic_hash, collect, - # the provenance ledger's branch round trip, the revision-diff baseline, extract and - # build-site. All of it used to be spelled out here, in 240 lines that were copy-pasted into - # three repositories and then drifted apart. It now lives in the action, which is tested in - # its own repository. + # 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-`; 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 rather than left floating: the tag names the Lean toolchain the binary was - # built for (`v4.34.0-rc2` here, matching this project's lean-toolchain), and the action - # takes its binary from the release of the same tag by default. + # 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: LeanMachineLearning/exposition@v4.35.0-rc2 + uses: LeanTrustBuilders/referee-site@v0.12.0 with: root: LeanMachineLearning - exclude-lib: LMLTutorial - site-url: https://leanmachinelearning.org/LML/exposition # 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 folds the provenance ledger, so - # that `home_page/` and `LMLTutorial/_out/` do not exist yet when the ledger records whether - # the tree was clean. + # 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 diff --git a/.gitignore b/.gitignore index a3a352df..fb8ef367 100644 --- a/.gitignore +++ b/.gitignore @@ -31,7 +31,6 @@ ## Website /home_page/ -/exposition/ ## Tutorial and docs /LMLTutorial/_out/