Give PRs stacked on a bump branch their checks back (and pin lean4export to the toolchain)

[Vilin97]

#301 is the first real answer to a challenge — the Odlyzko bound, proved in a 210-file pooled project with a thin Solution/Odlyzko.lean bridge. Comparator never ran on it, and two separate things were in the way.

The branch filter

challenge-verify.yml declared pull_request: branches: [main], and #301 targets bump/v4.33.0-rc1. During a version bump that is exactly where solution work stacks, so the check that decides whether a solution is real was skipped precisely when a solution arrived.

Its draft status was never the cause — the workflows without a branch filter (the PR guard, the partial-port audit, the metadata advisory) all ran on that same draft PR. Whether a proof proves the challenge has nothing to do with which branch it is heading for, so the filter is gone.

The lean4export pin

The bump is about to break verification in a way a 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.

So the workflow now asserts the coupling before building anything, and prints the replacement SHA:

::error::LEAN4EXPORT_COMMIT is pinned to a lean4export that does
not match lean-toolchain (v4.33.0-rc1). Comparator would fail
reading this repository's oleans. Set it in this workflow to:
  LEAN4EXPORT_COMMIT: af5aa64bb914c3c2c781f378088dbd38acf4f804

This means #295 needs that one-line pin update before or with the bump; otherwise Verify challenge solutions goes red on main the moment the bump lands.

Tested by extracting the check and running it against the current toolchain with the correct pin (passes), a simulated v4.33 bump with the stale pin (fails with the SHA above), and the same bump with the correct pin (passes). Lightweight tags answer only the plain ls-remote query while annotated ones need ^{}, so it asks for both; an unknown tag warns and moves on rather than blocking.

🤖 Generated with Claude Code

[greptile-apps]

Pin check runs unconditionally, including on cache hits

The git ls-remote call executes on every workflow run — even when the tools cache is a hit and no rebuild is needed. When the toolchain hasn't changed, the check will always pass (the cache key already includes both LEAN4EXPORT_COMMIT and hashFiles('lean-toolchain')), so it's essentially a no-op on cache hits while adding a synchronous network round-trip. Adding if: steps.tools.outputs.cache-hit != 'true' would eliminate the latency on warm cache runs without weakening correctness, since a stale pin would bust the cache and trigger a miss anyway. That said, the unconditional check does function as a final safety net against hand-edited LEAN4EXPORT_COMMIT values, so the trade-off is deliberate.

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[greptile-apps]

Greptile Summary

This PR fixes two gaps that caused PR #301 (the first Odlyzko challenge solution) to receive no automated checks at all: the challenge-verification workflow now fires on PRs targeting any branch (not just main), and the build CI now also covers PRs that stack on bump/** branches.

• challenge-verify.yml: Drops the branches: [main] guard from the pull_request trigger; the existing paths filter is sufficient scoping. Adds a new step that resolves the expected lean4export commit for the current toolchain version via git ls-remote before any build work, failing fast with the correct replacement SHA if the pin is stale.
• lean_action_ci.yml: Extends the pull_request: branches list with bump/** so solution PRs that stack on a bump branch get the full build/lint/quality pipeline. The push event is unchanged (still restricted to main).

Confidence Score: 4/5

Safe to merge — both changes address real gaps that caused a verified challenge solution to receive no CI at all, and the new pin-validation step fails fast with an actionable error message rather than silently producing a broken export.

The branch-filter removals are straightforward and well-scoped by the existing paths filters. The lean4export pin check logic is correct: it handles both lightweight and annotated tags, warns gracefully when no tag exists, and fails with the exact replacement SHA when the pin is stale. The one minor point is that the network call runs unconditionally even on cache hits, adding a round-trip that is essentially a no-op in the warm-cache case, but this is a deliberate design choice rather than a defect.

Files Needing Attention: No files require special attention, but challenge-verify.yml is worth a second read around the new pin-check step to confirm the git ls-remote placement relative to the tools-cache gate is intentional.

Important Files Changed

Filename	Overview
.github/workflows/challenge-verify.yml	Removes the branches: [main] filter from pull_request trigger (so verification now fires on PRs targeting any branch), and adds a new step that validates the LEAN4EXPORT_COMMIT pin against the lean-toolchain version before building anything.
.github/workflows/lean_action_ci.yml	Adds bump/** to the pull_request: branches filter so the build/lint/quality pipeline also runs on PRs that target a bump branch. No logic changes otherwise.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[PR opened] --> B{Target branch?}
    B -->|main| C[lean_action_ci.yml triggered]
    B -->|bump/**| C
    B -->|other| D[lean_action_ci.yml skipped]

    A --> E{Paths match Challenge/Solution/toolchain?}
    E -->|Yes - any branch| F[challenge-verify.yml triggered]
    E -->|No| G[challenge-verify.yml skipped]

    F --> H[Restore caches]
    H --> I[Install Lean + uv + Mathlib]
    I --> J[Cache verification tools?]
    J -->|miss| K[Build landrun]
    J -->|hit| L[Check lean4export pin vs lean-toolchain]
    K --> L

    L -->|tag found & matches| M[Build lean4export / comparator]
    L -->|tag found & MISMATCH| N[::error:: print correct SHA, exit 1]
    L -->|tag not found| O[::warning:: skip pin check, exit 0]

    M --> P[Verify every solved challenge via comparator]

Loading

_{Reviews (1): Last reviewed commit: "Build and gate PRs stacked on a bump bra..." | Re-trigger Greptile}

[github-actions]

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.