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 b9dc97c..2f39a78 100644 --- a/.github/workflows/build-and-deploy.yml +++ b/.github/workflows/build-and-deploy.yml @@ -3,17 +3,94 @@ 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. 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-*' 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: - 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: + 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 }} + 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 + 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" + } >> "$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 + # 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" + echo "round=$round" + echo "sandbox=$sandbox" + } >> "$GITHUB_OUTPUT" + 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 }} @@ -113,7 +190,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 @@ -132,6 +209,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 @@ -169,6 +249,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 @@ -188,7 +271,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 +294,94 @@ 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 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 + 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 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) + 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" --url "$ARENA_ROUNDS_URL/$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. + # checker failed. zenodo-reserve is skipped for non-round builds and may + # 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 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 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 @@ -275,19 +432,102 @@ 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" --tag "$GITHUB_REF_NAME" --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}' - # 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: Create the release + if: env.ROUND_READY == 'true' + run: | + prefix="lean-arena-round-$ROUND" + # 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. + # 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" \ + "/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/, 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 1000 --json tagName --jq '.[].tagName' \ + | { grep -E '^round-[0-9]{4}-[0-9]{2}$' || 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}' + + # 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}' @@ -299,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 @@ -306,6 +564,23 @@ jobs: with: artifact_name: github-pages-${{ github.run_attempt }} + # 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. + # 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() || 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=() + 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 +589,29 @@ 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" --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 new file mode 100755 index 0000000..e0b3c02 --- /dev/null +++ b/.github/zenodo.py @@ -0,0 +1,271 @@ +#!/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 + +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 +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" + +# 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" + + +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, 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; + # 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", [])) + # 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": "isIdenticalTo", + "identifier": url, + "resource_type": "dataset", + }) + 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, args.url)}, + ) + + # 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") + + 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: + 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}") + + # 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. + 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" + ) + + 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("--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", + ) + + 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") + 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") + + 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/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 dcd69c1..aeaa7cf 100644 --- a/README.md +++ b/README.md @@ -200,6 +200,90 @@ 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. 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 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 +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 its release is marked as +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 +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..18b66ea 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,25 @@ 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"]: + # 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" with open(results_json_file, "w") as f: @@ -2036,6 +2149,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 +2240,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 +2494,35 @@ 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( + "--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)", + ) + 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 +2606,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/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 6dddc18..3e84b3c 100644 --- a/templates/base.html +++ b/templates/base.html @@ -4,13 +4,14 @@ {% 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. #} + + + {# 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. #} @@ -19,6 +20,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 }}