[humuhumu33]

Closes #242.

What changes. Every step of ci.yml, honesty.yml and reproducibility.yml that fetches a toolchain now runs the fetch through .github/retry.sh:

• ci.yml: the seven "Install elan and the pinned Lean toolchain" steps (the vv legs and every Atlas job), both the elan installer and elan toolchain install "$(cat lean-toolchain)", and its three rustup toolchain install steps.
• honesty.yml and reproducibility.yml: their one rustup toolchain install step each. Neither installs Lean.

The bound. At most three attempts of the same command, 10 and then 20 seconds apart. When all three fail, the script exits with the third attempt's status after that attempt's own error, plus an ::error:: line naming the command. Every failing exit is retried, so an HTTP 5xx and a resolver failure (curl exit 6, the third occurrence on #242) are both covered. The command, its pinned version and the installer's own checks are the same on every attempt. Nothing about what is pinned or verified changes.

The host matrix's Rust step gains shell: bash, so that on Windows the script runs under Git Bash and not PowerShell. The step after it already does the same.

The plant (VERIFICATION.md, "A toolchain fetch is retried three times and no more"). The elan step's body was run outside Actions with HOME and GITHUB_PATH in a scratch directory:

URL	Observed
https://elan.lean-lang.org/elan-init.sh.wrong (the plant)	three curl: (22) … 404 attempts, then failed after 3 attempts (exit 22); the step exits 22
https://elan.lean-lang.invalid/elan-init.sh	three curl: (6) Could not resolve host attempts, then failed after 3 attempts (exit 6); the step exits 6
the real URL	Lean 4.32.1 installed, no retry line; the step exits 0

An HTTP 500 itself was not reproduced, because the host cannot be made to return one. The loop keys on the exit status, and the failed runs on #242 show elan toolchain install exits non-zero on a 500.

Register unchanged (443). RP-14 reads more of ci.yml than the triggers: it forbids vars., inputs. and continue-on-error, allows if: only in its three forms, counts cargo build once, and reads the gate step. It reads nothing in a toolchain step, and this change adds none of those strings. Run locally on this head: cargo xtask validate-model (audit-deferral reads .github/retry.sh), validate-spec-links, conformance_rp_13, conformance_rp_14, conformance_rp_16 and the meta-gate --test bdd. All pass.

Not covered. release.yml has the same unretried fetches. #242 names three workflows, so it is left as it is here.

🤖 Generated with Claude Code

[afflom]

Maintainer: read, and in the release/v0.5 queue. The head is green and mergeable; keep it so. The release/v0.4 landings (#255 in regeneration now, then #259, #262, #264, #265, #293, the bootstrap trio #258/#266/#282, #247, #256, and #261) hold the gate and the review agents first, by the owner's direction. The v0.5 lane is reviewed in this order as agents free up: #285, #290, #286, #287, #288, #289. Nothing is needed from you on this one before the review.

---

Generated by Claude Code

[afflom]

Maintainer: merged into release/v0.5 at 0694c7ca6 (merge commit) and #242 closed by hand. Reviewed: the bound is exactly three attempts with 10 s and 20 s between, the third attempt's status and stderr are what a permanent failure returns, the curl is inside the bash -euo pipefail -c so a fetch failure in the pipe is what gets retried, scope is the issue's three workflows with release.yml stated as untouched, RP-14 reads nothing a toolchain step contains, and the two planted runs in VERIFICATION show three attempts each. audit-deferral reads .github/*.sh.

---

Generated by Claude Code