submission.yml

# Auth (lean-eval-bot GitHub App + 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
# (read-only token in the evaluate job, .git stripped before lake runs,
# `_prime_workspace` not pre-building any user-controlled targets, etc.)
# are documented in LANDRUN.md → "What must not regress when this is
# fixed". Read that section before editing this file or
# `scripts/evaluate_submission.py`.
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:
  fetch:
    if: github.event.label.name == 'submission'
    runs-on: ubuntu-latest
    timeout-minutes: 10
    permissions:
      contents: read
      issues: write
    steps:
      # 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'

      - 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: Fetch submission
        id: fetch
        env:
          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: Upload submission source artifact
        if: 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-source
          path: |
            /tmp/fetch-out/source.tar.gz
            /tmp/fetch-out/metadata.json
          if-no-files-found: error
          retention-days: 7

      - name: Comment on fetch failure
        if: 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

  evaluate:
    needs: fetch
    runs-on: ubuntu-latest
    timeout-minutes: 90
    # Deliberately minimal: contents:read is only enough to clone this
    # public benchmark repo. No issues:write, no contents:write, no
    # packages. persist-credentials:false + rm -rf .git below ensures the
    # token cannot persist into the lake runtime.
    permissions:
      contents: read
    steps:
      - 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.
        # 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

      # actions/checkout pinned to 11bd7190 (= refs/tags/v4.2.2 as of 2026-05-04).
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
        with:
          persist-credentials: false

      - name: Strip git state before running untrusted Lean
        run: rm -rf .git

      # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          use-mathlib-cache: true

      # actions/setup-go pinned to d35c59ab (= refs/tags/v5.5.0 as of 2026-05-04).
      - uses: actions/setup-go@d35c59abb061a4a6fb18e82ac0862c26744d6ab5
        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: 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 12581a6b (= refs/tags/v4.30.0-rc2 as of 2026-05-04).
          # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
          git checkout 12581a6b680d8478175596338eb2d53383a323e3  # 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: 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. See SECURITY.md > "Validations done at submission time".
      - name: Probe sandbox is engaged
        run: python scripts/sandbox_engaged_probe.py --require-tools

      - name: Probe env-var allowlist
        run: python scripts/security_probes/env_dump_probe.py --require-tools

      # actions/download-artifact pinned to d3f86a10 (= refs/tags/v4.3.0 as of 2026-05-04).
      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
        with:
          name: submission-source
          path: /tmp/submission-artifact

      - name: Extract submission source
        run: |
          mkdir -p /tmp/submission-src
          tar -xzf /tmp/submission-artifact/source.tar.gz -C /tmp/submission-src --strip-components=1

      - name: Run evaluate_submission.py
        # Sharing the host 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 generated \
            --manifest manifests/problems.toml \
            --output-dir /tmp/evaluate-out \
            --repo-root "$PWD" \
            --shared-packages "$PWD/.lake/packages"

      - name: Copy frozen metadata through to record
        if: always()
        run: cp /tmp/submission-artifact/metadata.json /tmp/evaluate-out/metadata.json || true

      - name: Upload evaluate results artifact
        if: always()
        # 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

  record:
    needs: evaluate
    runs-on: ubuntu-latest
    timeout-minutes: 10
    permissions:
      contents: read
      issues: write
    steps:
      # actions/checkout pinned to 11bd7190 (= refs/tags/v4.2.2 as of 2026-05-04).
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
        with:
          persist-credentials: false
          path: lean-eval

      # 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

      # actions/checkout pinned to 11bd7190 (= refs/tags/v4.2.2 as of 2026-05-04).
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
        with:
          repository: leanprover/lean-eval-leaderboard
          token: ${{ secrets.LEADERBOARD_WRITE_TOKEN }}
          path: leaderboard

      - name: Configure git identity
        run: |
          git -C leaderboard config user.email "lean-eval-bot@users.noreply.github.com"
          git -C leaderboard 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
        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 leaderboard fetch origin main
            git -C leaderboard reset --hard origin/main

            OUTPUT=$(python lean-eval/scripts/update_leaderboard.py \
              --user "$SUBMITTED_BY" \
              --leaderboard-dir leaderboard \
              --results-json "$RESULTS_PATH" \
              --benchmark-commit "${{ github.sha }}" \
              --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 leaderboard add results/
            git -C leaderboard commit -m "$COMMIT_MSG"
            if git -C leaderboard push origin main; then
              echo "leaderboard push succeeded on attempt $attempt"
              break
            fi
            echo "leaderboard 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 to the leaderboard after $MAX_ATTEMPTS attempts (race). An operator will need to retry this submission."
              exit 1
            fi
          done

      - 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 but the pipeline did not
  # complete cleanly — most often `evaluate` failing because the
  # submitter's Submission.lean did not compile. Without this, the
  # `record` job is skipped (its `needs: evaluate` dependency was unmet)
  # and the submitter sees no comment at all.
  notify:
    needs: [fetch, evaluate, record]
    if: always() && needs.fetch.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 }}
          RECORD_RESULT: ${{ needs.record.result }}
        run: |
          if [ "$EVALUATE_RESULT" = "success" ]; then
            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 }}"
          else
            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 }}"
          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