fix: validate stage0 version matches release version

[kim-em]

This PR fixes a CMake scoping bug that made the -DLEAN_VERSION_* flags passed by CI (and forwarded to stage0 via STAGE0_ARGS) completely ineffective, and adds belt-and-suspenders CI validation.

The version variables (LEAN_VERSION_MAJOR, MINOR, PATCH, IS_RELEASE) were declared with plain set(), which creates CMake normal variables that shadow cache variables set by -D on the command line. This meant the version override mechanism was dead code. In contrast, LEAN_SPECIAL_VERSION_DESC used CACHE STRING, which is why the -rc2 suffix worked correctly while the version numbers didn't — producing .olean files stamped 4.30.0-rc2 in the v4.29.0-rc2 release tarball.

The fix changes the version set() calls to use CACHE STRING "" to match the existing LEAN_SPECIAL_VERSION_DESC pattern. Additionally, CI and release_checklist.py now validate that stage0/src/CMakeLists.txt has matching version numbers.

Closes #12681

🤖 Prepared with Claude Code

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 65a0c618068bd01a933596cdb6dd3b9b482d24a8 --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-26 09:34:10)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 65a0c618068bd01a933596cdb6dd3b9b482d24a8 --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-01 13:43:04)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 65a0c618068bd01a933596cdb6dd3b9b482d24a8 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-26 09:34:12)

[Kha]

I don't think this is the right fix. We already set -DLEAN_VERSION_* in ci.yml which CMakeLists.txt should forward to stage 0 as well, why isn't this working?

[kim-em]

I don't think this is the right fix. We already set -DLEAN_VERSION_* in ci.yml which CMakeLists.txt should forward to stage 0 as well, why isn't this working?

@Kha, the problem was that I unwittingly pulled in a stage0 update from master (which was using MINOR=30) to the releases/v4.29.0 branch. Our existing validation doesn't guard against this.

[Kha]

I understand the repo state that led to this but I don't understand why the logic I described above did not lead to the stage0/ content being irrelevant here

[kim-em]

You're right — the -DLEAN_VERSION_* flags are forwarded to stage0 via STAGE0_ARGS, so they should override the hardcoded values. The reason they don't is a CMake scoping issue: the version variables were declared with plain set() (no CACHE), which creates normal variables that shadow cache variables set by -D on the command line. So the forwarded flags were dead code.

Contrast with LEAN_SPECIAL_VERSION_DESC which uses CACHE STRING — that's why the -rc2 suffix was applied correctly while the major/minor/patch numbers weren't (the .olean files were stamped 4.30.0-rc2).

I've pushed a fix that changes the version set() calls to use CACHE STRING "" to match LEAN_SPECIAL_VERSION_DESC. The CI validation is kept as belt-and-suspenders.