From 92a51a56559d77411cc0aca43bbfd8ffe2fed5ee Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 27 Aug 2026 10:39:56 +0000 Subject: [PATCH 01/10] Add rounds: archived, citable snapshots of the arena The arena so far only ever showed its current state, with no way to refer to a result: checkers, tests and the Lean version they are measured against all move, so a number quoted today means something else next month. Introduce rounds. The site now says which round it shows, either a named round or "round in progress". Pushing a `round-` tag closes a round: CI runs the full suite (no tests skipped), publishes the site, the results and the test suite as release assets, and deposits them on Zenodo for a DOI. Deploys reassemble /round// from the release assets and generate an index of all rounds; the "other rounds" link is absolute so that it also works from a downloaded round tarball. The DOI is reserved before the site is built, so it can be shown on the round's own page, and published last, once everything else has succeeded, so that a failure discards the draft rather than minting a DOI that cannot be withdrawn. Rounds are deposited as successive versions of each other, giving them a shared concept DOI next to their per-round DOIs. `test-round-*` tags run the same path against sandbox.zenodo.org, on any branch, and can be deleted without leaving traces. Release assets are all named after their round, since they are read far away from the release page that would otherwise say which round they belong to. The archived site links to the results and the test tarball under fixed names, so the assembly step renames them back when placing them. Chota is now vendored instead of loaded from unpkg: an archived round has to still render years from now. Pages locate their assets through a `root_path` variable rather than a template block, since the stylesheet link is no longer the only one that needs it. --- .github/workflows/build-and-deploy.yml | 268 ++++++++++++++++++++++++- .github/zenodo.py | 245 ++++++++++++++++++++++ .zenodo.json | 39 ++++ README.md | 58 ++++++ lka.py | 154 +++++++++++++- templates/base.html | 12 +- templates/checker.html | 2 - templates/index.html | 29 ++- templates/rounds.html | 83 ++++++++ templates/static/chota.min.css | 3 + templates/static/style.css | 23 +++ templates/test.html | 2 - 12 files changed, 893 insertions(+), 25 deletions(-) create mode 100644 .github/zenodo.py create mode 100644 .zenodo.json create mode 100644 templates/rounds.html create mode 100644 templates/static/chota.min.css diff --git a/.github/workflows/build-and-deploy.yml b/.github/workflows/build-and-deploy.yml index b9dc97c..f5c1401 100644 --- a/.github/workflows/build-and-deploy.yml +++ b/.github/workflows/build-and-deploy.yml @@ -3,6 +3,14 @@ name: Build and Deploy Site on: workflow_dispatch: # Manual trigger, also deploys the site pull_request: # Run on pull requests + push: + tags: + # Closes a round: builds the site from scratch, publishes it as a release + # and deposits it on Zenodo for a DOI. `test-round-*` does the same + # against sandbox.zenodo.org, so the tag and release can be deleted again + # without leaving traces. + - 'round-*' + - 'test-round-*' permissions: contents: read @@ -12,6 +20,55 @@ concurrency: cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: + round-info: + name: Determine round + runs-on: ubuntu-latest + outputs: + # 'true' when this build closes a round (i.e. runs off a round tag) + is_round: ${{ steps.round.outputs.is_round }} + # The round name, e.g. 2026-10 (the tag without its prefix) + round: ${{ steps.round.outputs.round }} + # 'true' for test rounds, which use sandbox.zenodo.org and are published + # as GitHub pre-releases + sandbox: ${{ steps.round.outputs.sandbox }} + # Whether this build is deployed to GitHub Pages + deploy: ${{ steps.round.outputs.deploy }} + steps: + - name: Determine round from the tag + id: round + run: | + tag="$GITHUB_REF_NAME" + if [ "$GITHUB_REF_TYPE" != "tag" ]; then + echo "Not a tag build; this is the round in progress" + { + echo "is_round=false" + echo "round=" + echo "sandbox=false" + echo "deploy=${{ github.event_name == 'workflow_dispatch' }}" + } >> "$GITHUB_OUTPUT" + exit 0 + fi + case "$tag" in + test-round-*) sandbox=true; round="${tag#test-round-}" ;; + round-*) sandbox=false; round="${tag#round-}" ;; + *) echo "::error::Tag $tag is not a round tag"; exit 1 ;; + esac + # Rounds are named after a year and a month, e.g. 2026-10 + if ! printf '%s' "$round" | grep -qE '^[0-9]{4}-[0-9]{2}$'; then + echo "::error::Round name '$round' (from tag $tag) is not of the form YYYY-MM" + exit 1 + fi + echo "Closing round $round (sandbox=$sandbox)" + # A test round must not replace the live site; it only exercises the + # release and Zenodo path. + if [ "$sandbox" = true ]; then deploy=false; else deploy=true; fi + { + echo "is_round=true" + echo "round=$round" + echo "sandbox=$sandbox" + echo "deploy=$deploy" + } >> "$GITHUB_OUTPUT" + select-checkers: name: Select checkers runs-on: ubuntu-latest @@ -113,7 +170,7 @@ jobs: shell: 'nix develop -c bash -euxo pipefail {0}' - name: Generate tests - run: ./lka.py build-test --skip-declined-by "$CHECKER" ${{ github.event_name != 'workflow_dispatch' && '--skip-ci' || '' }} + run: ./lka.py build-test --skip-declined-by "$CHECKER" ${{ github.event_name == 'pull_request' && '--skip-ci' || '' }} shell: 'nix develop -c bash -euxo pipefail {0}' - name: Run checker on tests @@ -188,7 +245,7 @@ jobs: shell: 'nix develop -c bash -euxo pipefail {0}' - name: Generate tests - run: ./lka.py build-test ${{ github.event_name != 'workflow_dispatch' && '--skip-ci' || '' }} + run: ./lka.py build-test ${{ github.event_name == 'pull_request' && '--skip-ci' || '' }} shell: 'nix develop -c bash -euxo pipefail {0}' - name: Build test tarball @@ -211,20 +268,92 @@ jobs: name: test-tarball path: _out/lean-arena-tests.tar.gz + zenodo-reserve: + name: Reserve DOI on Zenodo + needs: [round-info, check, tutorial, test-stats] + # Only for rounds, and only once the measurements are in: a reserved DOI + # that is never published leaves a draft deposition behind. + if: ${{ !cancelled() && needs.round-info.outputs.is_round == 'true' && needs.check.result == 'success' }} + runs-on: ubuntu-latest + permissions: + contents: read + outputs: + doi: ${{ steps.reserve.outputs.doi }} + deposition_id: ${{ steps.reserve.outputs.deposition_id }} + bucket: ${{ steps.reserve.outputs.bucket }} + env: + GH_TOKEN: ${{ github.token }} + ROUND: ${{ needs.round-info.outputs.round }} + SANDBOX: ${{ needs.round-info.outputs.sandbox }} + steps: + - name: Checkout repository + uses: actions/checkout@v7 + + # Each round is deposited as a new version of the previous round, so that + # all rounds share one concept DOI that resolves to the newest round. + # The previous round records its deposition id in its own results.json. + - name: Find the previous round's deposition + id: previous + run: | + if [ "$SANDBOX" = true ]; then prefix=test-round-; else prefix=round-; fi + # grep finds nothing before the first round exists, and pipefail + # would turn that into a failure + previous=$(gh release list --limit 100 --json tagName --jq '.[].tagName' \ + | { grep "^${prefix}[0-9]" || true; } \ + | { grep -v "^${GITHUB_REF_NAME}$" || true; } \ + | sort -r | head -1) + if [ -z "$previous" ]; then + echo "No previous round; this is the first deposition" + echo "deposition=" >> "$GITHUB_OUTPUT" + exit 0 + fi + echo "Previous round: $previous" + gh release download "$previous" --pattern '*-results.json' --dir _previous + deposition=$(jq -r '.meta.zenodo_deposition // empty' _previous/*-results.json) + if [ -z "$deposition" ]; then + echo "::error::Round $previous has no Zenodo deposition recorded in its results.json" + exit 1 + fi + echo "Previous deposition: $deposition" + echo "deposition=$deposition" >> "$GITHUB_OUTPUT" + + - name: Create draft deposition and reserve a DOI + id: reserve + run: | + args=() + if [ "$SANDBOX" = true ]; then args+=(--sandbox); fi + args+=(reserve --round "$ROUND") + if [ -n "$PREVIOUS" ]; then args+=(--previous-deposition "$PREVIOUS"); fi + .github/zenodo.py "${args[@]}" + env: + PREVIOUS: ${{ steps.previous.outputs.deposition }} + ZENODO_TOKEN: ${{ needs.round-info.outputs.sandbox == 'true' && secrets.ZENODO_SANDBOX_TOKEN || secrets.ZENODO_TOKEN }} + build-site: name: Build and deploy site - needs: [check, tutorial, test-stats] + needs: [round-info, check, tutorial, test-stats, zenodo-reserve] # Run even if some checker jobs failed, so the site (including the failures) # is still built and deployed; a final step below then fails this job if any - # checker failed. - if: ${{ !cancelled() && needs.check.result != 'skipped' }} + # checker failed. zenodo-reserve is skipped for non-round builds, which is + # covered by !cancelled(). + if: ${{ !cancelled() && needs.check.result != 'skipped' && needs.zenodo-reserve.result != 'failure' }} runs-on: ubuntu-latest permissions: - contents: read + contents: write # to create the release for a round pages: write id-token: write + env: + GH_TOKEN: ${{ github.token }} + # A round is only stamped into the site, released and deposited once its + # DOI has been reserved, which in turn requires every checker to have + # succeeded. A round build with a failing checker still builds and + # deploys the site (and fails at the end), but publishes nothing. + ROUND_READY: ${{ needs.round-info.outputs.is_round == 'true' && needs.zenodo-reserve.result == 'success' }} + ROUND: ${{ needs.round-info.outputs.round }} + SANDBOX: ${{ needs.round-info.outputs.sandbox }} + steps: - name: Checkout repository uses: actions/checkout@v7 @@ -239,7 +368,7 @@ jobs: github_access_token: ${{ secrets.GITHUB_TOKEN }} - name: Setup Pages - if: github.event_name == 'workflow_dispatch' + if: needs.round-info.outputs.deploy == 'true' uses: actions/configure-pages@v6 - name: Setup nix shell @@ -275,7 +404,91 @@ jobs: path: _tarball - name: Generate website - run: ./lka.py build-site --tarball _tarball/lean-arena-tests.tar.gz + run: | + args=(--tarball _tarball/lean-arena-tests.tar.gz) + if [ "$ROUND_READY" = true ]; then + args+=(--round "$ROUND" --doi "$DOI" --zenodo-deposition "$DEPOSITION") + fi + ./lka.py build-site "${args[@]}" + shell: 'nix develop -c bash -euxo pipefail {0}' + env: + DOI: ${{ needs.zenodo-reserve.outputs.doi }} + DEPOSITION: ${{ needs.zenodo-reserve.outputs.deposition_id }} + + # Publish the round: the site as one tarball, plus results.json and the + # test suite separately, which are the two things people actually want to + # download. Every asset is named after its round, since they are read far + # away from the release page that would otherwise say which round they + # are. The site tarball leaves the other two out; the copy assembled + # under /round// below puts them back under the names the archived + # page links to. + - name: Pack the round + if: env.ROUND_READY == 'true' + run: | + mkdir -p /tmp/round + prefix="lean-arena-round-$ROUND" + tar -czf "/tmp/round/$prefix-site.tar.gz" \ + --exclude=results.json \ + --exclude=lean-arena-tests.tar.gz \ + --transform "s,^\\.,$prefix-site," \ + -C _out . + cp _out/results.json "/tmp/round/$prefix-results.json" + cp _out/lean-arena-tests.tar.gz "/tmp/round/$prefix-tests.tar.gz" + ls -l /tmp/round + shell: 'nix develop -c bash -euxo pipefail {0}' + + - name: Create the release + if: env.ROUND_READY == 'true' + run: | + prefix="lean-arena-round-$ROUND" + args=(--title "Round $ROUND" --notes "Round $ROUND of the Lean Kernel Arena.") + if [ "$SANDBOX" = true ]; then args+=(--prerelease); fi + gh release create "$GITHUB_REF_NAME" "${args[@]}" \ + "/tmp/round/$prefix-site.tar.gz" \ + "/tmp/round/$prefix-results.json" \ + "/tmp/round/$prefix-tests.tar.gz" + + - name: Upload the round to Zenodo + if: env.ROUND_READY == 'true' + run: | + prefix="lean-arena-round-$ROUND" + args=() + if [ "$SANDBOX" = true ]; then args+=(--sandbox); fi + .github/zenodo.py "${args[@]}" upload --bucket "$BUCKET" \ + "/tmp/round/$prefix-site.tar.gz" \ + "/tmp/round/$prefix-results.json" \ + "/tmp/round/$prefix-tests.tar.gz" + env: + BUCKET: ${{ needs.zenodo-reserve.outputs.bucket }} + ZENODO_TOKEN: ${{ needs.round-info.outputs.sandbox == 'true' && secrets.ZENODO_SANDBOX_TOKEN || secrets.ZENODO_TOKEN }} + + # Assemble the archive of closed rounds under /round/. This runs after the + # release above, so a build that closes a round already includes itself. + # Test rounds are deliberately not listed. + - name: Assemble previous rounds + if: needs.round-info.outputs.deploy == 'true' + run: | + mkdir -p _out/round + # No match before the first round is closed; pipefail would make that + # an error rather than an empty archive + tags=$(gh release list --limit 100 --json tagName --jq '.[].tagName' \ + | { grep '^round-[0-9]' || true; }) + for tag in $tags; do + round="${tag#round-}" + prefix="lean-arena-round-$round" + echo "::group::Round $round" + gh release download "$tag" --dir "/tmp/rounds/$round" + mkdir -p "_out/round/$round" + tar -xzf "/tmp/rounds/$round/$prefix-site.tar.gz" \ + -C "_out/round/$round" --strip-components=1 + # The archived site links to these relatively and under fixed + # names, so put them back next to it, rather than only offering + # them under their round-qualified names on the release + cp "/tmp/rounds/$round/$prefix-results.json" "_out/round/$round/results.json" + cp "/tmp/rounds/$round/$prefix-tests.tar.gz" "_out/round/$round/lean-arena-tests.tar.gz" + echo "::endgroup::" + done + ./lka.py build-rounds-index --outdir _out/round shell: 'nix develop -c bash -euxo pipefail {0}' # Give each run attempt its own artifact name. Re-running only this job @@ -300,12 +513,24 @@ jobs: archive: false - name: Deploy to GitHub Pages - if: github.event_name == 'workflow_dispatch' + if: needs.round-info.outputs.deploy == 'true' id: deployment uses: actions/deploy-pages@v5 with: artifact_name: github-pages-${{ github.run_attempt }} + # A draft deposition whose build failed would otherwise linger on Zenodo + # and hold on to a DOI that is never published. + - name: Discard the Zenodo draft on failure + if: ${{ failure() && env.ROUND_READY == 'true' && needs.zenodo-reserve.outputs.deposition_id }} + run: | + args=() + if [ "$SANDBOX" = true ]; then args+=(--sandbox); fi + .github/zenodo.py "${args[@]}" discard --deposition "$DEPOSITION" + env: + DEPOSITION: ${{ needs.zenodo-reserve.outputs.deposition_id }} + ZENODO_TOKEN: ${{ needs.round-info.outputs.sandbox == 'true' && secrets.ZENODO_SANDBOX_TOKEN || secrets.ZENODO_TOKEN }} + # The checker matrix uses fail-fast: false, so a failing checker does not # stop the others and the site is still built and deployed above. Surface # the failure by failing this final job once everything else is done. @@ -314,3 +539,28 @@ jobs: run: | echo "::error::One or more checker jobs failed; see the 'Checker: …' matrix jobs." exit 1 + + zenodo-publish: + name: Publish DOI on Zenodo + needs: [round-info, build-site, zenodo-reserve] + if: ${{ needs.round-info.outputs.is_round == 'true' }} + runs-on: ubuntu-latest + permissions: + contents: read + # Publishing mints the DOI and cannot be undone, so this runs as its own + # job: it only starts once build-site has succeeded, i.e. once the release + # exists and the deposition is complete. Practice on a test-round-* tag, + # which does all of this against sandbox.zenodo.org. + steps: + - name: Checkout repository + uses: actions/checkout@v7 + + - name: Publish the deposition + run: | + args=() + if [ "$SANDBOX" = true ]; then args+=(--sandbox); fi + .github/zenodo.py "${args[@]}" publish --deposition "$DEPOSITION" + env: + SANDBOX: ${{ needs.round-info.outputs.sandbox }} + DEPOSITION: ${{ needs.zenodo-reserve.outputs.deposition_id }} + ZENODO_TOKEN: ${{ needs.round-info.outputs.sandbox == 'true' && secrets.ZENODO_SANDBOX_TOKEN || secrets.ZENODO_TOKEN }} diff --git a/.github/zenodo.py b/.github/zenodo.py new file mode 100644 index 0000000..3636635 --- /dev/null +++ b/.github/zenodo.py @@ -0,0 +1,245 @@ +#!/usr/bin/env python3 +"""Deposit a closed round on Zenodo, to give it a citable DOI. + +The DOI has to be known *before* the site is built, because it is shown on the +round's index page. Zenodo supports this: creating a deposition reserves a DOI +that only becomes active on publication. The round build therefore runs + + reserve -> create a draft deposition, print its pre-reserved DOI + (build the site with that DOI baked in) + upload -> attach the built files to the draft + publish -> make the record (and the DOI) public + +with `publish` gated behind a manual approval, since publishing is +irreversible. `discard` deletes an unpublished draft again, for failed builds. + +Rounds after the first are created as new versions of the previous round's +deposition (`--previous-deposition`). That gives them a shared concept DOI +that always resolves to the newest round, next to the per-round DOIs. + +Uses only the standard library, so it needs no dependencies beyond the Python +in the dev shell. Authentication is via the ZENODO_TOKEN environment variable. +""" + +import argparse +import datetime +import json +import os +import sys +import urllib.error +import urllib.request +from pathlib import Path + +# Static deposition metadata (creators, license, ...) lives in the repository +# so that it can be reviewed and changed without touching this script. +METADATA_FILE = Path(__file__).resolve().parent.parent / ".zenodo.json" + +REPO_URL = "https://github.com/leanprover/lean-kernel-arena" + + +def api_base(sandbox: bool) -> str: + return "https://sandbox.zenodo.org" if sandbox else "https://zenodo.org" + + +def request(method: str, url: str, token: str, data=None, content_type="application/json"): + """Perform an API request and return the parsed JSON response (or None).""" + body = json.dumps(data).encode() if data is not None else None + req = urllib.request.Request(url, data=body, method=method) + req.add_header("Authorization", f"Bearer {token}") + if body is not None: + req.add_header("Content-Type", content_type) + try: + with urllib.request.urlopen(req) as response: + raw = response.read() + except urllib.error.HTTPError as e: + detail = e.read().decode(errors="replace") + sys.exit(f"Zenodo API error: {method} {url} -> {e.code} {e.reason}\n{detail}") + if not raw: + return None + return json.loads(raw) + + +def upload_file(bucket_url: str, path: Path, token: str) -> None: + """Upload one file to a deposition's bucket (streamed, not read into memory).""" + url = f"{bucket_url}/{path.name}" + size = path.stat().st_size + with open(path, "rb") as f: + req = urllib.request.Request(url, data=f, method="PUT") + req.add_header("Authorization", f"Bearer {token}") + req.add_header("Content-Type", "application/octet-stream") + req.add_header("Content-Length", str(size)) + try: + with urllib.request.urlopen(req) as response: + response.read() + except urllib.error.HTTPError as e: + detail = e.read().decode(errors="replace") + sys.exit(f"Zenodo upload failed: {path.name} -> {e.code} {e.reason}\n{detail}") + print(f"Uploaded {path.name} ({size} bytes)") + + +def deposition_metadata(round_name: str) -> dict: + """Build the deposition metadata for a round from .zenodo.json.""" + with open(METADATA_FILE, "r") as f: + # Keys starting with an underscore are comments for human readers; + # Zenodo rejects metadata fields it does not know. + metadata = {k: v for k, v in json.load(f).items() if not k.startswith("_")} + metadata["title"] = f"Lean Kernel Arena, Round {round_name}" + metadata["version"] = round_name + metadata["publication_date"] = datetime.date.today().isoformat() + related = list(metadata.get("related_identifiers", [])) + related.append({ + "relation": "isSupplementTo", + "identifier": f"{REPO_URL}/releases/tag/round-{round_name}", + "resource_type": "software", + }) + metadata["related_identifiers"] = related + return metadata + + +def prereserved_doi(deposition: dict) -> str: + doi = deposition.get("metadata", {}).get("prereserve_doi", {}).get("doi") + if not doi: + sys.exit(f"Zenodo did not pre-reserve a DOI for deposition {deposition.get('id')}") + return doi + + +def emit_outputs(**outputs) -> None: + """Print outputs, and write them to $GITHUB_OUTPUT when running in Actions.""" + lines = [f"{key}={value}" for key, value in outputs.items()] + for line in lines: + print(line) + github_output = os.environ.get("GITHUB_OUTPUT") + if github_output: + with open(github_output, "a") as f: + f.write("\n".join(lines) + "\n") + + +def cmd_reserve(args: argparse.Namespace, token: str) -> None: + base = api_base(args.sandbox) + + if args.previous_deposition: + # Continue the version chain, so all rounds share a concept DOI + print(f"Creating a new version of deposition {args.previous_deposition}") + result = request( + "POST", + f"{base}/api/deposit/depositions/{args.previous_deposition}/actions/newversion", + token, + ) + draft_url = result.get("links", {}).get("latest_draft") + if not draft_url: + sys.exit(f"Zenodo returned no draft for the new version of {args.previous_deposition}") + deposition = request("GET", draft_url, token) + # A new version inherits the previous version's files. Drop them: the + # site tarball is named after its round, so the previous round's copy + # would otherwise linger in this record next to this round's own. + for existing in deposition.get("files", []): + request( + "DELETE", + f"{base}/api/deposit/depositions/{deposition['id']}/files/{existing['id']}", + token, + ) + print(f"Removed inherited file {existing.get('filename')}") + else: + print("Creating a new deposition (first round)") + deposition = request("POST", f"{base}/api/deposit/depositions", token, data={}) + + deposition_id = deposition["id"] + doi = prereserved_doi(deposition) + + updated = request( + "PUT", + f"{base}/api/deposit/depositions/{deposition_id}", + token, + data={"metadata": deposition_metadata(args.round)}, + ) + + # Setting metadata must not disturb the reservation: the DOI is about to be + # baked into the built site, so a changed one has to fail the build. + if prereserved_doi(updated) != doi: + sys.exit( + f"Pre-reserved DOI changed from {doi} to {prereserved_doi(updated)} " + f"while setting metadata; aborting rather than publishing a wrong DOI" + ) + + bucket = updated.get("links", {}).get("bucket") + if not bucket: + sys.exit(f"Deposition {deposition_id} has no file bucket") + + emit_outputs( + doi=doi, + deposition_id=deposition_id, + bucket=bucket, + deposition_url=f"{base}/deposit/{deposition_id}", + ) + + +def cmd_upload(args: argparse.Namespace, token: str) -> None: + for name in args.files: + path = Path(name) + if not path.is_file(): + sys.exit(f"Not a file: {path}") + upload_file(args.bucket, path, token) + + +def cmd_publish(args: argparse.Namespace, token: str) -> None: + base = api_base(args.sandbox) + result = request( + "POST", + f"{base}/api/deposit/depositions/{args.deposition}/actions/publish", + token, + ) + doi = result.get("doi") + print(f"Published {result.get('links', {}).get('record_html')} as {doi}") + emit_outputs(doi=doi, concept_doi=result.get("conceptdoi", "")) + + +def cmd_discard(args: argparse.Namespace, token: str) -> None: + """Delete an unpublished draft, so a failed build leaves nothing behind.""" + base = api_base(args.sandbox) + request("DELETE", f"{base}/api/deposit/depositions/{args.deposition}", token) + print(f"Discarded draft deposition {args.deposition}") + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--sandbox", + action="store_true", + help="Use sandbox.zenodo.org instead of zenodo.org (for test-round-* tags)", + ) + subparsers = parser.add_subparsers(dest="command", required=True) + + reserve = subparsers.add_parser("reserve", help="Create a draft deposition and pre-reserve its DOI") + reserve.add_argument("--round", required=True, help="Round name, e.g. 2026-10") + reserve.add_argument( + "--previous-deposition", + help="Deposition id of the previous round; the new round becomes a new version of it", + ) + + upload = subparsers.add_parser("upload", help="Upload files to a draft deposition") + upload.add_argument("--bucket", required=True, help="Bucket URL reported by reserve") + upload.add_argument("files", nargs="+", help="Files to upload") + + publish = subparsers.add_parser("publish", help="Publish a draft deposition (irreversible)") + publish.add_argument("--deposition", required=True, help="Deposition id reported by reserve") + + discard = subparsers.add_parser("discard", help="Delete an unpublished draft deposition") + discard.add_argument("--deposition", required=True, help="Deposition id reported by reserve") + + args = parser.parse_args() + + token = os.environ.get("ZENODO_TOKEN") + if not token: + sys.exit("ZENODO_TOKEN is not set") + + { + "reserve": cmd_reserve, + "upload": cmd_upload, + "publish": cmd_publish, + "discard": cmd_discard, + }[args.command](args, token) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/.zenodo.json b/.zenodo.json new file mode 100644 index 0000000..94decd5 --- /dev/null +++ b/.zenodo.json @@ -0,0 +1,39 @@ +{ + "upload_type": "dataset", + "license": "apache-2.0", + "access_right": "open", + "description": "

A round of the Lean Kernel Arena: a snapshot of the benchmark results for proof checkers of the Lean theorem prover, comprising the rendered result site, the raw results as results.json, and the test suite the round was run against.

Results are only comparable within a round, since the checkers, the tests and the Lean version they are measured against all change between rounds.

", + "_comment_creators": [ + "Zenodo requires at least one creator, so this cannot be left empty.", + "Naming the project rather than individuals sidesteps having to decide who", + "counts as an author of a round: the checkers being measured are written by", + "people who are not authors of the arena, and the reverse. A name without a", + "comma is passed through verbatim, so this renders as an organizational", + "author. Whoever closes a round is named below as its editor instead." + ], + "creators": [ + { + "name": "The Lean Kernel Arena contributors" + } + ], + "contributors": [ + { + "name": "Breitner, Joachim", + "type": "Editor" + } + ], + "keywords": [ + "Lean", + "theorem prover", + "proof checking", + "kernel", + "benchmark" + ], + "related_identifiers": [ + { + "relation": "isSupplementTo", + "identifier": "https://github.com/leanprover/lean-kernel-arena", + "resource_type": "software" + } + ] +} diff --git a/README.md b/README.md index dcd69c1..6323c56 100644 --- a/README.md +++ b/README.md @@ -200,6 +200,64 @@ If it is already known that a checker cannot handle a test, and running it would The arena does not automatically update the checkers; please submit new releases manually. +## Rounds + +The arena runs in **rounds**. shows the round +currently in progress, rebuilt whenever checkers or tests change. Closing a +round archives it unchanged under +, so that results stay +referenceable even as checkers, tests and the Lean version they are measured +against move on. + +Rounds are named after a year and a month, e.g. `2026-10`, but are closed +whenever it seems right rather than on a schedule. + +### Closing a round + +Push a tag `round-`: + +```bash +git tag round-2026-10 +git push origin round-2026-10 +``` + +This runs the full CI build (no tests are skipped), and then: + +1. reserves a DOI on Zenodo, +2. builds the site with the round name and DOI baked in, +3. creates the GitHub release `round-2026-10` with three assets, each named + after the round: the whole site as `lean-arena-round-2026-10-site.tar.gz`, + the raw results as `lean-arena-round-2026-10-results.json`, and the test + suite as `lean-arena-round-2026-10-tests.tar.gz`, +4. uploads those to Zenodo as a draft deposition, +5. reassembles `/round/` from all round releases and deploys the site, +6. publishes the Zenodo record, which mints the DOI. + +Publishing cannot be undone, so it happens last, once everything else has +succeeded. If an earlier step fails, the draft deposition is discarded again +and no DOI is minted. + +Each round is deposited as a new version of the previous one, so all rounds +share a concept DOI that resolves to the most recent round, next to their +individual per-round DOIs. The deposition id needed for this is recorded in +each round's own `results.json`. + +### Trying it out + +A tag `test-round-` runs exactly the same thing, but against +[sandbox.zenodo.org](https://sandbox.zenodo.org) and without deploying the +site. Delete the tag and the GitHub release afterwards and nothing remains. +The tag does not have to be on `master`, so a change to the round machinery +can be exercised end to end while it is still a pull request. + +CI needs two secrets: `ZENODO_TOKEN` and `ZENODO_SANDBOX_TOKEN`, each a +personal access token with the `deposit:write` and `deposit:actions` scopes, +from zenodo.org and sandbox.zenodo.org respectively. + +The deposition metadata (authors, license, keywords) lives in +[`.zenodo.json`](.zenodo.json); title, version and publication date are filled +in per round. + ## Fair Play Checkers are not run in a sandbox. We assume good faith from all contributors. The goal is to collaboratively improve Lean kernel implementations, not to exploit the test environment. Malicious submissions will be rejected. diff --git a/lka.py b/lka.py index 87a2f9c..da63d58 100755 --- a/lka.py +++ b/lka.py @@ -55,6 +55,20 @@ def _configure_stdout_stderr_unbuffered() -> None: # test tarball. TEST_SIZE_LIMIT = 10 * 1024 * 1024 +# The canonical location of the published site. Used for the "other rounds" +# link, which has to be absolute: archived rounds are served from +# /round// and are also distributed as standalone tarballs, so a +# relative link back to the round index would not survive both. +SITE_URL = "https://arena.lean-lang.org" +ROUNDS_URL = f"{SITE_URL}/round/" + +# The GitHub repository, used for links to releases and source files. +REPO_URL = "https://github.com/leanprover/lean-kernel-arena" + +# A round named "2026-10" is released as the tag "round-2026-10" and served +# from "/round/2026-10/". +ROUND_TAG_PREFIX = "round-" + # Timing/measurement utilities @@ -1606,6 +1620,13 @@ def get_build_metadata() -> dict: "git_revision_short": None, "github_url": None, "github_action_url": None, + # Round metadata, filled in by build-site from its --round/--doi/ + # --zenodo-deposition options. A build without a round name is the + # ongoing round ("Round in progress"); only a release build off a + # round-* tag names a round and carries a DOI. + "round": None, + "doi": None, + "zenodo_deposition": None, } # Get git revision @@ -1667,9 +1688,8 @@ def generate_source_links(config: dict, config_type: str, git_revision: str | No return links # Generate declaration URL (YAML file in GitHub) - base_github_url = "https://github.com/leanprover/lean-kernel-arena" declaration_path = f"{config_type}/{config['name']}.yaml" - links["declaration_url"] = f"{base_github_url}/blob/{git_revision}/{declaration_path}" + links["declaration_url"] = f"{REPO_URL}/blob/{git_revision}/{declaration_path}" # Generate source URL url = config.get("url") @@ -1695,10 +1715,10 @@ def generate_source_links(config: dict, config_type: str, git_revision: str | No source_path = f"checkers/{local_dir}" else: source_path = local_dir - links["source_url"] = f"{base_github_url}/tree/{git_revision}/{source_path}" + links["source_url"] = f"{REPO_URL}/tree/{git_revision}/{source_path}" elif leanfile: # Lean file in this repository - links["source_url"] = f"{base_github_url}/blob/{git_revision}/{leanfile}" + links["source_url"] = f"{REPO_URL}/blob/{git_revision}/{leanfile}" return links @@ -1876,6 +1896,83 @@ def cmd_write_results(args: argparse.Namespace) -> int: return 0 +def cmd_build_rounds_index(args: argparse.Namespace) -> int: + """Handle the build-rounds-index command. + + Renders /round/index.html from the rounds already unpacked into the output + directory, one subdirectory per round. Everything shown is read from each + round's own results.json, so adding a round needs no changes here and the + archived rounds stay the single source of truth about themselves. + """ + rounds_dir = Path(args.outdir) + if not rounds_dir.is_dir(): + print(f"Rounds directory not found: {rounds_dir}") + return 1 + + rounds = [] + for round_dir in sorted(rounds_dir.iterdir()): + if not round_dir.is_dir(): + continue + results_file = round_dir / "results.json" + if not results_file.exists(): + print(f"Error: {round_dir} has no results.json") + return 1 + with open(results_file, "r") as f: + data = json.load(f) + meta = data.get("meta", {}) + name = meta.get("round") or round_dir.name + if name != round_dir.name: + print(f"Error: {results_file} is for round {name}, but sits in {round_dir.name}/") + return 1 + tarball = round_dir / "lean-arena-tests.tar.gz" + rounds.append({ + "name": name, + "timestamp": meta.get("timestamp"), + "doi": meta.get("doi"), + "release_url": meta.get("release_url", + f"{REPO_URL}/releases/tag/{ROUND_TAG_PREFIX}{name}"), + "git_revision": meta.get("git_revision"), + "git_revision_short": meta.get("git_revision_short"), + "github_url": meta.get("github_url"), + "checker_count": len(data.get("checkers", [])), + "test_count": len(data.get("tests", [])), + "results_json_size": results_file.stat().st_size, + "tarball_size": tarball.stat().st_size if tarball.exists() else None, + }) + + # Newest round first + rounds.sort(key=lambda r: r["name"], reverse=True) + + templates_dir = get_project_root() / "templates" + env = make_template_env(templates_dir) + template = env.get_template("rounds.html") + output_file = rounds_dir / "index.html" + template.stream({ + "rounds": rounds, + "format_memory": format_memory, + "build_info": get_build_metadata(), + # /round/index.html sits one level below the site root + "root_path": "../", + }).dump(str(output_file)) + print(f"Generated: {output_file} ({len(rounds)} rounds)") + return 0 + + +def make_template_env(templates_dir: Path) -> Environment: + """Create the Jinja environment used for all rendered pages. + + Pages locate their assets through the `root_path` context variable (the + relative path from the page to the site root), so that the whole site + stays relocatable and can be unpacked under /round//. + """ + env = Environment( + loader=FileSystemLoader(templates_dir), + autoescape=select_autoescape(), + ) + env.globals["rounds_url"] = ROUNDS_URL + return env + + def cmd_build_site(args: argparse.Namespace) -> int: """Handle the build-site command.""" output_dir = Path(args.outdir) @@ -1886,10 +1983,7 @@ def cmd_build_site(args: argparse.Namespace) -> int: print(f"Templates directory not found: {templates_dir}") return 1 - env = Environment( - loader=FileSystemLoader(templates_dir), - autoescape=select_autoescape(), - ) + env = make_template_env(templates_dir) env.globals["format_relative_perf"] = format_relative_perf # The site is rendered from the results.json data structure, either read @@ -1900,6 +1994,21 @@ def cmd_build_site(args: argparse.Namespace) -> int: else: results_data = collect_results_data() + # Stamp the round this build belongs to into the metadata, so that + # results.json is self-describing and the round index can be built from + # the results.json files of the individual rounds alone. + meta = results_data.setdefault("meta", {}) + for key in ("round", "doi", "zenodo_deposition"): + meta.setdefault(key, None) + if args.round: + meta["round"] = args.round + if args.doi: + meta["doi"] = args.doi + if args.zenodo_deposition: + meta["zenodo_deposition"] = int(args.zenodo_deposition) + if meta["round"]: + meta["release_url"] = f"{REPO_URL}/releases/tag/{ROUND_TAG_PREFIX}{meta['round']}" + # Publish the raw data alongside the site results_json_file = output_dir / "results.json" with open(results_json_file, "w") as f: @@ -2036,6 +2145,7 @@ def sort_key(checker): "build_info": build_info, "tarball_info": tarball_info, "results_json_info": results_json_info, + "root_path": "", } # Render index.html @@ -2126,6 +2236,7 @@ def sort_key(checker): "convert_instructions_to_time": convert_instructions_to_time, "instructions_per_second": instructions_per_second, "build_info": build_info, + "root_path": "../../", } output_file = checker_dir / "index.html" @@ -2379,6 +2490,31 @@ def main() -> int: metavar="FILE", help="Use a pre-built test tarball instead of creating one (see build-tarball)", ) + build_site_parser.add_argument( + "--round", + metavar="NAME", + help="Name of the round this build closes, e.g. 2026-10 (default: no round, i.e. the ongoing round)", + ) + build_site_parser.add_argument( + "--doi", + help="DOI of this round, shown for citation (pre-reserved on Zenodo before the build)", + ) + build_site_parser.add_argument( + "--zenodo-deposition", + metavar="ID", + help="Zenodo deposition id of this round, recorded in results.json so the next round can be created as a new version of it", + ) + + # build-rounds-index command + build_rounds_index_parser = subparsers.add_parser( + "build-rounds-index", + help="Build the index page listing all archived rounds", + ) + build_rounds_index_parser.add_argument( + "--outdir", + default="_out/round", + help="Directory holding the unpacked rounds, one subdirectory per round (default: _out/round)", + ) # build-tarball command build_tarball_parser = subparsers.add_parser( @@ -2462,6 +2598,8 @@ def main() -> int: return cmd_run_checker(args) elif args.command == "build-site": return cmd_build_site(args) + elif args.command == "build-rounds-index": + return cmd_build_rounds_index(args) elif args.command == "write-results": return cmd_write_results(args) elif args.command == "build-tarball": diff --git a/templates/base.html b/templates/base.html index a2b4248..a4fa2da 100644 --- a/templates/base.html +++ b/templates/base.html @@ -4,8 +4,10 @@ {% block title %}Lean Kernel Arena{% endblock %} - - + {# Chota is vendored rather than loaded from a CDN: archived rounds are + frozen artifacts that must still render years from now. #} + + @@ -14,6 +16,12 @@

{% block h1 %}Lean Kernel Arena{% endblock %}

+ {% block round_line %} +

+ {% if build_info.round %}Round {{ build_info.round }}{% else %}Round in progress{% endif %} + · other rounds +

+ {% endblock %}
diff --git a/templates/checker.html b/templates/checker.html index 40e2bfe..7b93db5 100644 --- a/templates/checker.html +++ b/templates/checker.html @@ -14,8 +14,6 @@ {% endmacro %} -{% block static_path %}../../{% endblock %} - {% block title %}{{ checker.name }} - Lean Kernel Arena{% endblock %} {% block h1 %}Lean Kernel Arena / {{ checker.name }} diff --git a/templates/index.html b/templates/index.html index e4a4edd..2a75275 100644 --- a/templates/index.html +++ b/templates/index.html @@ -1,7 +1,5 @@ {% extends "base.html" %} -{% block static_path %}{% endblock %} - {# One test row in the Tests table; group members are shown indented, without the group prefix #} {% macro test_row(test, group) %} @@ -280,5 +278,32 @@

Details

We are interested in extending our test suite, in particular tests that should be rejected are a useful help for authors of new kernel checkers.

+ + +
+
+

Rounds

+
+ +

+ {% if build_info.round %} + This page is the archived round {{ build_info.round }}, closed on {{ build_info.timestamp }}. It is not updated any more; the round currently in progress and all other rounds are listed on the rounds page. + {% else %} + The arena runs in rounds. This page shows the round currently in progress, rebuilt whenever checkers or tests change; results from earlier, closed rounds are archived on the rounds page. + {% endif %} + Results are only really comparable within a round, since checkers, tests and the Lean version they are measured against all move between rounds. +

+ + {% if build_info.doi %} +
+

+ This round is archived on Zenodo and can be cited as: +

+

+ Lean Kernel Arena, Round {{ build_info.round }}. https://doi.org/{{ build_info.doi }} +

+
+ {% endif %} +
{% endblock %} diff --git a/templates/rounds.html b/templates/rounds.html new file mode 100644 index 0000000..d1122a8 --- /dev/null +++ b/templates/rounds.html @@ -0,0 +1,83 @@ +{% extends "base.html" %} + +{% block title %}Rounds - Lean Kernel Arena{% endblock %} + +{% block h1 %}Lean Kernel Arena / Rounds{% endblock %} + +{# This page *is* the round index, so it does not link to itself #} +{% block round_line %}{% endblock %} + +{% block style %} +td.round-name { + white-space: nowrap; +} +{% endblock %} + +{% block content %} +
+

+ The Lean Kernel Arena runs in rounds. The + main page shows the round currently in + progress, which is rebuilt whenever checkers or tests change. When a + round is closed, its site is archived here unchanged, together with the + raw results and the test suite it was run against. +

+ +

+ Results are only really comparable within a round: checkers, + tests and the Lean version they are measured against all move between + rounds, and the timings depend on the machine the round happened to run + on. +

+
+ +
+
+

Closed rounds

+
+ {% if rounds %} +
+ + + + + + + + + + + + + {% for round in rounds %} + + + + + + + + + {% endfor %} + +
RoundClosedCheckersTestsDownloadsCitation
{{ round.name }}{{ round.timestamp or '-' }}{{ round.checker_count }}{{ round.test_count }} + results.json + ({{ format_memory(round.results_json_size) }}) + {% if round.tarball_size %} + · tests + ({{ format_memory(round.tarball_size) }}) + {% endif %} + · release + + {% if round.doi %} + {{ round.doi }} + {% else %} + - + {% endif %} +
+
+ {% else %} +

No rounds have been closed yet.

+ {% endif %} +
+{% endblock %} diff --git a/templates/static/chota.min.css b/templates/static/chota.min.css new file mode 100644 index 0000000..e73dc6c --- /dev/null +++ b/templates/static/chota.min.css @@ -0,0 +1,3 @@ +/*! + * chota.css v0.9.2 | MIT License | https://github.com/jenil/chota + */:root{--bg-color:#fff;--bg-secondary-color:#f3f3f6;--color-primary:#14854f;--color-lightGrey:#d2d6dd;--color-grey:#747681;--color-darkGrey:#3f4144;--color-error:#d43939;--color-success:#28bd14;--grid-maxWidth:120rem;--grid-gutter:2rem;--font-size:1.6rem;--font-color:#333;--font-family-sans:-apple-system,"BlinkMacSystemFont","Avenir","Avenir Next","Segoe UI","Roboto","Oxygen","Ubuntu","Cantarell","Fira Sans","Droid Sans","Helvetica Neue",sans-serif;--font-family-mono:monaco,"Consolas","Lucida Console",monospace}html{-webkit-text-size-adjust:100%;-moz-text-size-adjust:100%;-ms-text-size-adjust:100%;text-size-adjust:100%;-webkit-box-sizing:border-box;box-sizing:border-box;font-size:62.5%;line-height:1.15}*,:after,:before{-webkit-box-sizing:inherit;box-sizing:inherit}body{background-color:var(--bg-color);color:var(--font-color);font-family:Segoe UI,Helvetica Neue,sans-serif;font-family:var(--font-family-sans);font-size:var(--font-size);line-height:1.6;margin:0;padding:0}h1,h2,h3,h4,h5,h6{font-weight:500;margin:.35em 0 .7em}h1{font-size:2em}h2{font-size:1.75em}h3{font-size:1.5em}h4{font-size:1.25em}h5{font-size:1em}h6{font-size:.85em}a{color:var(--color-primary);text-decoration:none}a:hover:not(.button){opacity:.75}button{font-family:inherit}p{margin-top:0}blockquote{background-color:var(--bg-secondary-color);border-left:3px solid var(--color-lightGrey);padding:1.5rem 2rem}dl dt{font-weight:700}hr{background-color:var(--color-lightGrey);height:1px;margin:1rem 0}hr,table{border:none}table{border-collapse:collapse;border-spacing:0;text-align:left;width:100%}table.striped tr:nth-of-type(2n){background-color:var(--bg-secondary-color)}td,th{padding:1.2rem .4rem;vertical-align:middle}thead{border-bottom:2px solid var(--color-lightGrey)}tfoot{border-top:2px solid var(--color-lightGrey)}code,kbd,pre,samp,tt{font-family:var(--font-family-mono)}code,kbd{border-radius:4px;color:var(--color-error);font-size:90%;padding:.2em .4em;white-space:pre-wrap}code,kbd,pre{background-color:var(--bg-secondary-color)}pre{font-size:1em;overflow-x:auto;padding:1rem}pre code{background:none;padding:0}abbr[title]{border-bottom:none;text-decoration:underline;-webkit-text-decoration:underline dotted;text-decoration:underline dotted}img{max-width:100%}fieldset{border:1px solid var(--color-lightGrey)}iframe{border:0}.container{margin:0 auto;max-width:var(--grid-maxWidth);padding:0 calc(var(--grid-gutter)/2);width:96%}.row{-webkit-box-direction:normal;-webkit-box-pack:start;-ms-flex-pack:start;display:-webkit-box;display:-ms-flexbox;display:flex;-ms-flex-flow:row wrap;flex-flow:row wrap;justify-content:flex-start;margin-left:calc(var(--grid-gutter)/-2);margin-right:calc(var(--grid-gutter)/-2)}.row,.row.reverse{-webkit-box-orient:horizontal}.row.reverse{-webkit-box-direction:reverse;-ms-flex-direction:row-reverse;flex-direction:row-reverse}.col{-webkit-box-flex:1;-ms-flex:1;flex:1}.col,[class*=" col-"],[class^=col-]{margin:0 calc(var(--grid-gutter)/2) calc(var(--grid-gutter)/2)}.col-1{-ms-flex:0 0 calc(8.33333% - var(--grid-gutter));flex:0 0 calc(8.33333% - var(--grid-gutter));max-width:calc(8.33333% - var(--grid-gutter))}.col-1,.col-2{-webkit-box-flex:0}.col-2{-ms-flex:0 0 calc(16.66667% - var(--grid-gutter));flex:0 0 calc(16.66667% - var(--grid-gutter));max-width:calc(16.66667% - var(--grid-gutter))}.col-3{-ms-flex:0 0 calc(25% - var(--grid-gutter));flex:0 0 calc(25% - var(--grid-gutter));max-width:calc(25% - var(--grid-gutter))}.col-3,.col-4{-webkit-box-flex:0}.col-4{-ms-flex:0 0 calc(33.33333% - var(--grid-gutter));flex:0 0 calc(33.33333% - var(--grid-gutter));max-width:calc(33.33333% - var(--grid-gutter))}.col-5{-ms-flex:0 0 calc(41.66667% - var(--grid-gutter));flex:0 0 calc(41.66667% - var(--grid-gutter));max-width:calc(41.66667% - var(--grid-gutter))}.col-5,.col-6{-webkit-box-flex:0}.col-6{-ms-flex:0 0 calc(50% - var(--grid-gutter));flex:0 0 calc(50% - var(--grid-gutter));max-width:calc(50% - var(--grid-gutter))}.col-7{-ms-flex:0 0 calc(58.33333% - var(--grid-gutter));flex:0 0 calc(58.33333% - var(--grid-gutter));max-width:calc(58.33333% - var(--grid-gutter))}.col-7,.col-8{-webkit-box-flex:0}.col-8{-ms-flex:0 0 calc(66.66667% - var(--grid-gutter));flex:0 0 calc(66.66667% - var(--grid-gutter));max-width:calc(66.66667% - var(--grid-gutter))}.col-9{-ms-flex:0 0 calc(75% - var(--grid-gutter));flex:0 0 calc(75% - var(--grid-gutter));max-width:calc(75% - var(--grid-gutter))}.col-10,.col-9{-webkit-box-flex:0}.col-10{-ms-flex:0 0 calc(83.33333% - var(--grid-gutter));flex:0 0 calc(83.33333% - var(--grid-gutter));max-width:calc(83.33333% - var(--grid-gutter))}.col-11{-ms-flex:0 0 calc(91.66667% - var(--grid-gutter));flex:0 0 calc(91.66667% - var(--grid-gutter));max-width:calc(91.66667% - var(--grid-gutter))}.col-11,.col-12{-webkit-box-flex:0}.col-12{-ms-flex:0 0 calc(100% - var(--grid-gutter));flex:0 0 calc(100% - var(--grid-gutter));max-width:calc(100% - var(--grid-gutter))}@media screen and (max-width:599px){.container{width:100%}.col,[class*=col-],[class^=col-]{-webkit-box-flex:0;-ms-flex:0 1 100%;flex:0 1 100%;max-width:100%}}@media screen and (min-width:900px){.col-1-md{-webkit-box-flex:0;-ms-flex:0 0 calc(8.33333% - var(--grid-gutter));flex:0 0 calc(8.33333% - var(--grid-gutter));max-width:calc(8.33333% - var(--grid-gutter))}.col-2-md{-webkit-box-flex:0;-ms-flex:0 0 calc(16.66667% - var(--grid-gutter));flex:0 0 calc(16.66667% - var(--grid-gutter));max-width:calc(16.66667% - var(--grid-gutter))}.col-3-md{-webkit-box-flex:0;-ms-flex:0 0 calc(25% - var(--grid-gutter));flex:0 0 calc(25% - var(--grid-gutter));max-width:calc(25% - var(--grid-gutter))}.col-4-md{-webkit-box-flex:0;-ms-flex:0 0 calc(33.33333% - var(--grid-gutter));flex:0 0 calc(33.33333% - var(--grid-gutter));max-width:calc(33.33333% - var(--grid-gutter))}.col-5-md{-webkit-box-flex:0;-ms-flex:0 0 calc(41.66667% - var(--grid-gutter));flex:0 0 calc(41.66667% - var(--grid-gutter));max-width:calc(41.66667% - var(--grid-gutter))}.col-6-md{-webkit-box-flex:0;-ms-flex:0 0 calc(50% - var(--grid-gutter));flex:0 0 calc(50% - var(--grid-gutter));max-width:calc(50% - var(--grid-gutter))}.col-7-md{-webkit-box-flex:0;-ms-flex:0 0 calc(58.33333% - var(--grid-gutter));flex:0 0 calc(58.33333% - var(--grid-gutter));max-width:calc(58.33333% - var(--grid-gutter))}.col-8-md{-webkit-box-flex:0;-ms-flex:0 0 calc(66.66667% - var(--grid-gutter));flex:0 0 calc(66.66667% - var(--grid-gutter));max-width:calc(66.66667% - var(--grid-gutter))}.col-9-md{-webkit-box-flex:0;-ms-flex:0 0 calc(75% - var(--grid-gutter));flex:0 0 calc(75% - var(--grid-gutter));max-width:calc(75% - var(--grid-gutter))}.col-10-md{-webkit-box-flex:0;-ms-flex:0 0 calc(83.33333% - var(--grid-gutter));flex:0 0 calc(83.33333% - var(--grid-gutter));max-width:calc(83.33333% - var(--grid-gutter))}.col-11-md{-webkit-box-flex:0;-ms-flex:0 0 calc(91.66667% - var(--grid-gutter));flex:0 0 calc(91.66667% - var(--grid-gutter));max-width:calc(91.66667% - var(--grid-gutter))}.col-12-md{-webkit-box-flex:0;-ms-flex:0 0 calc(100% - var(--grid-gutter));flex:0 0 calc(100% - var(--grid-gutter));max-width:calc(100% - var(--grid-gutter))}}@media screen and (min-width:1200px){.col-1-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(8.33333% - var(--grid-gutter));flex:0 0 calc(8.33333% - var(--grid-gutter));max-width:calc(8.33333% - var(--grid-gutter))}.col-2-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(16.66667% - var(--grid-gutter));flex:0 0 calc(16.66667% - var(--grid-gutter));max-width:calc(16.66667% - var(--grid-gutter))}.col-3-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(25% - var(--grid-gutter));flex:0 0 calc(25% - var(--grid-gutter));max-width:calc(25% - var(--grid-gutter))}.col-4-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(33.33333% - var(--grid-gutter));flex:0 0 calc(33.33333% - var(--grid-gutter));max-width:calc(33.33333% - var(--grid-gutter))}.col-5-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(41.66667% - var(--grid-gutter));flex:0 0 calc(41.66667% - var(--grid-gutter));max-width:calc(41.66667% - var(--grid-gutter))}.col-6-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(50% - var(--grid-gutter));flex:0 0 calc(50% - var(--grid-gutter));max-width:calc(50% - var(--grid-gutter))}.col-7-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(58.33333% - var(--grid-gutter));flex:0 0 calc(58.33333% - var(--grid-gutter));max-width:calc(58.33333% - var(--grid-gutter))}.col-8-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(66.66667% - var(--grid-gutter));flex:0 0 calc(66.66667% - var(--grid-gutter));max-width:calc(66.66667% - var(--grid-gutter))}.col-9-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(75% - var(--grid-gutter));flex:0 0 calc(75% - var(--grid-gutter));max-width:calc(75% - var(--grid-gutter))}.col-10-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(83.33333% - var(--grid-gutter));flex:0 0 calc(83.33333% - var(--grid-gutter));max-width:calc(83.33333% - var(--grid-gutter))}.col-11-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(91.66667% - var(--grid-gutter));flex:0 0 calc(91.66667% - var(--grid-gutter));max-width:calc(91.66667% - var(--grid-gutter))}.col-12-lg{-webkit-box-flex:0;-ms-flex:0 0 calc(100% - var(--grid-gutter));flex:0 0 calc(100% - var(--grid-gutter));max-width:calc(100% - var(--grid-gutter))}}fieldset{padding:.5rem 2rem}legend{font-size:.8em;letter-spacing:.1rem;text-transform:uppercase}input:not([type=checkbox],[type=radio],[type=submit],[type=color],[type=button],[type=reset]),select,textarea,textarea[type=text]{border:1px solid var(--color-lightGrey);border-radius:4px;display:block;font-family:inherit;font-size:1em;padding:.8rem 1rem;-webkit-transition:all .2s ease;transition:all .2s ease;width:100%}select{-webkit-appearance:none;-moz-appearance:none;appearance:none;background:#f3f3f6 no-repeat 100%;background-image:url("data:image/svg+xml;utf8,");background-origin:content-box;background-size:1ex}.button,[type=button],[type=reset],[type=submit],button{background:var(--color-lightGrey);border:1px solid transparent;border-radius:4px;color:var(--color-darkGrey);cursor:pointer;display:inline-block;font-size:var(--font-size);line-height:1;padding:1rem 2.5rem;text-align:center;text-decoration:none;-webkit-transform:scale(1);transform:scale(1);-webkit-transition:opacity .2s ease;transition:opacity .2s ease}.button.dark,.button.error,.button.primary,.button.secondary,.button.success,[type=submit]{background-color:#000;background-color:var(--color-primary);color:#fff;z-index:1}.button:hover,[type=button]:hover,[type=reset]:hover,[type=submit]:hover,button:hover{opacity:.8}button:disabled,button:disabled:hover,input:disabled,input:disabled:hover{cursor:not-allowed;opacity:.4}.grouped{display:-webkit-box;display:-ms-flexbox;display:flex}.grouped>:not(:last-child){margin-right:16px}.grouped.gapless>*{border-radius:0!important;margin:0 0 0 -1px!important}.grouped.gapless>:first-child{border-radius:4px 0 0 4px!important;margin:0!important}.grouped.gapless>:last-child{border-radius:0 4px 4px 0!important}input:not([type=checkbox],[type=radio],[type=submit],[type=color],[type=button],[type=reset],:disabled):hover,select:hover,textarea:hover,textarea[type=text]:hover{border-color:var(--color-grey)}input:not([type=checkbox],[type=radio],[type=submit],[type=color],[type=button],[type=reset]):focus,select:focus,textarea:focus,textarea[type=text]:focus{border-color:var(--color-primary);-webkit-box-shadow:0 0 1px var(--color-primary);box-shadow:0 0 1px var(--color-primary);outline:none}input.error:not([type=checkbox],[type=radio],[type=submit],[type=color],[type=button],[type=reset]),textarea.error{border-color:var(--color-error)}input.success:not([type=checkbox],[type=radio],[type=submit],[type=color],[type=button],[type=reset]),textarea.success{border-color:var(--color-success)}[type=checkbox],[type=radio]{height:1.6rem;width:2rem}.button+.button{margin-left:1rem}.button.secondary{background-color:var(--color-grey)}.button.dark{background-color:var(--color-darkGrey)}.button.error{background-color:var(--color-error)}.button.success{background-color:var(--color-success)}.button.outline{background-color:transparent;border-color:var(--color-lightGrey)}.button.outline.primary{border-color:var(--color-primary);color:var(--color-primary)}.button.outline.secondary{border-color:var(--color-grey);color:var(--color-grey)}.button.outline.dark{border-color:var(--color-darkGrey);color:var(--color-darkGrey)}.button.clear{background-color:transparent;border-color:transparent;color:var(--color-primary)}.button.icon{-webkit-box-align:center;-ms-flex-align:center;align-items:center;display:-webkit-inline-box;display:-ms-inline-flexbox;display:inline-flex}.button.icon>img{margin-left:2px}.button.icon-only{padding:1rem}.button:active:not(:disabled),[type=button]:active:not(:disabled),[type=reset]:active:not(:disabled),[type=submit]:active:not(:disabled),button:active:not(:disabled){-webkit-transform:scale(.98);transform:scale(.98)}::-webkit-input-placeholder{color:#bdbfc4}::-moz-placeholder{color:#bdbfc4}:-ms-input-placeholder{color:#bdbfc4}::-ms-input-placeholder{color:#bdbfc4}::placeholder{color:#bdbfc4}.nav{-webkit-box-align:stretch;-ms-flex-align:stretch;align-items:stretch;display:-webkit-box;display:-ms-flexbox;display:flex;min-height:5rem}.nav img{max-height:3rem}.nav-center,.nav-left,.nav-right,.nav>.container{display:-webkit-box;display:-ms-flexbox;display:flex}.nav-center,.nav-left,.nav-right{-webkit-box-flex:1;-ms-flex:1;flex:1}.nav-left{-webkit-box-pack:start;-ms-flex-pack:start;justify-content:flex-start}.nav-right{-webkit-box-pack:end;-ms-flex-pack:end;justify-content:flex-end}.nav-center{-webkit-box-pack:center;-ms-flex-pack:center;justify-content:center}@media screen and (max-width:480px){.nav,.nav>.container{-webkit-box-orient:vertical;-webkit-box-direction:normal;-ms-flex-direction:column;flex-direction:column}.nav-center,.nav-left,.nav-right{-webkit-box-pack:center;-ms-flex-pack:center;-ms-flex-wrap:wrap;flex-wrap:wrap;justify-content:center}}.nav .brand,.nav a{-webkit-box-align:center;-ms-flex-align:center;align-items:center;color:var(--color-darkGrey);display:-webkit-box;display:-ms-flexbox;display:flex;padding:1rem 2rem;text-decoration:none}.nav .active:not(.button),.nav [aria-current=page]:not(.button){color:#000;color:var(--color-primary)}.nav .brand{font-size:1.75em;padding-bottom:0;padding-top:0}.nav .brand img{padding-right:1rem}.nav .button{margin:auto 1rem}.card{background:var(--bg-color);border-radius:4px;-webkit-box-shadow:0 1px 3px var(--color-grey);box-shadow:0 1px 3px var(--color-grey);padding:1rem 2rem}.card p:last-child{margin:0}.card header>*{margin-bottom:1rem;margin-top:0}.tabs{display:-webkit-box;display:-ms-flexbox;display:flex}.tabs a{text-decoration:none}.tabs>.dropdown>summary,.tabs>a{-webkit-box-flex:0;border-bottom:2px solid var(--color-lightGrey);color:var(--color-darkGrey);-ms-flex:0 1 auto;flex:0 1 auto;padding:1rem 2rem;text-align:center}.tabs>a.active,.tabs>a:hover,.tabs>a[aria-current=page]{border-bottom:2px solid var(--color-darkGrey);opacity:1}.tabs>a.active,.tabs>a[aria-current=page]{border-color:var(--color-primary)}.tabs.is-full a{-webkit-box-flex:1;-ms-flex:1 1 auto;flex:1 1 auto}.tag{border:1px solid var(--color-lightGrey);color:var(--color-grey);display:inline-block;letter-spacing:.5px;line-height:1;padding:.5rem;text-transform:uppercase}.tag.is-small{font-size:.75em;padding:.4rem}.tag.is-large{font-size:1.125em;padding:.7rem}.tag+.tag{margin-left:1rem}details.dropdown{display:inline-block;position:relative}details.dropdown>:last-child{left:0;position:absolute;white-space:nowrap}.bg-primary{background-color:var(--color-primary)!important}.bg-light{background-color:var(--color-lightGrey)!important}.bg-dark{background-color:var(--color-darkGrey)!important}.bg-grey{background-color:var(--color-grey)!important}.bg-error{background-color:var(--color-error)!important}.bg-success{background-color:var(--color-success)!important}.bd-primary{border:1px solid var(--color-primary)!important}.bd-light{border:1px solid var(--color-lightGrey)!important}.bd-dark{border:1px solid var(--color-darkGrey)!important}.bd-grey{border:1px solid var(--color-grey)!important}.bd-error{border:1px solid var(--color-error)!important}.bd-success{border:1px solid var(--color-success)!important}.text-primary{color:var(--color-primary)!important}.text-light{color:var(--color-lightGrey)!important}.text-dark{color:var(--color-darkGrey)!important}.text-grey{color:var(--color-grey)!important}.text-error{color:var(--color-error)!important}.text-success{color:var(--color-success)!important}.text-white{color:#fff!important}.pull-right{float:right!important}.pull-left{float:left!important}.text-center{text-align:center}.text-left{text-align:left}.text-right{text-align:right}.text-justify{text-align:justify}.text-uppercase{text-transform:uppercase}.text-lowercase{text-transform:lowercase}.text-capitalize{text-transform:capitalize}.is-full-screen{min-height:100vh;width:100%}.is-full-width{width:100%!important}.is-vertical-align{-webkit-box-align:center;-ms-flex-align:center;align-items:center;display:-webkit-box;display:-ms-flexbox;display:flex}.is-center,.is-horizontal-align{-webkit-box-pack:center;-ms-flex-pack:center;display:-webkit-box;display:-ms-flexbox;display:flex;justify-content:center}.is-center{-webkit-box-align:center;-ms-flex-align:center;align-items:center}.is-right{-webkit-box-pack:end;-ms-flex-pack:end;justify-content:flex-end}.is-left,.is-right{-webkit-box-align:center;-ms-flex-align:center;align-items:center;display:-webkit-box;display:-ms-flexbox;display:flex}.is-left{-webkit-box-pack:start;-ms-flex-pack:start;justify-content:flex-start}.is-fixed{position:fixed;width:100%}.is-paddingless{padding:0!important}.is-marginless{margin:0!important}.is-pointer{cursor:pointer!important}.is-rounded{border-radius:100%}.clearfix{clear:both;content:"";display:table}.is-hidden{display:none!important}@media screen and (max-width:599px){.hide-xs{display:none!important}}@media screen and (min-width:600px) and (max-width:899px){.hide-sm{display:none!important}}@media screen and (min-width:900px) and (max-width:1199px){.hide-md{display:none!important}}@media screen and (min-width:1200px){.hide-lg{display:none!important}}@media print{.hide-pr{display:none!important}} \ No newline at end of file diff --git a/templates/static/style.css b/templates/static/style.css index 1540cac..c280dd9 100644 --- a/templates/static/style.css +++ b/templates/static/style.css @@ -72,3 +72,26 @@ td.group-member { tbody.group:has(.group-toggle:checked) .group-arrow::before { content: "▾ "; } + +/* Round indicator under the page title: either the tag of a released round + or "Round in progress" for the continuously updated site */ +.round-line { + font-size: 0.9em; + margin-top: -0.5rem; + color: var(--color-grey, #747681); +} +.round-line a { + color: var(--color-grey, #747681); +} + +/* Citation box for a released round with a DOI */ +.citation { + background-color: var(--bg-secondary-color, #f3f3f6); + border-left: 4px solid var(--color-primary, #14854f); + padding: 0.6rem 1rem; + margin: 1rem 0; +} +.citation code { + white-space: pre-wrap; + word-break: break-word; +} diff --git a/templates/test.html b/templates/test.html index bf39a47..73d2808 100644 --- a/templates/test.html +++ b/templates/test.html @@ -1,8 +1,6 @@ {% extends "base.html" %} {% from "macros.html" import detail_styles, result_status_cell, perf_cells, perf_header %} -{% block static_path %}{{ root_path }}{% endblock %} - {% block title %}{{ test.name }} - Lean Kernel Arena{% endblock %} {% block h1 %}Lean Kernel Arena / {{ test.name }} From d0b59c503e208209e307210884560bf54b23574c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 27 Aug 2026 12:49:06 +0000 Subject: [PATCH 02/10] Rounds: only deploy from workflow_dispatch, and fix review findings A round tag now only produces the release and the Zenodo deposition. It used to deploy as well, which meant the live site briefly *was* the archived round page, telling visitors at the site root that it is not updated any more. A round becomes visible under /round// with the next dispatch run, which is also the only thing that assembles /round/ at all. That drops the `deploy` output, the second render of the site root, and the distinction between real and test rounds outside of Zenodo. Fixes found in review: - .github/zenodo.py was not executable, so every round build would have died at the first Zenodo step. - A round build that failed after creating the release could not be retried: `gh release create` refuses an existing release, and the cleanup discarded only the Zenodo draft, leaving a release advertising a results.json that points at it. The next round would then try to chain its version onto that discarded deposition and fail too. The release is now replaced on a re-run and removed together with the draft on failure. - A failed DOI reservation no longer blocks building and deploying the site; it just does not close the round. - Two runs deploying at once would race over /round/; all non-pull-request runs now share a concurrency group. - Reserving a DOI required only the checkers to have succeeded, so a failing tutorial or test-stats job still created a draft that was then discarded. The implicit success() over `needs` covers this and is shorter. - Test rounds recorded a `round-*` release URL in their Zenodo metadata; the tag is now passed in rather than reconstructed. - Tag matching is anchored to the validated YYYY-MM shape, so an unrelated release tag starting with `round-` cannot enter the archive. Add the LICENSE, taken verbatim from leanprover/lean4, so that the Apache-2.0 that the Zenodo metadata claims is actually stated somewhere. --- .github/workflows/build-and-deploy.yml | 70 ++++++++++++++----------- .github/zenodo.py | 20 ++++---- LICENSE | 71 ++++++++++++++++++++++++++ README.md | 24 ++++++--- 4 files changed, 138 insertions(+), 47 deletions(-) mode change 100644 => 100755 .github/zenodo.py create mode 100644 LICENSE diff --git a/.github/workflows/build-and-deploy.yml b/.github/workflows/build-and-deploy.yml index f5c1401..62fff17 100644 --- a/.github/workflows/build-and-deploy.yml +++ b/.github/workflows/build-and-deploy.yml @@ -6,9 +6,10 @@ on: push: tags: # Closes a round: builds the site from scratch, publishes it as a release - # and deposits it on Zenodo for a DOI. `test-round-*` does the same - # against sandbox.zenodo.org, so the tag and release can be deleted again - # without leaving traces. + # and deposits it on Zenodo for a DOI. Does not deploy — the round shows + # up under /round// with the next workflow_dispatch. `test-round-*` + # does the same against sandbox.zenodo.org, so the tag and release can be + # deleted again without leaving traces. - 'round-*' - 'test-round-*' @@ -16,7 +17,11 @@ permissions: contents: read concurrency: - group: ${{ github.workflow }}-${{ github.ref }} + # Pull requests get a group each, so they queue and cancel per branch. All + # other runs share one group: two of them deploying or closing a round at the + # same time would race, and they are expensive enough to be worth serializing + # anyway. + group: ${{ github.workflow }}-${{ github.event_name == 'pull_request' && github.ref || 'main' }} cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: @@ -31,8 +36,6 @@ jobs: # 'true' for test rounds, which use sandbox.zenodo.org and are published # as GitHub pre-releases sandbox: ${{ steps.round.outputs.sandbox }} - # Whether this build is deployed to GitHub Pages - deploy: ${{ steps.round.outputs.deploy }} steps: - name: Determine round from the tag id: round @@ -44,7 +47,6 @@ jobs: echo "is_round=false" echo "round=" echo "sandbox=false" - echo "deploy=${{ github.event_name == 'workflow_dispatch' }}" } >> "$GITHUB_OUTPUT" exit 0 fi @@ -59,14 +61,10 @@ jobs: exit 1 fi echo "Closing round $round (sandbox=$sandbox)" - # A test round must not replace the live site; it only exercises the - # release and Zenodo path. - if [ "$sandbox" = true ]; then deploy=false; else deploy=true; fi { echo "is_round=true" echo "round=$round" echo "sandbox=$sandbox" - echo "deploy=$deploy" } >> "$GITHUB_OUTPUT" select-checkers: @@ -271,9 +269,10 @@ jobs: zenodo-reserve: name: Reserve DOI on Zenodo needs: [round-info, check, tutorial, test-stats] - # Only for rounds, and only once the measurements are in: a reserved DOI - # that is never published leaves a draft deposition behind. - if: ${{ !cancelled() && needs.round-info.outputs.is_round == 'true' && needs.check.result == 'success' }} + # Only for rounds, and only once everything the round needs has succeeded: + # a DOI reserved for a build that then fails is a draft deposition to clean + # up. The implicit success() over `needs` covers that. + if: ${{ needs.round-info.outputs.is_round == 'true' }} runs-on: ubuntu-latest permissions: contents: read @@ -299,7 +298,7 @@ jobs: # grep finds nothing before the first round exists, and pipefail # would turn that into a failure previous=$(gh release list --limit 100 --json tagName --jq '.[].tagName' \ - | { grep "^${prefix}[0-9]" || true; } \ + | { grep -E "^${prefix}[0-9]{4}-[0-9]{2}$" || true; } \ | { grep -v "^${GITHUB_REF_NAME}$" || true; } \ | sort -r | head -1) if [ -z "$previous" ]; then @@ -322,7 +321,7 @@ jobs: run: | args=() if [ "$SANDBOX" = true ]; then args+=(--sandbox); fi - args+=(reserve --round "$ROUND") + args+=(reserve --round "$ROUND" --tag "$GITHUB_REF_NAME") if [ -n "$PREVIOUS" ]; then args+=(--previous-deposition "$PREVIOUS"); fi .github/zenodo.py "${args[@]}" env: @@ -334,9 +333,10 @@ jobs: needs: [round-info, check, tutorial, test-stats, zenodo-reserve] # Run even if some checker jobs failed, so the site (including the failures) # is still built and deployed; a final step below then fails this job if any - # checker failed. zenodo-reserve is skipped for non-round builds, which is - # covered by !cancelled(). - if: ${{ !cancelled() && needs.check.result != 'skipped' && needs.zenodo-reserve.result != 'failure' }} + # checker failed. zenodo-reserve is skipped for non-round builds and may + # fail for a round, in which case this still builds and deploys the site, + # just without closing the round (see ROUND_READY). + if: ${{ !cancelled() && needs.check.result != 'skipped' }} runs-on: ubuntu-latest permissions: @@ -368,7 +368,7 @@ jobs: github_access_token: ${{ secrets.GITHUB_TOKEN }} - name: Setup Pages - if: needs.round-info.outputs.deploy == 'true' + if: github.event_name == 'workflow_dispatch' uses: actions/configure-pages@v6 - name: Setup nix shell @@ -441,6 +441,13 @@ jobs: if: env.ROUND_READY == 'true' run: | prefix="lean-arena-round-$ROUND" + # Re-running a round build finds the release an earlier attempt left + # behind; replace it rather than failing, so a round can be retried + # without deleting anything by hand. Deleting a release keeps its tag. + if gh release view "$GITHUB_REF_NAME" >/dev/null 2>&1; then + echo "Replacing the release left behind by an earlier attempt" + gh release delete "$GITHUB_REF_NAME" --yes + fi args=(--title "Round $ROUND" --notes "Round $ROUND of the Lean Kernel Arena.") if [ "$SANDBOX" = true ]; then args+=(--prerelease); fi gh release create "$GITHUB_REF_NAME" "${args[@]}" \ @@ -462,17 +469,17 @@ jobs: BUCKET: ${{ needs.zenodo-reserve.outputs.bucket }} ZENODO_TOKEN: ${{ needs.round-info.outputs.sandbox == 'true' && secrets.ZENODO_SANDBOX_TOKEN || secrets.ZENODO_TOKEN }} - # Assemble the archive of closed rounds under /round/. This runs after the - # release above, so a build that closes a round already includes itself. - # Test rounds are deliberately not listed. - - name: Assemble previous rounds - if: needs.round-info.outputs.deploy == 'true' + # Assemble the archive of closed rounds under /round/, from the release + # assets. Only deploying runs need this, and a round becomes visible on + # the site with the next one. Test rounds are deliberately not listed. + - name: Assemble closed rounds + if: github.event_name == 'workflow_dispatch' run: | mkdir -p _out/round # No match before the first round is closed; pipefail would make that # an error rather than an empty archive tags=$(gh release list --limit 100 --json tagName --jq '.[].tagName' \ - | { grep '^round-[0-9]' || true; }) + | { grep -E '^round-[0-9]{4}-[0-9]{2}$' || true; }) for tag in $tags; do round="${tag#round-}" prefix="lean-arena-round-$round" @@ -513,17 +520,20 @@ jobs: archive: false - name: Deploy to GitHub Pages - if: needs.round-info.outputs.deploy == 'true' + if: github.event_name == 'workflow_dispatch' id: deployment uses: actions/deploy-pages@v5 with: artifact_name: github-pages-${{ github.run_attempt }} - # A draft deposition whose build failed would otherwise linger on Zenodo - # and hold on to a DOI that is never published. - - name: Discard the Zenodo draft on failure + # Leave nothing half-published behind. The draft would otherwise linger + # on Zenodo holding a DOI that is never published, and the release would + # advertise a results.json pointing at that discarded draft — which the + # next round would then try to build its version chain on. + - name: Discard the round on failure if: ${{ failure() && env.ROUND_READY == 'true' && needs.zenodo-reserve.outputs.deposition_id }} run: | + gh release delete "$GITHUB_REF_NAME" --yes || echo "No release to delete" args=() if [ "$SANDBOX" = true ]; then args+=(--sandbox); fi .github/zenodo.py "${args[@]}" discard --deposition "$DEPOSITION" diff --git a/.github/zenodo.py b/.github/zenodo.py old mode 100644 new mode 100755 index 3636635..c3710c9 --- a/.github/zenodo.py +++ b/.github/zenodo.py @@ -10,8 +10,9 @@ upload -> attach the built files to the draft publish -> make the record (and the DOI) public -with `publish` gated behind a manual approval, since publishing is -irreversible. `discard` deletes an unpublished draft again, for failed builds. +Publishing is irreversible, so it runs last, once the release exists and the +site is deployed; `discard` deletes the still unpublished draft again when an +earlier step fails. Rounds after the first are created as new versions of the previous round's deposition (`--previous-deposition`). That gives them a shared concept DOI @@ -77,7 +78,7 @@ def upload_file(bucket_url: str, path: Path, token: str) -> None: print(f"Uploaded {path.name} ({size} bytes)") -def deposition_metadata(round_name: str) -> dict: +def deposition_metadata(round_name: str, tag: str) -> dict: """Build the deposition metadata for a round from .zenodo.json.""" with open(METADATA_FILE, "r") as f: # Keys starting with an underscore are comments for human readers; @@ -89,7 +90,7 @@ def deposition_metadata(round_name: str) -> dict: related = list(metadata.get("related_identifiers", [])) related.append({ "relation": "isSupplementTo", - "identifier": f"{REPO_URL}/releases/tag/round-{round_name}", + "identifier": f"{REPO_URL}/releases/tag/{tag}", "resource_type": "software", }) metadata["related_identifiers"] = related @@ -150,7 +151,7 @@ def cmd_reserve(args: argparse.Namespace, token: str) -> None: "PUT", f"{base}/api/deposit/depositions/{deposition_id}", token, - data={"metadata": deposition_metadata(args.round)}, + data={"metadata": deposition_metadata(args.round, args.tag)}, ) # Setting metadata must not disturb the reservation: the DOI is about to be @@ -165,12 +166,8 @@ def cmd_reserve(args: argparse.Namespace, token: str) -> None: if not bucket: sys.exit(f"Deposition {deposition_id} has no file bucket") - emit_outputs( - doi=doi, - deposition_id=deposition_id, - bucket=bucket, - deposition_url=f"{base}/deposit/{deposition_id}", - ) + print(f"Draft deposition: {base}/deposit/{deposition_id}") + emit_outputs(doi=doi, deposition_id=deposition_id, bucket=bucket) def cmd_upload(args: argparse.Namespace, token: str) -> None: @@ -211,6 +208,7 @@ def main() -> int: reserve = subparsers.add_parser("reserve", help="Create a draft deposition and pre-reserve its DOI") reserve.add_argument("--round", required=True, help="Round name, e.g. 2026-10") + reserve.add_argument("--tag", required=True, help="Tag the round is released under, e.g. round-2026-10") reserve.add_argument( "--previous-deposition", help="Deposition id of the previous round; the new round becomes a new version of it", diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..813da29 --- /dev/null +++ b/LICENSE @@ -0,0 +1,71 @@ +Apache License 2.0 (Apache) +Apache License +Version 2.0, January 2004 +http://www.apache.org/licenses/ + +TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + +1. Definitions. + +"License" shall mean the terms and conditions for use, reproduction, and distribution as defined by Sections 1 through 9 of this document. + +"Licensor" shall mean the copyright owner or entity authorized by the copyright owner that is granting the License. + +"Legal Entity" shall mean the union of the acting entity and all other entities that control, are controlled by, or are under common control with that entity. For the purposes of this definition, "control" means (i) the power, direct or indirect, to cause the direction or management of such entity, whether by contract or otherwise, or (ii) ownership of fifty percent (50%) or more of the outstanding shares, or (iii) beneficial ownership of such entity. + +"You" (or "Your") shall mean an individual or Legal Entity exercising permissions granted by this License. + +"Source" form shall mean the preferred form for making modifications, including but not limited to software source code, documentation source, and configuration files. + +"Object" form shall mean any form resulting from mechanical transformation or translation of a Source form, including but not limited to compiled object code, generated documentation, and conversions to other media types. + +"Work" shall mean the work of authorship, whether in Source or Object form, made available under the License, as indicated by a copyright notice that is included in or attached to the work (an example is provided in the Appendix below). + +"Derivative Works" shall mean any work, whether in Source or Object form, that is based on (or derived from) the Work and for which the editorial revisions, annotations, elaborations, or other modifications represent, as a whole, an original work of authorship. For the purposes of this License, Derivative Works shall not include works that remain separable from, or merely link (or bind by name) to the interfaces of, the Work and Derivative Works thereof. + +"Contribution" shall mean any work of authorship, including the original version of the Work and any modifications or additions to that Work or Derivative Works thereof, that is intentionally submitted to Licensor for inclusion in the Work by the copyright owner or by an individual or Legal Entity authorized to submit on behalf of the copyright owner. For the purposes of this definition, "submitted" means any form of electronic, verbal, or written communication sent to the Licensor or its representatives, including but not limited to communication on electronic mailing lists, source code control systems, and issue tracking systems that are managed by, or on behalf of, the Licensor for the purpose of discussing and improving the Work, but excluding communication that is conspicuously marked or otherwise designated in writing by the copyright owner as "Not a Contribution." + +"Contributor" shall mean Licensor and any individual or Legal Entity on behalf of whom a Contribution has been received by Licensor and subsequently incorporated within the Work. + +2. Grant of Copyright License. + +Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable copyright license to reproduce, prepare Derivative Works of, publicly display, publicly perform, sublicense, and distribute the Work and such Derivative Works in Source or Object form. + +3. Grant of Patent License. + +Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable (except as stated in this section) patent license to make, have made, use, offer to sell, sell, import, and otherwise transfer the Work, where such license applies only to those patent claims licensable by such Contributor that are necessarily infringed by their Contribution(s) alone or by combination of their Contribution(s) with the Work to which such Contribution(s) was submitted. If You institute patent litigation against any entity (including a cross-claim or counterclaim in a lawsuit) alleging that the Work or a Contribution incorporated within the Work constitutes direct or contributory patent infringement, then any patent licenses granted to You under this License for that Work shall terminate as of the date such litigation is filed. + +4. Redistribution. + +You may reproduce and distribute copies of the Work or Derivative Works thereof in any medium, with or without modifications, and in Source or Object form, provided that You meet the following conditions: + +1. You must give any other recipients of the Work or Derivative Works a copy of this License; and + +2. You must cause any modified files to carry prominent notices stating that You changed the files; and + +3. You must retain, in the Source form of any Derivative Works that You distribute, all copyright, patent, trademark, and attribution notices from the Source form of the Work, excluding those notices that do not pertain to any part of the Derivative Works; and + +4. If the Work includes a "NOTICE" text file as part of its distribution, then any Derivative Works that You distribute must include a readable copy of the attribution notices contained within such NOTICE file, excluding those notices that do not pertain to any part of the Derivative Works, in at least one of the following places: within a NOTICE text file distributed as part of the Derivative Works; within the Source form or documentation, if provided along with the Derivative Works; or, within a display generated by the Derivative Works, if and wherever such third-party notices normally appear. The contents of the NOTICE file are for informational purposes only and do not modify the License. You may add Your own attribution notices within Derivative Works that You distribute, alongside or as an addendum to the NOTICE text from the Work, provided that such additional attribution notices cannot be construed as modifying the License. + +You may add Your own copyright statement to Your modifications and may provide additional or different license terms and conditions for use, reproduction, or distribution of Your modifications, or for any such Derivative Works as a whole, provided Your use, reproduction, and distribution of the Work otherwise complies with the conditions stated in this License. + +5. Submission of Contributions. + +Unless You explicitly state otherwise, any Contribution intentionally submitted for inclusion in the Work by You to the Licensor shall be under the terms and conditions of this License, without any additional terms or conditions. Notwithstanding the above, nothing herein shall supersede or modify the terms of any separate license agreement you may have executed with Licensor regarding such Contributions. + +6. Trademarks. + +This License does not grant permission to use the trade names, trademarks, service marks, or product names of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and reproducing the content of the NOTICE file. + +7. Disclaimer of Warranty. + +Unless required by applicable law or agreed to in writing, Licensor provides the Work (and each Contributor provides its Contributions) on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied, including, without limitation, any warranties or conditions of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A PARTICULAR PURPOSE. You are solely responsible for determining the appropriateness of using or redistributing the Work and assume any risks associated with Your exercise of permissions under this License. + +8. Limitation of Liability. + +In no event and under no legal theory, whether in tort (including negligence), contract, or otherwise, unless required by applicable law (such as deliberate and grossly negligent acts) or agreed to in writing, shall any Contributor be liable to You for damages, including any direct, indirect, special, incidental, or consequential damages of any character arising as a result of this License or out of the use or inability to use the Work (including but not limited to damages for loss of goodwill, work stoppage, computer failure or malfunction, or any and all other commercial damages or losses), even if such Contributor has been advised of the possibility of such damages. + +9. Accepting Warranty or Additional Liability. + +While redistributing the Work or Derivative Works thereof, You may choose to offer, and charge a fee for, acceptance of support, warranty, indemnity, or other liability obligations and/or rights consistent with this License. However, in accepting such obligations, You may act only on Your own behalf and on Your sole responsibility, not on behalf of any other Contributor, and only if You agree to indemnify, defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against, such Contributor by reason of your accepting any such warranty or additional liability. + diff --git a/README.md b/README.md index 6323c56..933cba7 100644 --- a/README.md +++ b/README.md @@ -230,12 +230,22 @@ This runs the full CI build (no tests are skipped), and then: the raw results as `lean-arena-round-2026-10-results.json`, and the test suite as `lean-arena-round-2026-10-tests.tar.gz`, 4. uploads those to Zenodo as a draft deposition, -5. reassembles `/round/` from all round releases and deploys the site, -6. publishes the Zenodo record, which mints the DOI. +5. publishes the Zenodo record, which mints the DOI. + +A round build does not touch the live site. The round appears under +`/round/2026-10/`, and the round index gains a row, with the next +`workflow_dispatch` run, which assembles `/round/` from the release assets. +So closing a round is: push the tag, wait for it to go green, then dispatch a +run of the same workflow. Publishing cannot be undone, so it happens last, once everything else has -succeeded. If an earlier step fails, the draft deposition is discarded again -and no DOI is minted. +succeeded. If an earlier step fails, both the draft deposition and the release +are removed again and no DOI is minted, so the tag can simply be pushed again. + +If only the last step fails, the release exists but the DOI does not resolve +yet. Re-run the `Publish DOI on Zenodo` job; do not close another round before +it has succeeded, since the next round is built as a new version of this one's +deposition. Each round is deposited as a new version of the previous one, so all rounds share a concept DOI that resolves to the most recent round, next to their @@ -245,8 +255,10 @@ each round's own `results.json`. ### Trying it out A tag `test-round-` runs exactly the same thing, but against -[sandbox.zenodo.org](https://sandbox.zenodo.org) and without deploying the -site. Delete the tag and the GitHub release afterwards and nothing remains. +[sandbox.zenodo.org](https://sandbox.zenodo.org), and its release is marked as +a pre-release. Delete the tag and the GitHub release afterwards and nothing +remains; `/round/` only ever lists `round-*`, so a test round never shows up on +the site even if its release is left in place. The tag does not have to be on `master`, so a change to the round machinery can be exercised end to end while it is still a pull request. From ee797b14a7dd1d81da5feb03dc74ac0d23ebf069 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 27 Aug 2026 13:00:12 +0000 Subject: [PATCH 03/10] Refuse to close a round that already has a release MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replacing an existing release on a re-run, added in the previous commit, was the wrong cure: the step cannot tell a release left behind by a failed attempt from the release of a round that closed successfully. A single "Re-run all jobs" on a green round build would have deleted the published round's release, recreated it pointing at a fresh deposition, and minted a second DOI for the same round, while the first DOI kept resolving to the old content. Refuse instead, and do it in round-info, before the hours of building: a failed attempt removes its own release, so one still being there means the round is closed or a run died mid-flight, and both want a human. Recovering from the latter is one `gh release delete` away, which the error message says. Also discard the round when a run is cancelled, not just when it fails — cancelling between creating the release and publishing leaves exactly the half-published state the cleanup exists to prevent. Fix comments that still said a round tag deploys the site, correct the README on how to retry (pushing an existing tag does nothing; "Re-run failed jobs" reuses the discarded deposition, so it has to be "Re-run all jobs"), and raise the release listing cap, which the archive and the version chain both scan. --- .github/workflows/build-and-deploy.yml | 40 +++++++++++++++++--------- .github/zenodo.py | 6 ++-- README.md | 12 ++++++-- 3 files changed, 39 insertions(+), 19 deletions(-) diff --git a/.github/workflows/build-and-deploy.yml b/.github/workflows/build-and-deploy.yml index 62fff17..0fb14c0 100644 --- a/.github/workflows/build-and-deploy.yml +++ b/.github/workflows/build-and-deploy.yml @@ -36,6 +36,10 @@ jobs: # 'true' for test rounds, which use sandbox.zenodo.org and are published # as GitHub pre-releases sandbox: ${{ steps.round.outputs.sandbox }} + env: + GH_TOKEN: ${{ github.token }} + # This job has no checkout, so gh cannot infer the repository + GH_REPO: ${{ github.repository }} steps: - name: Determine round from the tag id: round @@ -60,6 +64,15 @@ jobs: echo "::error::Round name '$round' (from tag $tag) is not of the form YYYY-MM" exit 1 fi + # Refuse to close a round that already has a release, before spending + # hours on the build. A failed attempt deletes its own release again, + # so one still being here means either the round was closed + # successfully — re-running that would mint a second DOI for it — or + # a run died without getting to clean up, which wants a look anyway. + if gh release view "$tag" >/dev/null 2>&1; then + echo "::error::A release for $tag already exists. If round $round was closed successfully, do not re-run this build: it would create a second Zenodo record and DOI for the same round. If it is left over from a run that failed to clean up, delete it with 'gh release delete $tag' and start the build again." + exit 1 + fi echo "Closing round $round (sandbox=$sandbox)" { echo "is_round=true" @@ -297,7 +310,7 @@ jobs: if [ "$SANDBOX" = true ]; then prefix=test-round-; else prefix=round-; fi # grep finds nothing before the first round exists, and pipefail # would turn that into a failure - previous=$(gh release list --limit 100 --json tagName --jq '.[].tagName' \ + previous=$(gh release list --limit 1000 --json tagName --jq '.[].tagName' \ | { grep -E "^${prefix}[0-9]{4}-[0-9]{2}$" || true; } \ | { grep -v "^${GITHUB_REF_NAME}$" || true; } \ | sort -r | head -1) @@ -334,8 +347,8 @@ jobs: # Run even if some checker jobs failed, so the site (including the failures) # is still built and deployed; a final step below then fails this job if any # checker failed. zenodo-reserve is skipped for non-round builds and may - # fail for a round, in which case this still builds and deploys the site, - # just without closing the round (see ROUND_READY). + # fail for a round, in which case this still builds the site, just without + # closing the round (see ROUND_READY). if: ${{ !cancelled() && needs.check.result != 'skipped' }} runs-on: ubuntu-latest @@ -348,8 +361,8 @@ jobs: GH_TOKEN: ${{ github.token }} # A round is only stamped into the site, released and deposited once its # DOI has been reserved, which in turn requires every checker to have - # succeeded. A round build with a failing checker still builds and - # deploys the site (and fails at the end), but publishes nothing. + # succeeded. A round build with a failing checker still builds the site + # (and fails at the end), but publishes nothing. ROUND_READY: ${{ needs.round-info.outputs.is_round == 'true' && needs.zenodo-reserve.result == 'success' }} ROUND: ${{ needs.round-info.outputs.round }} SANDBOX: ${{ needs.round-info.outputs.sandbox }} @@ -441,13 +454,10 @@ jobs: if: env.ROUND_READY == 'true' run: | prefix="lean-arena-round-$ROUND" - # Re-running a round build finds the release an earlier attempt left - # behind; replace it rather than failing, so a round can be retried - # without deleting anything by hand. Deleting a release keeps its tag. - if gh release view "$GITHUB_REF_NAME" >/dev/null 2>&1; then - echo "Replacing the release left behind by an earlier attempt" - gh release delete "$GITHUB_REF_NAME" --yes - fi + # An existing release is refused by round-info, not replaced here: a + # release that survived a failed attempt is indistinguishable from + # the release of a round that closed successfully, and silently + # replacing the latter would mint a second DOI for the same round. args=(--title "Round $ROUND" --notes "Round $ROUND of the Lean Kernel Arena.") if [ "$SANDBOX" = true ]; then args+=(--prerelease); fi gh release create "$GITHUB_REF_NAME" "${args[@]}" \ @@ -478,7 +488,7 @@ jobs: mkdir -p _out/round # No match before the first round is closed; pipefail would make that # an error rather than an empty archive - tags=$(gh release list --limit 100 --json tagName --jq '.[].tagName' \ + tags=$(gh release list --limit 1000 --json tagName --jq '.[].tagName' \ | { grep -E '^round-[0-9]{4}-[0-9]{2}$' || true; }) for tag in $tags; do round="${tag#round-}" @@ -530,8 +540,10 @@ jobs: # on Zenodo holding a DOI that is never published, and the release would # advertise a results.json pointing at that discarded draft — which the # next round would then try to build its version chain on. + # Cancellation counts: a run stopped between creating the release and + # publishing leaves exactly the half-published state this prevents. - name: Discard the round on failure - if: ${{ failure() && env.ROUND_READY == 'true' && needs.zenodo-reserve.outputs.deposition_id }} + if: ${{ (failure() || cancelled()) && env.ROUND_READY == 'true' && needs.zenodo-reserve.outputs.deposition_id }} run: | gh release delete "$GITHUB_REF_NAME" --yes || echo "No release to delete" args=() diff --git a/.github/zenodo.py b/.github/zenodo.py index c3710c9..685387b 100755 --- a/.github/zenodo.py +++ b/.github/zenodo.py @@ -10,9 +10,9 @@ upload -> attach the built files to the draft publish -> make the record (and the DOI) public -Publishing is irreversible, so it runs last, once the release exists and the -site is deployed; `discard` deletes the still unpublished draft again when an -earlier step fails. +Publishing is irreversible, so it runs last, once the release exists and all +its assets are uploaded; `discard` deletes the still unpublished draft again +when an earlier step fails. Rounds after the first are created as new versions of the previous round's deposition (`--previous-deposition`). That gives them a shared concept DOI diff --git a/README.md b/README.md index 933cba7..90a8ca1 100644 --- a/README.md +++ b/README.md @@ -239,14 +239,22 @@ So closing a round is: push the tag, wait for it to go green, then dispatch a run of the same workflow. Publishing cannot be undone, so it happens last, once everything else has -succeeded. If an earlier step fails, both the draft deposition and the release -are removed again and no DOI is minted, so the tag can simply be pushed again. +succeeded. If an earlier step fails or the run is cancelled, both the draft +deposition and the release are removed again and no DOI is minted. Retry with +*Re-run all jobs* in the Actions UI — pushing the tag again does nothing, since +the remote already has it. *Re-run failed jobs* does not work here: it reuses +the discarded deposition and fails at the upload. If only the last step fails, the release exists but the DOI does not resolve yet. Re-run the `Publish DOI on Zenodo` job; do not close another round before it has succeeded, since the next round is built as a new version of this one's deposition. +A round that closed successfully cannot be built again: the build refuses to +start while a release for its tag exists, because a second run would mint a +second DOI for the same round. Should a run ever die without cleaning up after +itself, delete the release by hand and start the build again. + Each round is deposited as a new version of the previous one, so all rounds share a concept DOI that resolves to the most recent round, next to their individual per-round DOIs. The deposition id needed for this is recorded in From cb40b65719575f9ba9b09771d13bc595d5c554b4 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 27 Aug 2026 13:02:48 +0000 Subject: [PATCH 04/10] Stop the pipeline when the round tag is rejected round-info refusing a tag only turned that one job red; select-checkers and the checker matrix have no dependency on it, so an accidental re-run of a closed round still burned the full multi-hour build beside the error before build-site declined to do anything with it. Gate the three entry-point jobs on round-info. A rejected tag now skips check, which skips build-site through its existing 'check was not skipped' condition, and with it the release, Zenodo and deploy steps. --- .github/workflows/build-and-deploy.yml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.github/workflows/build-and-deploy.yml b/.github/workflows/build-and-deploy.yml index 0fb14c0..eadc219 100644 --- a/.github/workflows/build-and-deploy.yml +++ b/.github/workflows/build-and-deploy.yml @@ -82,6 +82,9 @@ jobs: select-checkers: name: Select checkers + # Nothing runs until the tag has been accepted, so a rejected round + # tag costs half a minute rather than a full build + needs: round-info runs-on: ubuntu-latest outputs: checkers: ${{ steps.select.outputs.checkers }} @@ -200,6 +203,9 @@ jobs: tutorial: name: Build tutorial page + # Nothing runs until the tag has been accepted, so a rejected round + # tag costs half a minute rather than a full build + needs: round-info runs-on: ubuntu-latest steps: - name: Checkout repository @@ -237,6 +243,9 @@ jobs: test-stats: name: Build test stats and tarball + # Nothing runs until the tag has been accepted, so a rejected round + # tag costs half a minute rather than a full build + needs: round-info runs-on: ubuntu-latest steps: - name: Checkout repository From 8a08f2ad5d10aecc50abb5df8087540667d62844 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 27 Aug 2026 14:47:36 +0000 Subject: [PATCH 05/10] Record the actual release tag in a round's results.json The release_url was reconstructed as round-, so a test round released under test-round- advertised a release that does not exist. Found in the first sandbox rehearsal: the published results.json pointed at releases/tag/round-2026-08 while the release was test-round-2026-08. Pass the tag in, as zenodo.py already does for the same reason, and keep the reconstruction as the default for building a round site outside CI. --- .github/workflows/build-and-deploy.yml | 2 +- lka.py | 10 +++++++++- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build-and-deploy.yml b/.github/workflows/build-and-deploy.yml index eadc219..80af0a7 100644 --- a/.github/workflows/build-and-deploy.yml +++ b/.github/workflows/build-and-deploy.yml @@ -429,7 +429,7 @@ jobs: run: | args=(--tarball _tarball/lean-arena-tests.tar.gz) if [ "$ROUND_READY" = true ]; then - args+=(--round "$ROUND" --doi "$DOI" --zenodo-deposition "$DEPOSITION") + args+=(--round "$ROUND" --tag "$GITHUB_REF_NAME" --doi "$DOI" --zenodo-deposition "$DEPOSITION") fi ./lka.py build-site "${args[@]}" shell: 'nix develop -c bash -euxo pipefail {0}' diff --git a/lka.py b/lka.py index da63d58..18b66ea 100755 --- a/lka.py +++ b/lka.py @@ -2007,7 +2007,11 @@ def cmd_build_site(args: argparse.Namespace) -> int: if args.zenodo_deposition: meta["zenodo_deposition"] = int(args.zenodo_deposition) if meta["round"]: - meta["release_url"] = f"{REPO_URL}/releases/tag/{ROUND_TAG_PREFIX}{meta['round']}" + # The tag is passed in rather than derived: a test round is released + # under test-round-, so reconstructing it from the round name + # would point at a release that does not exist. + tag = args.tag or f"{ROUND_TAG_PREFIX}{meta['round']}" + meta["release_url"] = f"{REPO_URL}/releases/tag/{tag}" # Publish the raw data alongside the site results_json_file = output_dir / "results.json" @@ -2495,6 +2499,10 @@ def main() -> int: metavar="NAME", help="Name of the round this build closes, e.g. 2026-10 (default: no round, i.e. the ongoing round)", ) + build_site_parser.add_argument( + "--tag", + help=f"Tag this round is released under (default: {ROUND_TAG_PREFIX})", + ) build_site_parser.add_argument( "--doi", help="DOI of this round, shown for citation (pre-reserved on Zenodo before the build)", From 973d13a3f8e5c7fcbdc0cfb5a7e7dc3b234e795b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 27 Aug 2026 15:39:46 +0000 Subject: [PATCH 06/10] Point the release and the Zenodo record at the round on the site Both advertised the GitHub release, which is where the bytes happen to live rather than where a reader wants to end up. The release notes now link to arena.lean-lang.org/round//, and the Zenodo record relates the deposit to that address as isIdenticalTo instead of naming the release. zenodo.py no longer needs to know how a round is tagged or where the repository is, so --tag and REPO_URL go away again; the address is passed in, from a single definition at the top of the workflow that mirrors ROUNDS_URL in lka.py. --- .github/workflows/build-and-deploy.yml | 13 +++++++++++-- .github/zenodo.py | 17 +++++++++-------- 2 files changed, 20 insertions(+), 10 deletions(-) diff --git a/.github/workflows/build-and-deploy.yml b/.github/workflows/build-and-deploy.yml index 80af0a7..e829971 100644 --- a/.github/workflows/build-and-deploy.yml +++ b/.github/workflows/build-and-deploy.yml @@ -16,6 +16,12 @@ on: permissions: contents: read +env: + # Where a closed round ends up on the published site. Mirrors ROUNDS_URL in + # lka.py; this is the address a round is advertised and cited under, rather + # than the release it happens to be distributed from. + ARENA_ROUNDS_URL: https://arena.lean-lang.org/round + concurrency: # Pull requests get a group each, so they queue and cancel per branch. All # other runs share one group: two of them deploying or closing a round at the @@ -343,7 +349,7 @@ jobs: run: | args=() if [ "$SANDBOX" = true ]; then args+=(--sandbox); fi - args+=(reserve --round "$ROUND" --tag "$GITHUB_REF_NAME") + args+=(reserve --round "$ROUND" --url "$ARENA_ROUNDS_URL/$ROUND/") if [ -n "$PREVIOUS" ]; then args+=(--previous-deposition "$PREVIOUS"); fi .github/zenodo.py "${args[@]}" env: @@ -467,7 +473,10 @@ jobs: # release that survived a failed attempt is indistinguishable from # the release of a round that closed successfully, and silently # replacing the latter would mint a second DOI for the same round. - args=(--title "Round $ROUND" --notes "Round $ROUND of the Lean Kernel Arena.") + # Send readers to the round on the site rather than leaving them with + # three tarballs; the assets stay here for downloading and archiving. + notes="Round $ROUND of the Lean Kernel Arena: $ARENA_ROUNDS_URL/$ROUND/" + args=(--title "Round $ROUND" --notes "$notes") if [ "$SANDBOX" = true ]; then args+=(--prerelease); fi gh release create "$GITHUB_REF_NAME" "${args[@]}" \ "/tmp/round/$prefix-site.tar.gz" \ diff --git a/.github/zenodo.py b/.github/zenodo.py index 685387b..22dfcfd 100755 --- a/.github/zenodo.py +++ b/.github/zenodo.py @@ -35,8 +35,6 @@ # so that it can be reviewed and changed without touching this script. METADATA_FILE = Path(__file__).resolve().parent.parent / ".zenodo.json" -REPO_URL = "https://github.com/leanprover/lean-kernel-arena" - def api_base(sandbox: bool) -> str: return "https://sandbox.zenodo.org" if sandbox else "https://zenodo.org" @@ -78,7 +76,7 @@ def upload_file(bucket_url: str, path: Path, token: str) -> None: print(f"Uploaded {path.name} ({size} bytes)") -def deposition_metadata(round_name: str, tag: str) -> dict: +def deposition_metadata(round_name: str, url: str) -> dict: """Build the deposition metadata for a round from .zenodo.json.""" with open(METADATA_FILE, "r") as f: # Keys starting with an underscore are comments for human readers; @@ -88,10 +86,13 @@ def deposition_metadata(round_name: str, tag: str) -> dict: metadata["version"] = round_name metadata["publication_date"] = datetime.date.today().isoformat() related = list(metadata.get("related_identifiers", [])) + # The same round, served on the web. Point at that rather than at the + # GitHub release it is distributed from: the release is where the bytes + # happen to live, the round page is what a reader wants to be sent to. related.append({ - "relation": "isSupplementTo", - "identifier": f"{REPO_URL}/releases/tag/{tag}", - "resource_type": "software", + "relation": "isIdenticalTo", + "identifier": url, + "resource_type": "dataset", }) metadata["related_identifiers"] = related return metadata @@ -151,7 +152,7 @@ def cmd_reserve(args: argparse.Namespace, token: str) -> None: "PUT", f"{base}/api/deposit/depositions/{deposition_id}", token, - data={"metadata": deposition_metadata(args.round, args.tag)}, + data={"metadata": deposition_metadata(args.round, args.url)}, ) # Setting metadata must not disturb the reservation: the DOI is about to be @@ -208,7 +209,7 @@ def main() -> int: reserve = subparsers.add_parser("reserve", help="Create a draft deposition and pre-reserve its DOI") reserve.add_argument("--round", required=True, help="Round name, e.g. 2026-10") - reserve.add_argument("--tag", required=True, help="Tag the round is released under, e.g. round-2026-10") + reserve.add_argument("--url", required=True, help="Canonical address of the round on the site, e.g. https://arena.lean-lang.org/round/2026-10/") reserve.add_argument( "--previous-deposition", help="Deposition id of the previous round; the new round becomes a new version of it", From b4ad749a7d31a000b61074cf4f337a02e1b27737 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 27 Aug 2026 17:43:55 +0000 Subject: [PATCH 07/10] Check that the published DOI is the one baked into the round MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The round's pages and its results.json cite the DOI that reserve pre-reserved, and they are frozen into the release before publication. Nothing checked that publication then hands out that same DOI, which is the assumption the whole arrangement rests on. The sandbox rehearsal showed it can differ: round 2026-08 was built citing 10.5281/zenodo.593158 and its record was published as 10.5072/zenodo.593158 — the sandbox pre-reserves under the production prefix and publishes under its own. That is a sandbox artifact and production should be consistent, but it is exactly the failure this cannot afford to have silently. Fail publication on a mismatch, and reduce it to a warning on sandbox, where it is expected and the DOIs are meaningless anyway. --- .github/workflows/build-and-deploy.yml | 3 ++- .github/zenodo.py | 19 +++++++++++++++++++ README.md | 8 +++++++- 3 files changed, 28 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build-and-deploy.yml b/.github/workflows/build-and-deploy.yml index e829971..cf99bc0 100644 --- a/.github/workflows/build-and-deploy.yml +++ b/.github/workflows/build-and-deploy.yml @@ -599,8 +599,9 @@ jobs: run: | args=() if [ "$SANDBOX" = true ]; then args+=(--sandbox); fi - .github/zenodo.py "${args[@]}" publish --deposition "$DEPOSITION" + .github/zenodo.py "${args[@]}" publish --deposition "$DEPOSITION" --expect-doi "$DOI" env: SANDBOX: ${{ needs.round-info.outputs.sandbox }} DEPOSITION: ${{ needs.zenodo-reserve.outputs.deposition_id }} + DOI: ${{ needs.zenodo-reserve.outputs.doi }} ZENODO_TOKEN: ${{ needs.round-info.outputs.sandbox == 'true' && secrets.ZENODO_SANDBOX_TOKEN || secrets.ZENODO_TOKEN }} diff --git a/.github/zenodo.py b/.github/zenodo.py index 22dfcfd..0004b44 100755 --- a/.github/zenodo.py +++ b/.github/zenodo.py @@ -188,6 +188,24 @@ def cmd_publish(args: argparse.Namespace, token: str) -> None: ) doi = result.get("doi") print(f"Published {result.get('links', {}).get('record_html')} as {doi}") + + # The whole round is built around the pre-reserved DOI, which is printed on + # its pages and recorded in its results.json. If publication hands out a + # different one, the round cites a DOI that is not its own, and the pages + # are already frozen in the release: say so loudly rather than let it pass. + if args.expect_doi and doi != args.expect_doi: + message = ( + f"Published DOI {doi} differs from the pre-reserved {args.expect_doi} " + f"that is baked into round's pages and results.json" + ) + if args.sandbox: + # Sandbox pre-reserves under the production prefix (10.5281) but + # publishes under its own (10.5072), so test rounds always show + # this and their DOIs are meaningless anyway. + print(f"Warning: {message}. This is expected on sandbox.") + else: + sys.exit(message) + emit_outputs(doi=doi, concept_doi=result.get("conceptdoi", "")) @@ -221,6 +239,7 @@ def main() -> int: publish = subparsers.add_parser("publish", help="Publish a draft deposition (irreversible)") publish.add_argument("--deposition", required=True, help="Deposition id reported by reserve") + publish.add_argument("--expect-doi", help="DOI reserve handed out; publishing a different one is an error") discard = subparsers.add_parser("discard", help="Delete an unpublished draft deposition") discard.add_argument("--deposition", required=True, help="Deposition id reported by reserve") diff --git a/README.md b/README.md index 90a8ca1..aeaa7cf 100644 --- a/README.md +++ b/README.md @@ -264,7 +264,13 @@ each round's own `results.json`. A tag `test-round-` runs exactly the same thing, but against [sandbox.zenodo.org](https://sandbox.zenodo.org), and its release is marked as -a pre-release. Delete the tag and the GitHub release afterwards and nothing +a pre-release. Do not read anything into the DOI of a test round: the sandbox +pre-reserves DOIs under the production prefix (`10.5281`) and then publishes +them under its own (`10.5072`), so the DOI printed on a test round's pages is +not the DOI its sandbox record ends up with, and it resolves to whatever +unrelated record happens to have that id on the real Zenodo. The build says so +in the `Publish DOI on Zenodo` job; for a real round the same mismatch is an +error, since the pages that cite the DOI are frozen by then. Delete the tag and the GitHub release afterwards and nothing remains; `/round/` only ever lists `round-*`, so a test round never shows up on the site even if its release is left in place. The tag does not have to be on `master`, so a change to the round machinery From 40eae9cbab5a6ad7bf84eb15c6254eda4f5da06f Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 27 Aug 2026 21:15:36 +0000 Subject: [PATCH 08/10] Add analytics to the deployed pages only, not to the built site MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The snippet went into base.html, so it ended up in every page the site is made of — including the ones packed into a round tarball, deposited on Zenodo and cited by DOI. Whoever opens that copy years from now should not have their browser call a third party, and an archived round is supposed to be a frozen artifact rather than something that keeps phoning home. Move it out of the template and into the deployed copy, inserted before in every page as the last step before the pages are handed to GitHub Pages. The self-contained report is now generated before that step, so it stays clean too, and tag builds never reach it at all. --- .github/add-analytics.py | 46 ++++++++++++++++++++++++++ .github/workflows/build-and-deploy.yml | 30 +++++++++++------ templates/analytics.html | 5 +++ templates/base.html | 9 +++-- 4 files changed, 75 insertions(+), 15 deletions(-) create mode 100755 .github/add-analytics.py create mode 100644 templates/analytics.html diff --git a/.github/add-analytics.py b/.github/add-analytics.py new file mode 100755 index 0000000..e477913 --- /dev/null +++ b/.github/add-analytics.py @@ -0,0 +1,46 @@ +#!/usr/bin/env python3 +"""Insert the analytics snippet into the pages that are about to be deployed. + +This is deliberately not part of the templates. A round is archived as a +tarball, deposited on Zenodo and cited by DOI, and whoever opens that copy in +ten years should not have their browser call out to a third party. So the +built site stays clean, and the snippet is added to the deployed pages only, +as the last thing before they are handed to GitHub Pages. + +Usage: add-analytics.py +""" + +import sys +from pathlib import Path + + +def main(argv: list[str]) -> int: + if len(argv) != 3: + sys.exit(__doc__) + snippet = Path(argv[1]).read_text() + root = Path(argv[2]) + if not root.is_dir(): + sys.exit(f"Not a directory: {root}") + + inserted, skipped = 0, [] + for html in sorted(root.rglob("*.html")): + text = html.read_text(errors="surrogateescape") + if "" not in text: + # Not a full page; nothing to do, but say so rather than silently + # leaving a deployed page untracked. + skipped.append(html.relative_to(root)) + continue + html.write_text(text.replace("", snippet + "", 1), + errors="surrogateescape") + inserted += 1 + + print(f"Inserted {argv[1]} into {inserted} HTML files below {root}") + for path in skipped: + print(f" no , left alone: {path}") + if not inserted: + sys.exit(f"No HTML files with a found below {root}") + return 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv)) diff --git a/.github/workflows/build-and-deploy.yml b/.github/workflows/build-and-deploy.yml index cf99bc0..2f39a78 100644 --- a/.github/workflows/build-and-deploy.yml +++ b/.github/workflows/build-and-deploy.yml @@ -526,16 +526,8 @@ jobs: ./lka.py build-rounds-index --outdir _out/round shell: 'nix develop -c bash -euxo pipefail {0}' - # Give each run attempt its own artifact name. Re-running only this job - # leaves the previous attempt's artifact in place; a fixed name would then - # collide and deploy-pages aborts with "Multiple artifacts named - # github-pages". A per-attempt name makes restarts collision-free. - - name: Upload artifact - uses: actions/upload-pages-artifact@v5 - with: - name: github-pages-${{ github.run_attempt }} - path: '_out' - + # Taken before the analytics snippet goes in, so the standalone report is + # as free of it as the round tarballs are. - name: Generate self-contained report run: monolith _out/index.html -o /tmp/report.html -i -F -e -M -q shell: 'nix develop -c bash -euxo pipefail {0}' @@ -547,6 +539,24 @@ jobs: path: '/tmp/report.html' archive: false + # Last thing before the pages leave the runner, so that only the deployed + # copy carries it: not the round tarballs, not the Zenodo deposits, not + # the report above. + - name: Add analytics to the deployed pages + if: github.event_name == 'workflow_dispatch' + run: .github/add-analytics.py templates/analytics.html _out + shell: 'nix develop -c bash -euxo pipefail {0}' + + # Give each run attempt its own artifact name. Re-running only this job + # leaves the previous attempt's artifact in place; a fixed name would then + # collide and deploy-pages aborts with "Multiple artifacts named + # github-pages". A per-attempt name makes restarts collision-free. + - name: Upload artifact + uses: actions/upload-pages-artifact@v5 + with: + name: github-pages-${{ github.run_attempt }} + path: '_out' + - name: Deploy to GitHub Pages if: github.event_name == 'workflow_dispatch' id: deployment diff --git a/templates/analytics.html b/templates/analytics.html new file mode 100644 index 0000000..7096d0f --- /dev/null +++ b/templates/analytics.html @@ -0,0 +1,5 @@ + + diff --git a/templates/base.html b/templates/base.html index 08d5474..3e84b3c 100644 --- a/templates/base.html +++ b/templates/base.html @@ -8,11 +8,10 @@ frozen artifacts that must still render years from now. #} - - + {# The analytics snippet is deliberately not here; it is injected into the + deployed pages only, see .github/add-analytics.py. A round is archived + and cited as a frozen artifact, and must not carry a script that calls + out to a third party for as long as anyone keeps a copy of it. #} From 9771d118f63fc2721a92074377f1864284270b9a Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 27 Aug 2026 23:23:36 +0000 Subject: [PATCH 09/10] Fix a slipped article in the DOI mismatch message --- .github/zenodo.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/zenodo.py b/.github/zenodo.py index 0004b44..4ea51ac 100755 --- a/.github/zenodo.py +++ b/.github/zenodo.py @@ -196,7 +196,7 @@ def cmd_publish(args: argparse.Namespace, token: str) -> None: if args.expect_doi and doi != args.expect_doi: message = ( f"Published DOI {doi} differs from the pre-reserved {args.expect_doi} " - f"that is baked into round's pages and results.json" + f"that is baked into the round's pages and results.json" ) if args.sandbox: # Sandbox pre-reserves under the production prefix (10.5281) but From 958f6c43341c4e5119ca7b96e31f674a99607b19 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 28 Aug 2026 07:55:11 +0000 Subject: [PATCH 10/10] Expect the sandbox DOI prefix swap rather than waiving the check Zenodo does not store a reserved DOI: its legacy serializer synthesizes prereserve_doi on every response with a hardcoded 10.5281 prefix, while the DOI is minted from the instance's configured DATACITE_PREFIX over the same record id. On production those coincide and the two are equal by construction; sandbox mints under DataCite's test prefix, so only there do they differ, and only in the prefix. The check waived any mismatch on sandbox, which exempted the one environment where it can actually be rehearsed. Expect exactly the prefix swap instead, so a changed record id or an unswapped prefix still fails a test round. --- .github/zenodo.py | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/.github/zenodo.py b/.github/zenodo.py index 4ea51ac..e0b3c02 100755 --- a/.github/zenodo.py +++ b/.github/zenodo.py @@ -35,6 +35,11 @@ # so that it can be reviewed and changed without touching this script. METADATA_FILE = Path(__file__).resolve().parent.parent / ".zenodo.json" +# Zenodo mints DOIs as /zenodo.. Sandbox uses DataCite's +# test prefix, which is why a test round's DOI is not a real one. +PRODUCTION_DOI_PREFIX = "10.5281" +SANDBOX_DOI_PREFIX = "10.5072" + def api_base(sandbox: bool) -> str: return "https://sandbox.zenodo.org" if sandbox else "https://zenodo.org" @@ -193,18 +198,21 @@ def cmd_publish(args: argparse.Namespace, token: str) -> None: # its pages and recorded in its results.json. If publication hands out a # different one, the round cites a DOI that is not its own, and the pages # are already frozen in the release: say so loudly rather than let it pass. - if args.expect_doi and doi != args.expect_doi: - message = ( - f"Published DOI {doi} differs from the pre-reserved {args.expect_doi} " - f"that is baked into the round's pages and results.json" + expected = args.expect_doi + if expected and args.sandbox: + # Zenodo synthesizes prereserve_doi with a hardcoded production prefix + # (see dump_prereserve_doi in zenodo-rdm's legacy serializer) while + # minting under the instance's configured DATACITE_PREFIX, which is + # 10.5072 on sandbox. Only the prefix moves; the record id is the same + # on both sides. Expect exactly that swap rather than waiving the check + # on sandbox altogether, so rehearsals still exercise it. + expected = expected.replace(f"{PRODUCTION_DOI_PREFIX}/", f"{SANDBOX_DOI_PREFIX}/", 1) + + if expected and doi != expected: + sys.exit( + f"Published DOI {doi} differs from the {expected} that is baked " + f"into the round's pages and results.json" ) - if args.sandbox: - # Sandbox pre-reserves under the production prefix (10.5281) but - # publishes under its own (10.5072), so test rounds always show - # this and their DOIs are meaningless anyway. - print(f"Warning: {message}. This is expected on sandbox.") - else: - sys.exit(message) emit_outputs(doi=doi, concept_doi=result.get("conceptdoi", ""))