[submission] platonic_classification #775
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
| # Auth (lean-eval-bot GitHub App, lean-eval-recorder GitHub App, and | |
| # LEADERBOARD_WRITE_TOKEN PAT) is documented in docs/ci-secrets.md. | |
| # | |
| # Security model: untrusted submitter Lean code is ONLY ever elaborated | |
| # inside comparator's landrun sandbox (invoked from `lake test` via | |
| # WorkspaceTest.lean). The non-negotiable invariants of this workflow | |
| # (`APP_INSTALLATION_TOKEN` scoped to the single `Fetch submission` | |
| # step's env, .git stripped from BOTH checkouts before lake runs, | |
| # `_prime_workspace` not pre-building any user-controlled targets, etc.) | |
| # are documented in SECURITY.md. Read that section before editing this | |
| # file or `scripts/evaluate_submission.py`. | |
| # | |
| # Fetch + evaluate live in a single job on purpose: a previous version | |
| # uploaded the cloned source as a `submission-source` artifact so a | |
| # separate `evaluate` job could pick it up, but on a public repo | |
| # anyone authenticated can download workflow artifacts via the API, | |
| # which leaked private submissions. Keeping fetch and evaluate | |
| # co-located removes the cross-runner transport entirely. Do not | |
| # re-split these jobs. | |
| # | |
| # Two checkouts: this repo (lean-eval-submissions) supplies the | |
| # pipeline scripts; `leanprover/lean-eval` supplies the benchmark | |
| # (generated/ workspaces, manifests/, the `lean-eval` Lean CLI). The | |
| # submission is scored against `leanprover/lean-eval@main` HEAD and the | |
| # resolved SHA is recorded as `benchmark_commit`. | |
| name: Submission | |
| on: | |
| issues: | |
| types: [labeled] | |
| concurrency: | |
| # Per-issue concurrency: each submission issue gets its own group so | |
| # parallel submissions from the same user do not cancel each other. | |
| # GitHub keeps at most 1 running + 1 pending per group, and any newer | |
| # pending run cancels the previously-pending one — which manifested as | |
| # silent dropouts when several issues were filed in quick succession. | |
| # Concurrent leaderboard pushes from sibling runs are already handled | |
| # by the `record` job's push-retry loop below. | |
| group: submission-issue-${{ github.event.issue.number }} | |
| cancel-in-progress: false | |
| jobs: | |
| evaluate: | |
| if: github.event.label.name == 'submission' | |
| # TEMPORARY: self-hosted chonk pool. Even ubuntu-latest-large (64 GB) | |
| # SIGTERM'd (exit 143) at ~99% of issue #467's multi-hour build, hitting | |
| # the hosted per-job memory cap. chonk has the memory headroom to finish. | |
| # This routes UNTRUSTED submission Lean onto self-hosted hardware; it is | |
| # acceptable only because the comparator runs inside the landrun sandbox | |
| # (--ro /, verified by the "Probe sandbox is engaged" step). Revert to a | |
| # GitHub-hosted runner once #467 is through. See docs/audit-archive.md. | |
| runs-on: [self-hosted, chonk] | |
| # 360 minutes is GitHub's per-job ceiling for hosted runners; set it | |
| # explicitly so genuinely long proofs run to the platform limit rather | |
| # than being cut off, and so the intended cap stays visible here. | |
| timeout-minutes: 360 | |
| # `issues: write` is needed by the in-job fetch-failure / evaluate-failure | |
| # commenters below. The default `GITHUB_TOKEN` is *not* placed into the | |
| # env of any step that runs untrusted Lean: it only appears in the | |
| # explicit `env: GH_TOKEN:` blocks on the commenter steps. The | |
| # `lean-eval-bot` installation token (which can read private | |
| # submission repos) is similarly scoped to the single `Fetch | |
| # submission` step's env. persist-credentials:false on BOTH checkouts | |
| # + `rm -rf .git` on BOTH before lake runs ensures no checkout token | |
| # persists into the lake runtime either. | |
| permissions: | |
| contents: read | |
| issues: write | |
| # Surfaces whether the fetch step succeeded to the downstream `notify` | |
| # job, which otherwise cannot distinguish fetch failure (already | |
| # commented inline) from evaluate failure (needs a comment). | |
| # `benchmark_commit` is the resolved leanprover/lean-eval@main HEAD the | |
| # submission was scored against; the `record` job records it. | |
| outputs: | |
| fetch_succeeded: ${{ steps.fetch_status.outputs.succeeded }} | |
| size_within_cap: ${{ steps.size_status.outputs.within_cap }} | |
| audit_ciphertext_ready: ${{ steps.audit_status.outputs.ready }} | |
| benchmark_commit: ${{ steps.benchmark.outputs.sha }} | |
| steps: | |
| # This repo (lean-eval-submissions): supplies the pipeline scripts. | |
| # actions/checkout pinned to 11bd7190 (= refs/tags/v4.2.2 as of 2026-05-04). | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 | |
| with: | |
| persist-credentials: false | |
| # The benchmark repo: supplies generated/, manifests/, the Lean CLI. | |
| # Scored against main HEAD; persist-credentials:false because this | |
| # tree shares the runner with the untrusted build. | |
| # actions/checkout pinned to 11bd7190 (= refs/tags/v4.2.2 as of 2026-05-04). | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 | |
| with: | |
| repository: leanprover/lean-eval | |
| ref: main | |
| path: lean-eval | |
| persist-credentials: false | |
| - name: Resolve benchmark commit | |
| id: benchmark | |
| run: echo "sha=$(git -C lean-eval rev-parse HEAD)" >> "$GITHUB_OUTPUT" | |
| # Self-hosted (NixOS chonk) provisioning. The GitHub-hosted setup-* | |
| # actions and the apt `Install age` step below are guarded to | |
| # github-hosted only; on nix they cannot work (no FHS prebuilts / | |
| # no apt). Supply the two tools the job is missing here — go (for | |
| # `go install` landrun) and age (audit encryption) — by building | |
| # them from nixpkgs and prepending to PATH. python / lean / elan / | |
| # lake / git / gh are already on the runner; elan provides the | |
| # pinned toolchain. nix-ld lets the resulting prebuilt binaries run. | |
| - name: Provision tools via nix (self-hosted) | |
| # The chonk runner's service PATH is curated (it has python and git | |
| # but not go, age, the Lean toolchain, or `which`). Supply the rest | |
| # from nixpkgs and prepend to PATH for every later step. The `elan` | |
| # package ships the `lake`/`lean` shims, which resolve the pinned | |
| # toolchain per `lean-toolchain`; nix-ld runs the fetched binaries. | |
| # `which` is needed by EvalTools' comparator-installation check, | |
| # which shells out to `which landrun` / `which lean`. The `^out` | |
| # output selector keeps multi-output packages (which) to one path. | |
| if: runner.environment != 'github-hosted' | |
| run: | | |
| { | |
| echo "$(nix build --no-link --print-out-paths 'nixpkgs#go^out')/bin" | |
| echo "$(nix build --no-link --print-out-paths 'nixpkgs#age^out')/bin" | |
| echo "$(nix build --no-link --print-out-paths 'nixpkgs#elan^out')/bin" | |
| echo "$(nix build --no-link --print-out-paths 'nixpkgs#which^out')/bin" | |
| } >> "$GITHUB_PATH" | |
| # actions/setup-python pinned to a26af69b (= refs/tags/v5.6.0 as of 2026-05-04). | |
| - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 | |
| if: runner.environment == 'github-hosted' | |
| with: | |
| python-version: '3.11.10' | |
| - name: Extract source owner from issue body | |
| id: owner | |
| env: | |
| ISSUE_BODY: ${{ github.event.issue.body }} | |
| run: | | |
| python - <<'PY' | |
| import os, re, sys | |
| body = os.environ.get("ISSUE_BODY", "") | |
| m = re.search( | |
| r"^###\s+Submission URL\s*\n+(?P<value>.+?)(?=\n+###\s|\Z)", | |
| body, | |
| re.MULTILINE | re.DOTALL, | |
| ) | |
| if not m: | |
| sys.exit("no Submission URL section in issue body") | |
| url = m.group("value").strip() | |
| out_path = os.environ["GITHUB_OUTPUT"] | |
| with open(out_path, "a") as fh: | |
| repo = re.match(r"https://github\.com/([^/]+)/", url) | |
| if repo: | |
| fh.write(f"kind=github_repo\n") | |
| fh.write(f"owner={repo.group(1)}\n") | |
| elif url.startswith("https://gist.github.com/"): | |
| fh.write(f"kind=gist\n") | |
| fh.write(f"owner=\n") | |
| else: | |
| sys.exit(f"unsupported URL in issue body: {url!r}") | |
| PY | |
| - name: Mint lean-eval-bot installation token | |
| id: app_token | |
| if: steps.owner.outputs.kind == 'github_repo' | |
| # actions/create-github-app-token pinned to d72941d7 (= refs/tags/v1 as of 2026-05-04). | |
| uses: actions/create-github-app-token@d72941d797fd3113feb6b93fd0dec494b13a2547 | |
| continue-on-error: true | |
| with: | |
| app-id: ${{ secrets.LEAN_EVAL_BOT_APP_ID }} | |
| private-key: ${{ secrets.LEAN_EVAL_BOT_PRIVATE_KEY }} | |
| owner: ${{ steps.owner.outputs.owner }} | |
| - name: Clean scratch dirs (self-hosted runner reuse) | |
| # Self-hosted chonk runners persist /tmp across jobs, unlike the | |
| # ephemeral hosted runners this workflow was written for. Stale | |
| # scratch state breaks fetch's checkout ("untracked working tree | |
| # files would be overwritten ... Aborting") and could otherwise | |
| # leak one submission's source into the next job's build. Wipe the | |
| # scratch dirs at job start; on hosted runners they do not exist | |
| # yet, so the rm is a harmless no-op. | |
| run: rm -rf /tmp/fetch-out /tmp/submission-src /tmp/evaluate-out /tmp/audit-encrypt | |
| - name: Fetch submission | |
| id: fetch | |
| env: | |
| # Step-scoped: the app token is NOT present in the env of any | |
| # later step in this job. This is the load-bearing assumption | |
| # that lets fetch + evaluate share a job without leaking | |
| # access to private submission repos into the landrun-sandboxed | |
| # evaluation. Do not promote this to a job-level env or | |
| # secrets block. | |
| APP_INSTALLATION_TOKEN: ${{ steps.app_token.outputs.token }} | |
| run: | | |
| python scripts/fetch_submission.py \ | |
| --event-path "$GITHUB_EVENT_PATH" \ | |
| --output-dir /tmp/fetch-out | |
| - name: Record fetch status for downstream jobs | |
| id: fetch_status | |
| if: always() | |
| run: | | |
| if [ "${{ steps.fetch.outcome }}" = "success" ]; then | |
| echo "succeeded=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "succeeded=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Comment on fetch failure | |
| if: failure() && steps.fetch.outcome == 'failure' | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| gh issue comment ${{ github.event.issue.number }} \ | |
| --repo "${{ github.repository }}" \ | |
| --body "❌ Submission fetch failed. See the workflow logs: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}. If your submission repo is private, make sure the \`lean-eval-bot\` GitHub App is installed on it." | |
| gh issue close ${{ github.event.issue.number }} --repo "${{ github.repository }}" --reason "not planned" || true | |
| # Audit-archive integration. The compressed source tar produced by | |
| # fetch_submission.py is capped at 10 MiB (see docs/audit-archive.md | |
| # > "Size cap"), then encrypted with `age` against | |
| # `.audit/recipients.txt` and uploaded as a ciphertext-only artifact | |
| # for the `archive` job to push to leanprover/lean-eval-audit. | |
| # | |
| # Order: BEFORE the expensive lean/landrun/comparator setup so that | |
| # a size-cap failure rejects the submission fast. The encrypted | |
| # artifact is safe to upload even on a public repo because the | |
| # plaintext source never appears in it (see SECURITY.md and the | |
| # leading comment of this file for why the plaintext source must | |
| # NEVER be uploaded as an artifact). | |
| - name: Check submission size cap | |
| id: size_check | |
| if: steps.fetch.outcome == 'success' | |
| run: | | |
| SIZE_BYTES=$(stat -c %s /tmp/fetch-out/source.tar.gz) | |
| CAP_BYTES=$((10 * 1024 * 1024)) | |
| echo "submission tarball size: ${SIZE_BYTES} bytes (cap: ${CAP_BYTES} bytes / 10 MiB)" | |
| if [ "$SIZE_BYTES" -gt "$CAP_BYTES" ]; then | |
| echo "::error::source tarball is ${SIZE_BYTES} bytes, over the ${CAP_BYTES}-byte (10 MiB) audit cap" | |
| exit 1 | |
| fi | |
| - name: Record size-cap status for downstream jobs | |
| id: size_status | |
| if: always() | |
| run: | | |
| if [ "${{ steps.size_check.outcome }}" = "success" ]; then | |
| echo "within_cap=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "within_cap=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Comment on size cap failure | |
| if: failure() && steps.size_check.outcome == 'failure' | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| SIZE_KB=$(( $(stat -c %s /tmp/fetch-out/source.tar.gz) / 1024 )) | |
| gh issue comment ${{ github.event.issue.number }} \ | |
| --repo "${{ github.repository }}" \ | |
| --body "❌ Submission rejected: the compressed source tarball is ${SIZE_KB} KiB, over the 10240 KiB (10 MiB) audit-archive cap. Every evaluated submission is retained in encrypted form for audit (see [docs/audit-archive.md](https://github.com/${{ github.repository }}/blob/main/docs/audit-archive.md)); the cap keeps that archive bounded. Trim build artifacts, large fixtures, or unrelated files from your submission repo before resubmitting." | |
| gh issue close ${{ github.event.issue.number }} --repo "${{ github.repository }}" --reason "not planned" || true | |
| - name: Install age (audit encryption) | |
| # github-hosted only: on self-hosted nix, age is provisioned above. | |
| if: runner.environment == 'github-hosted' && steps.size_check.outcome == 'success' | |
| run: sudo apt-get update -qq && sudo apt-get install -y -qq age | |
| - name: Encrypt submission for audit archive | |
| id: encrypt | |
| if: steps.size_check.outcome == 'success' | |
| run: | | |
| mkdir -p /tmp/audit-encrypt | |
| python scripts/archive_submission.py encrypt \ | |
| --source-tar /tmp/fetch-out/source.tar.gz \ | |
| --metadata /tmp/fetch-out/metadata.json \ | |
| --recipients .audit/recipients.txt \ | |
| --output-dir /tmp/audit-encrypt | |
| - name: Upload audit ciphertext artifact | |
| id: upload_audit | |
| if: steps.encrypt.outcome == 'success' | |
| # actions/upload-artifact pinned to ea165f8d (= refs/tags/v4.6.2 as of 2026-05-04). | |
| # Safe to upload on a public repo because the artifact contains | |
| # only the age-encrypted ciphertext and the unencrypted sidecar | |
| # metadata, never the plaintext source. See docs/audit-archive.md | |
| # > "Threat model" and the SECURITY.md note that forbids uploading | |
| # the plaintext source. | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: submission-audit-ciphertext | |
| path: | | |
| /tmp/audit-encrypt/source.tar.gz.age | |
| /tmp/audit-encrypt/sidecar.partial.json | |
| if-no-files-found: error | |
| retention-days: 7 | |
| - name: Record audit-ciphertext readiness for downstream jobs | |
| id: audit_status | |
| if: always() | |
| run: | | |
| # `archive` and `notify` both branch on this. Without it, an | |
| # encrypt or artifact-upload failure would make `archive` start, | |
| # fail at download-artifact, and the submitter would see a | |
| # generic "evaluation did not produce results" message instead | |
| # of the correct "audit encryption failed" one. | |
| if [ "${{ steps.encrypt.outcome }}" = "success" ] \ | |
| && [ "${{ steps.upload_audit.outcome }}" = "success" ]; then | |
| echo "ready=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "ready=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Free disk space for Mathlib cache | |
| # Standard runners ship with ~14GB free; Mathlib unpacked is | |
| # several GB and we hold it twice (repo root + per-workspace). | |
| # Strip Android, .NET, Haskell, and other preinstalled caches we | |
| # do not need. Frees ~30GB. | |
| # GitHub-hosted only: on a self-hosted runner this action would | |
| # delete the host's Docker images and system toolchains. chonk has | |
| # ample disk, so skip it there. | |
| if: runner.environment == 'github-hosted' | |
| # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04). | |
| uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be | |
| with: | |
| tool-cache: false | |
| android: true | |
| dotnet: true | |
| haskell: true | |
| large-packages: false | |
| docker-images: true | |
| swap-storage: false | |
| - name: Strip git state before running untrusted Lean | |
| # Both checkouts: comparator's landrun policy is `--ro /`, so any | |
| # authenticated remote left in a `.git/config` anywhere the | |
| # sandbox can stat it is readable by the untrusted Lean elaborator. | |
| run: rm -rf .git lean-eval/.git | |
| # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04). | |
| # github-hosted only: lean-action's helper scripts use a /bin/bash | |
| # shebang that does not exist on NixOS (bad interpreter, exit 126). | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| if: runner.environment == 'github-hosted' | |
| with: | |
| lake-package-directory: lean-eval | |
| use-mathlib-cache: true | |
| - name: Lean toolchain + mathlib cache (self-hosted) | |
| # Self-hosted nix equivalent of lean-action above: elan (on PATH) | |
| # resolves the pinned toolchain, `cache get` fetches Mathlib oleans, | |
| # and `lake build` builds the harness. nix-ld lets the elan-fetched | |
| # toolchain binaries run. | |
| if: runner.environment != 'github-hosted' | |
| working-directory: lean-eval | |
| run: | | |
| lake exe cache get | |
| lake build | |
| # actions/setup-go pinned to d35c59ab (= refs/tags/v5.5.0 as of 2026-05-04). | |
| # github-hosted only: on self-hosted nix, go is provisioned above. | |
| - uses: actions/setup-go@d35c59abb061a4a6fb18e82ac0862c26744d6ab5 | |
| if: runner.environment == 'github-hosted' | |
| with: | |
| # Concrete Go version, not `stable`, so a runner-image bump cannot | |
| # silently change the toolchain we install landrun with. | |
| go-version: '1.24.0' | |
| - name: Install landrun | |
| run: | | |
| # landrun pinned to 5ed4a3db (zouuup/landrun main HEAD as of 2026-05-04). | |
| # Bump procedure: leanprover/lean-eval SECURITY.md > "Bumping pinned dependencies". | |
| go install github.com/zouuup/landrun/cmd/landrun@5ed4a3db3a4ad930d577215c6b9abaa19df7f99f | |
| echo "$(go env GOPATH)/bin" >> "$GITHUB_PATH" | |
| - name: Build lean4export | |
| run: | | |
| git clone https://github.com/leanprover/lean4export.git .ci/lean4export | |
| cd .ci/lean4export | |
| # lean4export pinned to 3de59f10 (= refs/tags/v4.32.0-rc1 as of 2026-06-27). | |
| # Bump procedure: leanprover/lean-eval SECURITY.md > "Bumping pinned dependencies". | |
| git checkout 3de59f10bc4b4a0f2de698597aeb1246caa0df0a # pin-audit: exempt -- SHA, see comment | |
| lake build lean4export | |
| echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH" | |
| - name: Build comparator | |
| run: | | |
| git clone https://github.com/leanprover/comparator.git .ci/comparator | |
| cd .ci/comparator | |
| # comparator pinned to 71b52ec2 (leanprover/comparator, originally adopted before 2026-05-04). | |
| # Bump procedure: leanprover/lean-eval SECURITY.md > "Bumping pinned dependencies". | |
| git checkout 71b52ec29e06d4b7d882726553b1ceb99a2499e0 # pin-audit: exempt -- SHA, see comment | |
| lake build comparator | |
| echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH" | |
| # SECURITY: probes that gate every submission. A regression here | |
| # (sandbox not engaged, or env-var leak) means we cannot trust any | |
| # downstream comparator verdict — abort before touching the | |
| # submission. The probe scripts live in leanprover/lean-eval (which | |
| # owns the comparator/sandbox integration); they are run here from | |
| # the lean-eval checkout. See leanprover/lean-eval SECURITY.md > | |
| # "Validations done at submission time". | |
| - name: Probe sandbox is engaged | |
| run: python lean-eval/scripts/sandbox_engaged_probe.py --require-tools | |
| - name: Probe env-var allowlist | |
| run: python lean-eval/scripts/security_probes/env_dump_probe.py --require-tools | |
| - name: Extract submission source | |
| run: | | |
| mkdir -p /tmp/submission-src | |
| tar -xzf /tmp/fetch-out/source.tar.gz -C /tmp/submission-src --strip-components=1 | |
| - name: Run evaluate_submission.py | |
| # Sharing the benchmark repo's .lake/packages tree across every | |
| # per-submission workspace lets each `lake update` reuse Mathlib | |
| # (~3GB unpacked) instead of cloning + decompressing it per | |
| # workspace. Required to handle submissions that overlay several | |
| # generated workspaces on a single runner without "no space left | |
| # on device". Assumes generated workspaces stay in lock-step with | |
| # the benchmark repo on dependency revs (they do, by construction). | |
| run: | | |
| python scripts/evaluate_submission.py \ | |
| --source-dir /tmp/submission-src \ | |
| --generated-root lean-eval/generated \ | |
| --manifest-dir lean-eval/manifests/problems \ | |
| --output-dir /tmp/evaluate-out \ | |
| --repo-root lean-eval \ | |
| --shared-packages lean-eval/.lake/packages | |
| - name: Copy frozen metadata through to record | |
| if: always() | |
| run: cp /tmp/fetch-out/metadata.json /tmp/evaluate-out/metadata.json || true | |
| - name: Upload evaluate results artifact | |
| if: always() && steps.fetch.outcome == 'success' | |
| # actions/upload-artifact pinned to ea165f8d (= refs/tags/v4.6.2 as of 2026-05-04). | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: submission-results | |
| path: /tmp/evaluate-out/* | |
| if-no-files-found: warn | |
| retention-days: 7 | |
| archive: | |
| # Pushes the encrypted submission tarball + sidecar JSON to | |
| # leanprover/lean-eval-audit using the `lean-eval-archiver` GitHub | |
| # App. Runs on a fresh runner — the archiver's write-capable | |
| # installation token must not be co-resident with untrusted Lean | |
| # elaboration. See docs/audit-archive.md > "Threat model". | |
| # | |
| # `if: always()` gated on the two evaluate outputs: archive runs | |
| # whenever the source was successfully fetched AND was within the | |
| # size cap, even if the evaluation step itself later failed (the | |
| # ciphertext artifact will exist; archiving the source is still | |
| # required for audit). On fetch-failure or size-cap-failure, archive | |
| # is skipped and the relevant in-job commenter has already explained | |
| # the rejection to the submitter. | |
| needs: evaluate | |
| if: | | |
| always() | |
| && needs.evaluate.outputs.fetch_succeeded == 'true' | |
| && needs.evaluate.outputs.size_within_cap == 'true' | |
| && needs.evaluate.outputs.audit_ciphertext_ready == 'true' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 10 | |
| permissions: | |
| contents: read | |
| steps: | |
| # This repo (lean-eval-submissions): supplies scripts/archive_submission.py. | |
| # actions/checkout pinned to 11bd7190 (= refs/tags/v4.2.2 as of 2026-05-04). | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 | |
| with: | |
| persist-credentials: false | |
| # actions/setup-python pinned to a26af69b (= refs/tags/v5.6.0 as of 2026-05-04). | |
| - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 | |
| with: | |
| python-version: '3.11.10' | |
| # actions/download-artifact pinned to d3f86a10 (= refs/tags/v4.3.0 as of 2026-05-04). | |
| # Ciphertext artifact is required: archive cannot proceed without it. | |
| - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 | |
| with: | |
| name: submission-audit-ciphertext | |
| path: /tmp/audit-in | |
| # Results artifact is optional: if evaluate failed mid-run the | |
| # results.json may not have been uploaded, but the source archive | |
| # should still be recorded (with sidecar.evaluator_verdict omitted). | |
| - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 | |
| id: results_download | |
| continue-on-error: true | |
| with: | |
| name: submission-results | |
| path: /tmp/results-in | |
| - name: Mint lean-eval-archiver installation token | |
| id: archiver_token | |
| # actions/create-github-app-token pinned to d72941d7 (= refs/tags/v1 as of 2026-05-04). | |
| uses: actions/create-github-app-token@d72941d797fd3113feb6b93fd0dec494b13a2547 | |
| with: | |
| app-id: ${{ secrets.LEAN_EVAL_ARCHIVER_APP_ID }} | |
| private-key: ${{ secrets.LEAN_EVAL_ARCHIVER_PRIVATE_KEY }} | |
| owner: leanprover | |
| repositories: lean-eval-audit | |
| - name: Push to lean-eval-audit | |
| env: | |
| # Step-scoped: never in the env of any other step in this job. | |
| # Mirrors the lean-eval-bot token scoping pattern in `evaluate`. | |
| ARCHIVER_TOKEN: ${{ steps.archiver_token.outputs.token }} | |
| run: | | |
| set -euo pipefail | |
| # Per-problem evaluator verdict lives in summary.json under | |
| # `run_eval.problems`, not in results.json (which is just | |
| # {"passed": [ids]}). See scripts/evaluate_submission.py. | |
| SUMMARY_FLAG=() | |
| if [ -f /tmp/results-in/summary.json ]; then | |
| SUMMARY_FLAG+=(--summary /tmp/results-in/summary.json) | |
| fi | |
| python scripts/archive_submission.py push \ | |
| --ciphertext /tmp/audit-in/source.tar.gz.age \ | |
| --sidecar /tmp/audit-in/sidecar.partial.json \ | |
| --benchmark-commit "${{ needs.evaluate.outputs.benchmark_commit }}" \ | |
| --workflow-run-url "${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" \ | |
| "${SUMMARY_FLAG[@]}" | |
| record: | |
| # Now gated on `archive` as well: if the audit archival did not | |
| # complete, the leaderboard must not advance either. The two | |
| # mechanisms are independent, but our policy is that a recorded | |
| # leaderboard entry implies a durable archived copy of the source. | |
| needs: [evaluate, archive] | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 10 | |
| permissions: | |
| contents: read | |
| issues: write | |
| steps: | |
| # Two checkouts of this repo. `code/` is read-only and pinned to | |
| # this workflow's own SHA: it supplies scripts/update_leaderboard.py | |
| # and must NOT be touched by the push-retry loop. `results-store/` | |
| # is the writable working copy the loop resets/commits/pushes — so | |
| # the loop can `git reset --hard origin/main` without yanking the | |
| # script out from under the running process. | |
| # actions/checkout pinned to 11bd7190 (= refs/tags/v4.2.2 as of 2026-05-04). | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 | |
| with: | |
| ref: ${{ github.sha }} | |
| persist-credentials: false | |
| path: code | |
| # actions/setup-python pinned to a26af69b (= refs/tags/v5.6.0 as of 2026-05-04). | |
| - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 | |
| with: | |
| python-version: '3.11.10' | |
| # actions/download-artifact pinned to d3f86a10 (= refs/tags/v4.3.0 as of 2026-05-04). | |
| - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 | |
| with: | |
| name: submission-results | |
| path: /tmp/submission-results | |
| # The writable results store. Checked out with the lean-eval-recorder | |
| # App token so the `record:` push to this repo's protected `main` | |
| # bypasses branch protection (the App is the ruleset bypass actor; | |
| # see docs/ci-secrets.md). | |
| - name: Mint lean-eval-recorder installation token | |
| id: recorder_token | |
| # actions/create-github-app-token pinned to d72941d7 (= refs/tags/v1 as of 2026-05-04). | |
| uses: actions/create-github-app-token@d72941d797fd3113feb6b93fd0dec494b13a2547 | |
| with: | |
| app-id: ${{ secrets.LEAN_EVAL_RECORDER_APP_ID }} | |
| private-key: ${{ secrets.LEAN_EVAL_RECORDER_PRIVATE_KEY }} | |
| # actions/checkout pinned to 11bd7190 (= refs/tags/v4.2.2 as of 2026-05-04). | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 | |
| with: | |
| token: ${{ steps.recorder_token.outputs.token }} | |
| path: results-store | |
| - name: Configure git identity | |
| run: | | |
| git -C results-store config user.email "lean-eval-bot@users.noreply.github.com" | |
| git -C results-store config user.name "lean-eval-bot" | |
| - name: Record submission with push-retry | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| METADATA_PATH: /tmp/submission-results/metadata.json | |
| RESULTS_PATH: /tmp/submission-results/results.json | |
| SUMMARY_PATH: /tmp/submission-results/summary.json | |
| BENCHMARK_COMMIT: ${{ needs.evaluate.outputs.benchmark_commit }} | |
| run: | | |
| set -euo pipefail | |
| if [ ! -f "$METADATA_PATH" ] || [ ! -f "$RESULTS_PATH" ]; then | |
| echo "missing metadata or results artifact; evaluate likely failed" | |
| gh issue comment ${{ github.event.issue.number }} \ | |
| --repo "${{ github.repository }}" \ | |
| --body "❌ Evaluation did not produce results. See: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| exit 1 | |
| fi | |
| # Read frozen metadata fields | |
| SUBMITTED_BY=$(python -c "import json,sys; print(json.load(open(sys.argv[1]))['submitted_by'])" "$METADATA_PATH") | |
| MODEL=$(python -c "import json,sys; print(json.load(open(sys.argv[1]))['model'])" "$METADATA_PATH") | |
| SUBMISSION_KIND=$(python -c "import json,sys; print(json.load(open(sys.argv[1]))['submission_kind'])" "$METADATA_PATH") | |
| SUBMISSION_REPO=$(python -c "import json,sys; print(json.load(open(sys.argv[1]))['submission_repo'])" "$METADATA_PATH") | |
| SUBMISSION_REF=$(python -c "import json,sys; print(json.load(open(sys.argv[1]))['submission_ref'])" "$METADATA_PATH") | |
| SUBMISSION_PUBLIC=$(python -c "import json,sys; print(str(json.load(open(sys.argv[1]))['submission_public']).lower())" "$METADATA_PATH") | |
| PRODUCTION_DESCRIPTION=$(python -c "import json,sys; d=json.load(open(sys.argv[1])); print(d.get('production_description') or '')" "$METADATA_PATH") | |
| if [ "$SUBMISSION_PUBLIC" = "true" ]; then | |
| PUBLIC_FLAG="--submission-public" | |
| else | |
| PUBLIC_FLAG="--no-submission-public" | |
| fi | |
| DESCRIPTION_ARGS=() | |
| if [ -n "$PRODUCTION_DESCRIPTION" ]; then | |
| DESCRIPTION_ARGS+=(--production-description "$PRODUCTION_DESCRIPTION") | |
| fi | |
| MAX_ATTEMPTS=5 | |
| for attempt in $(seq 1 $MAX_ATTEMPTS); do | |
| git -C results-store fetch origin main | |
| git -C results-store reset --hard origin/main | |
| OUTPUT=$(python code/scripts/update_leaderboard.py \ | |
| --user "$SUBMITTED_BY" \ | |
| --leaderboard-dir results-store \ | |
| --results-json "$RESULTS_PATH" \ | |
| --benchmark-commit "$BENCHMARK_COMMIT" \ | |
| --submission-kind "$SUBMISSION_KIND" \ | |
| --submission-repo "$SUBMISSION_REPO" \ | |
| --submission-ref "$SUBMISSION_REF" \ | |
| $PUBLIC_FLAG \ | |
| --model "$MODEL" \ | |
| --issue-number "${{ github.event.issue.number }}" \ | |
| "${DESCRIPTION_ARGS[@]}") | |
| CHANGED=$(python -c "import json,sys; print(json.loads(sys.argv[1])['changed'])" "$OUTPUT") | |
| if [ "$CHANGED" != "True" ]; then | |
| echo "no new records to commit" | |
| break | |
| fi | |
| COMMIT_MSG=$(python -c "import json,sys; print(json.loads(sys.argv[1])['commit_message'])" "$OUTPUT") | |
| git -C results-store add results/ | |
| git -C results-store commit -m "$COMMIT_MSG" | |
| if git -C results-store push origin HEAD:main; then | |
| echo "results push succeeded on attempt $attempt" | |
| break | |
| fi | |
| echo "results push rejected on attempt $attempt; retrying" | |
| sleep $((attempt * 2)) | |
| if [ "$attempt" -eq "$MAX_ATTEMPTS" ]; then | |
| gh issue comment ${{ github.event.issue.number }} \ | |
| --repo "${{ github.repository }}" \ | |
| --body "⚠️ Could not push the result after $MAX_ATTEMPTS attempts (race). An operator will need to retry this submission." | |
| exit 1 | |
| fi | |
| done | |
| - name: Redeploy leaderboard | |
| # Fire a repository_dispatch so the leaderboard rebuilds with the | |
| # new result. Best-effort: if the dispatch fails AFTER the result | |
| # push succeeded, the data advanced but the site did not — surface | |
| # an operator-actionable comment rather than failing the job (which | |
| # would mislead the `notify` job into reporting a record failure). | |
| env: | |
| DISPATCH_TOKEN: ${{ secrets.LEADERBOARD_WRITE_TOKEN }} | |
| COMMENT_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| ISSUE: ${{ github.event.issue.number }} | |
| run: | | |
| set -uo pipefail | |
| if GH_TOKEN="$DISPATCH_TOKEN" gh api repos/leanprover/lean-eval-leaderboard/dispatches \ | |
| -X POST \ | |
| -F event_type=results-advanced \ | |
| -F "client_payload[issue]=$ISSUE"; then | |
| echo "leaderboard redeploy dispatched" | |
| else | |
| echo "::warning::leaderboard redeploy dispatch failed" | |
| GH_TOKEN="$COMMENT_TOKEN" gh issue comment "$ISSUE" \ | |
| --repo "${{ github.repository }}" \ | |
| --body "⚠️ The result was recorded, but the leaderboard redeploy dispatch failed. An operator should re-run it: \`gh api repos/leanprover/lean-eval-leaderboard/dispatches -X POST -F event_type=results-advanced\`" || true | |
| fi | |
| - name: Comment submission summary | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| RESULTS_PATH: /tmp/submission-results/results.json | |
| SUMMARY_PATH: /tmp/submission-results/summary.json | |
| run: | | |
| set -euo pipefail | |
| BODY=$(python - <<'PY' | |
| import json, os | |
| results = json.load(open(os.environ["RESULTS_PATH"])) | |
| summary = json.load(open(os.environ["SUMMARY_PATH"])) | |
| lines = ["## Submission result", ""] | |
| passed = results.get("passed") or [] | |
| if passed: | |
| lines.append(f"✅ Newly-solved problems: {', '.join(passed)}") | |
| else: | |
| lines.append("No new problems solved in this submission.") | |
| lines.append("") | |
| re = summary.get("run_eval") or {} | |
| total = re.get("total_problems", 0) | |
| attempted = re.get("attempted_problems", 0) | |
| succeeded = re.get("succeeded_problems", 0) | |
| lines.append(f"Attempted {attempted} / {total}; succeeded on {succeeded}.") | |
| lines.append("") | |
| lines.append("### Per-problem") | |
| for entry in (re.get("problems") or [])[:50]: | |
| status = "pass" if entry.get("succeeded") else ( | |
| "fail" if entry.get("attempted") else "skipped" | |
| ) | |
| lines.append(f"- `{entry.get('id')}`: {status}") | |
| body = "\n".join(lines) | |
| CAP = 40000 | |
| if len(body) > CAP: | |
| body = body[:CAP] + "\n\n...truncated..." | |
| print(body) | |
| PY | |
| ) | |
| gh issue comment ${{ github.event.issue.number }} \ | |
| --repo "${{ github.repository }}" \ | |
| --body "$BODY" | |
| - name: Close issue | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| gh issue close ${{ github.event.issue.number }} \ | |
| --repo "${{ github.repository }}" \ | |
| --reason "completed" | |
| # Catches the case where fetch succeeded AND the size cap passed but | |
| # the pipeline did not complete cleanly — most often the evaluation | |
| # steps failing because the submitter's Submission.lean did not | |
| # compile, the audit-archive push failing, or the leaderboard | |
| # `record` job failing. Without this, the submitter sees no comment. | |
| # | |
| # Gated on `fetch_succeeded` AND `size_within_cap` so we do NOT | |
| # duplicate the in-job fetch-failure comment or the size-cap-failure | |
| # comment (those rejection paths each have their own dedicated | |
| # commenter step in the evaluate job). | |
| notify: | |
| needs: [evaluate, archive, record] | |
| if: | | |
| always() | |
| && needs.evaluate.outputs.fetch_succeeded == 'true' | |
| && needs.evaluate.outputs.size_within_cap == 'true' | |
| && ( | |
| needs.evaluate.outputs.audit_ciphertext_ready != 'true' | |
| || needs.archive.result != 'success' | |
| || needs.record.result != 'success' | |
| ) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| permissions: | |
| issues: write | |
| steps: | |
| - name: Comment on workflow failure and close issue | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| EVALUATE_RESULT: ${{ needs.evaluate.result }} | |
| ARCHIVE_RESULT: ${{ needs.archive.result }} | |
| RECORD_RESULT: ${{ needs.record.result }} | |
| # Audit-encrypt failure also fails the evaluate job, so check | |
| # it first — otherwise the submitter would see "Submission.lean | |
| # failed to compile" for what was really an infrastructure | |
| # failure unrelated to their proof. | |
| AUDIT_CIPHERTEXT_READY: ${{ needs.evaluate.outputs.audit_ciphertext_ready }} | |
| run: | | |
| if [ "$AUDIT_CIPHERTEXT_READY" != "true" ]; then | |
| BODY="❌ Audit encryption of the submission did not complete; the submission was not evaluated and the leaderboard was not updated. An operator will need to investigate. See the workflow logs: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| elif [ "$EVALUATE_RESULT" != "success" ]; then | |
| BODY="❌ Submission evaluation did not produce results (evaluate job: $EVALUATE_RESULT). The most common cause is that \`Submission.lean\` failed to compile. See the workflow logs: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| elif [ "$ARCHIVE_RESULT" != "success" ]; then | |
| BODY="❌ Audit archival did not complete (archive job: $ARCHIVE_RESULT); the leaderboard was not updated. An operator will need to investigate. See the workflow logs: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| else | |
| BODY="❌ Recording the submission to the leaderboard did not complete (record job: $RECORD_RESULT). See the workflow logs: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| fi | |
| gh issue comment ${{ github.event.issue.number }} \ | |
| --repo "${{ github.repository }}" \ | |
| --body "$BODY" | |
| gh issue close ${{ github.event.issue.number }} \ | |
| --repo "${{ github.repository }}" \ | |
| --reason "not planned" || true |