From 47221158112a695b1dc8bc76627f503d7328d368 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 28 Jul 2026 23:52:55 -0700 Subject: [PATCH 1/2] Verify solutions wherever they target, and pin lean4export to the toolchain MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two things kept comparator away from PR #301, the first real solution to a challenge (the Odlyzko bound, proved in a 210-file pooled project). First, `challenge-verify.yml` only ran on PRs targeting `main`, and #301 targets `bump/v4.33.0-rc1` — during a version bump that is exactly where solution work stacks. Whether a proof proves the challenge has nothing to do with which branch it is heading for, so the filter is gone. (Its draft status was never the cause: the workflows without a branch filter ran on it fine.) Second, the bump is about to break verification in a way the commit pin hides. lean4export reads the oleans our build produced, so its version has to track `lean-toolchain`; pinned at the v4.32.0-rc1 tag it cannot read v4.33 oleans, and the failure would surface inside an export as a file-format error rather than as a stale pin. Assert the coupling up front and print the replacement SHA — for v4.33.0-rc1 that is af5aa64bb914c3c2c781f378088dbd38acf4f804. Lightweight tags answer only the plain ls-remote query, annotated ones need `^{}`, so it asks for both; an unknown tag warns and moves on rather than blocking. Co-Authored-By: Claude Opus 5 --- .github/workflows/challenge-verify.yml | 39 ++++++++++++++++++++++++-- 1 file changed, 37 insertions(+), 2 deletions(-) diff --git a/.github/workflows/challenge-verify.yml b/.github/workflows/challenge-verify.yml index de86e436d..d165fe420 100644 --- a/.github/workflows/challenge-verify.yml +++ b/.github/workflows/challenge-verify.yml @@ -16,9 +16,13 @@ name: Verify challenge solutions # landrun is defence in depth on top of the ephemeral runner. on: + # Deliberately not restricted to PRs targeting `main`. A solution lands + # wherever the work is happening — during a Lean/Mathlib bump, solution PRs + # stack on the bump branch — and whether a proof proves the challenge has + # nothing to do with which branch it is heading for. PR #301 (the first + # solution to the Odlyzko challenge) got no verification at all because it + # targeted `bump/v4.33.0-rc1`. pull_request: - branches: - - main paths: - 'Challenge/**' - 'Challenge.lean' @@ -120,6 +124,37 @@ jobs: if: steps.tools.outputs.cache-hit != 'true' run: go install "github.com/zouuup/landrun/cmd/landrun@$LANDRUN_COMMIT" + # lean4export reads the oleans this repository's build produced, so its + # version has to track `lean-toolchain`. That coupling is invisible in a + # commit pin: a version bump that forgets it fails later, inside an + # export, with an error about the file format rather than the pin. Say + # it here instead, with the replacement SHA already resolved. + - name: Check the lean4export pin matches the toolchain + run: | + set -euo pipefail + toolchain="$(cut -d: -f2 lean-toolchain)" + # Annotated tags need the `^{}` dereference to reach the commit; + # lightweight ones (what lean4export uses today) answer only the + # plain query. Ask for both rather than depend on which it is. + expected="$(git ls-remote https://github.com/leanprover/lean4export \ + "refs/tags/$toolchain^{}" | cut -f1)" + if [ -z "$expected" ]; then + expected="$(git ls-remote https://github.com/leanprover/lean4export \ + "refs/tags/$toolchain" | cut -f1)" + fi + if [ -z "$expected" ]; then + echo "::warning::lean4export has no $toolchain tag; leaving the pin alone." + exit 0 + fi + if [ "$expected" != "$LEAN4EXPORT_COMMIT" ]; then + echo "::error::LEAN4EXPORT_COMMIT is pinned to a lean4export that does" + echo "not match lean-toolchain ($toolchain). Comparator would fail" + echo "reading this repository's oleans. Set it in this workflow to:" + echo " LEAN4EXPORT_COMMIT: $expected" + exit 1 + fi + echo "lean4export pin matches $toolchain." + - name: Build lean4export if: steps.tools.outputs.cache-hit != 'true' run: | From b96ffaeddc388ab5d76bc5d2e5950dfb3373dc13 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 28 Jul 2026 23:54:07 -0700 Subject: [PATCH 2/2] Build and gate PRs stacked on a bump branch Same class of bug as the challenge-verify filter: work stacked on a bump branch got no Lean build, no linters, and no quality checks, so a 210-file contribution sat in PR #301 with nothing having compiled it. Add bump/** to the pull_request branch filter. Co-Authored-By: Claude Opus 5 --- .github/workflows/lean_action_ci.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index c605deffc..1b89034f9 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -42,6 +42,11 @@ on: pull_request: branches: - main + # Work stacks on the bump branch during a Lean/Mathlib migration, and + # a contribution that never builds is a contribution nobody can judge: + # PR #301 added a 210-file project onto `bump/v4.33.0-rc1` and got no + # build, no linters, and no quality checks at all. + - 'bump/**' paths: - '**/*.lean' - 'lakefile.toml'