v4.29.0-rc2: olean version mismatch in release tarball

Stream: lean4

[Nicolas Rouquette]

I noticed that all .olean files shipped in the v4.29.0-rc2 release are stamped with version 4.30.0-rc2 in their headers, while the lean binary correctly reports 4.29.0-rc2. Previous releases (v4.29.0-rc1, v4.28.0) don't have this mismatch.

lake build is unaffected (it uses .olean.private files internally), but downstream tooling that reads .olean headers to validate cache consistency will see version mismatches against the toolchain.

I ran into this while updating doc-verification-bridge to v4.29.0-rc2 — its experiment pipeline validates .olean versions, and due to this bug, the system toolchain files appear contaminated.

I filed the olean issue as https://github.com/leanprover/lean4/issues/12681

[Kim Morrison]

Thanks. I will fix this soon. Do remember the announcement about v4.29.0 explicitly discourages downstream projects from adopting it yet. :-)

[Kim Morrison]

Unfortunately the 4.30.0 version was already baked into the stage0: unusually this time I made v4.29.0-rc2 from further along master than v4.29.0-rc1, rather than cherry-picking a few commits. An update-stage0 had landed in the meantime.

This will require an rc3, which I need to make anyway soon.

[Kim Morrison]

lean#12700 will prevent this happening again