ci(lean): adopt the rules_lean platform fix, drop the workaround and the stale patch

[avrabe]

rules_lean#30 is fixed upstream in 70f5138 — "detect host platform at fetch time, not lock time". Verified against gale rather than taken on the closure.

The lockfile is platform-neutral again

Before (lock generated on this Mac):

"mathlib": { "attributes": {
    "host_platform": "darwin_aarch64",
    "lean_version": "4.27.0", "mathlib_rev": "v4.27.0" } }

After re-resolving on the new pin:

"mathlib": { "attributes": {
    "lean_version": "4.27.0", "mathlib_rev": "v4.27.0" } }

host_platform is gone. All four platform repos are still generated (lean_{darwin,linux}_{aarch64,x86_64}) — what changed is that mathlib no longer pins one of them permanently, which is what made a Linux runner execute a Mach-O lake (#288).

So --lockfile_mode=off is removed. It was a workaround with a named exit condition, and this is that condition.

The patch is dropped, not rebased

patches/rules_lean_mathlib_timeout.patch conflicted with the upstream change (CONTENT_DOES_NOT_MATCH_TARGET near line 162). Rather than rebase it I checked whether it was still needed: it raised the lake update timeout 600 → 1800, and upstream now uses 3600 / 1200 / 7200 — all larger. It was obsolete, not merely conflicting. patches/ is now empty and removed.

CI is the kill-criterion

This is the criterion I wrote on rules_lean#30, and this PR runs it for real:

Generate MODULE.bazel.lock on macOS, commit it, then bazel test a lean_proof_test on Linux with the lock unchanged. It must fetch a Linux lake and pass.

The committed lockfile here was generated on darwin_aarch64; the Lean Proofs job runs on ubuntu-22.04. If it goes green, a macOS-generated lock produced a working Linux build — precisely what could not happen before. That is not something I can prove locally, which is the point.

Locally: bazel test //proofs/lean:all → 8 of 8.

Note

The lean job here still gates on //proofs/lean:all, so #295's PartitionSupply.lean stays covered. Merge order between the two does not matter; whichever lands second rebases onto the other.

🤖 Generated with Claude Code

https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!