CI: build the referee site with referee-site, with the evidence store LML-evidence

.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-<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 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

.gitignore

@@ -31,7 +31,6 @@
 
 ## Website
 /home_page/
-/exposition/
 
 ## Tutorial and docs
 /LMLTutorial/_out/