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

[RemyDegenne]

The referee site is now built by referee-site's action, instead of LeanMachineLearning/exposition@v4.35.0-rc2. The old action's binary only reads Lean 4.35.0-rc2, so it would block the bump to rc3 (#262).

What the new step does on each push to main

• Dataset. It extracts LML's dataset with the newest trust-extract release for the toolchain in lean-toolchain. The extractor gets a release for every toolchain Mathlib's master moves to, within about an hour.
• Kernel check. Lean's kernel checks that every declaration's dependency closure is all it needs, along both meaning and term.
• Release. It publishes the dataset as the release dataset-<commit12>, about 4 MB, never marked "Latest".
• Ledger. It records the build in the provenance ledger on a new branch, trust-ledger.
• Site. It builds the site against the previous build, with the reviews in the evidence store LeanMachineLearning/LML-evidence and in the stores that store imports (the Mathlib probability store). The site's review buttons open that repository's issue forms.

The site still lands in home_page/exposition/, so its URL doesn't change. Links into individual pages of the old site may break, because the two tools lay out pages differently.

The step is pinned to referee-site@v0.12.0, which pins the evidence-core (v0.16.1) and evidence-store (v0.7.2) releases it was tested with. The site build changes only when that tag changes.

Other changes

• The actions: read permission is gone: the old action used it to fetch the previous run's artifact.
• /exposition/ is gone from .gitignore: the new action writes nothing into the checkout.

Testing

The site step only runs on pushes to main, so it first runs in this repository at merge. Beforehand, the same action, with the same inputs, ran on LML's main from a scratch workflow in another repository, with publishing and the ledger turned off:

• extraction with trust-extract 0.13.0 for rc2;
• the kernel check passed for all 1,468 declarations, along both notions;
• the site was built with 1,468 declarations, and its forms pointed at LML-evidence.

After merging

• The first run creates the dataset-<commit12> release and the trust-ledger branch.
• The old referee-ledger branch is no longer used, and can be deleted.
• Bump mathlib dependency to v4.35.0-rc3 #262, the bump to rc3, never ran CI, because the update bot opened it with the workflow token. Pushing to its branch, or closing and reopening it, runs CI. trust-extract 0.13.1 is released for rc3.

🤖 Generated with Claude Code