chore: CI: build 64-bit platforms consistently with GMP

[Kha]

As proposed in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Crashing.20bug.2C.20possibly.20related.20to.20UInt64.20arithmetic/near/463428033

Should be combined with the version bump in #5089

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 390a9a63a24ca28306a60faa0381d4292d23af95 --onto 7845a05cf1094f24a5c4a51c32dd84bf4ff31a54. (2024-09-26 10:11:30)

[digama0]

While we're at it with the olean version bump, can we add a bit of data which explicitly indicates GMP-ness in the file? Also, it would be extremely useful to have the lean version string (i.e. v4.12.0-rc1) inside the file, with the field null or empty for custom, nightly, PR, fork toolchains. Right now the only version information available is the githash and this is useless for inequality queries.

[eric-wieser]

Such information could be used in digama0/oleandump#4, instead of the user having to tell oleandump which platform the oleans they are inspecting were built on.

[eric-wieser]

This is the hex-encoded git hash rather than the raw 20-byte SHA, right?

[digama0]

Yes. (I had a version of .lgz which parsed this and re-encoded it as a 20-byte sha, but it had invertibility issues in the case where there is something weird in this field.)

[digama0]

Thanks for adding the GMP flag. What are your thoughts on including the version information? (IIRC @eric-wieser also had a request for olean v2 but I forget what it is and it might be covered by my two requests.) If encoded as (4u8, 13u8, 0u8, 1u8) for v4.13.0-rc1 RCs with rc = 255 meaning the stable, then it can be done as pure lexicographic order, but encoding as a string is also an option which leaves more room for encoding unusual versions at the risk of underspecifying how version ordering should apply on these versions.

[eric-wieser]

Perhaps you're thinking of me talking about #2908? This would be a change to what ends up in the olean, but not one that breaks any downstream readers, so is orthogonal to any versioning.