lean4-htt/doc/dev
Kim Morrison 8059477292
fix: auto-update ProofWidgets4 pin in mathlib4 during releases (#12503)
This PR adds automatic ProofWidgets4 version pin updates to
`release_steps.py` when processing mathlib4. ProofWidgets4 uses
sequential version tags (`v0.0.X`) rather than toolchain-based tags
(`v4.X.Y`), so the existing regex that updates dependency versions in
lakefiles doesn't match it. This has caused CI failures in two
consecutive releases where the mathlib4 PR was created with a stale
ProofWidgets4 pin.

Changes:
- `script/release_steps.py`: Add `find_proofwidgets_tag()` to look up
the latest ProofWidgets4 tag compatible with the target toolchain, and
use it to update mathlib4's lakefile automatically
- `doc/dev/release_checklist.md`: Document the ProofWidgets4 pin update
step for mathlib4

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-02-16 22:39:22 +00:00
..
bootstrap.md doc: fix typos (#12418) 2026-02-10 19:26:49 +00:00
commit_convention.md doc: commit conventions and Mathlib CI (#6605) 2025-01-13 02:29:46 +00:00
debugging.md doc: stderrAsMessages is now the default on the cmdline as well (#4955) 2024-08-08 10:28:22 +00:00
ffi.md doc: replace ffi.md with links to the reference manual (#11737) 2025-12-19 07:23:06 +00:00
index.md doc: testing Lean while avoiding rebuilds for downstream projects (#10328) 2025-09-10 13:53:34 +00:00
release_checklist.md fix: auto-update ProofWidgets4 pin in mathlib4 during releases (#12503) 2026-02-16 22:39:22 +00:00
testing.md doc: note that tests/lean/run disables linters (#11595) 2025-12-11 01:33:07 +00:00