Arena rounds: archived, citable snapshots of the arena - #169
Merged
Conversation
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-<name>` 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/<name>/ 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.
nomeata
changed the title
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/<name>/ 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-<digit>` 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.
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.
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.
The release_url was reconstructed as round-<name>, so a test round released under test-round-<name> 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.
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/<name>/, 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.
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.
# Conflicts: # templates/base.html
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 </head> 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.
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.
nomeata
marked this pull request as ready for review
August 28, 2026 08:28
nomeata
enabled auto-merge (squash)
August 28, 2026 08:28
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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-<name>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-*tagsrun 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_pathvariable rather than a template block, since the stylesheet link is no longer
the only one that needs it.