leanprover
chore: CI: build 64-bit platforms consistently with GMP
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
Mathlib CI status (docs):
- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase 390a9a63a24ca28306a60faa0381d4292d23af95 --onto 7845a05cf1094f24a5c4a51c32dd84bf4ff31a54. (2024-09-26 10:11:30)
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.
Such information could be used in https://github.com/digama0/oleandump/pull/4, instead of the user having to tell oleandump which platform the oleans they are inspecting were built on.
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.
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.
@digama0 I added a Lean version string field and hope this is now enough .olean metadata for the next decade :) . Could you take a look?
Mathlib CI status (docs):
- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase a167860e3b2a1236af3e989259f5badc04d50b8c --onto 3a34a8e0d119d8a907614af62b405d85149672f0. (2024-10-18 16:31:06) - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase 3450c2a8ac3a8c193d4fcc28056d0725ca3b4a1f --onto 4ee44ceb1d77f16b9b81bc655bc8b318cd6e8c4d. (2024-10-30 04:02:49) - ❗ Mathlib CI can not be attempted yet, as the
nightly-testing-2024-11-01tag does not exist there yet. We will retry when you push more commits. If you rebase your branch ontonightly-with-mathlib, Mathlib CI should run now. (2024-11-01 11:25:07)
Sorry for not sending my lgtm after your last message. I will get on implementing this in leangz.
My only comment here is whether we want to fix #2908 at the same time rather than bumping the olean version number twice.
My only comment here is whether we want to fix #2908 at the same time rather than bumping the olean version number twice.
I think #2908 can be fixed without a version bump, since the current implementation is nondeterministic anyway and this just resolves the nondeterminism. (But I agree that doing them at the same time is likely to result in less knock-on effects.)
Bumping the version means you can easily check whether you need to consider determinism when inspecting the file.
I won't worry about #2908 for now, given that it's only relevant for non-standard Lean builds now
Which milestone is this change set for? I want to make sure I release such that there are no unpatched lean versions between when leangz releases a new version and when the patch comes out in an RC or regular release of lean.
Oops, @Kha has sent this to the queue, but that won't work as it has stage0 updates.
I will rebase / redo stage0 now.
@digama0, I think if we merge in the next 24 hours, this will arrive in v4.14.0-rc1. Would that work for you for leangz?
I have a version of leangz I would like to test, but this PR has no working pr-release AFAICT
Okay, https://github.com/digama0/leangz/compare/olean2 seems to work based on a manually built lean executable using this PR. But I did notice one issue: Currently, manually built lean executables have the lean_version field set to e.g. 4.12.0, even though they are not official releases. Can we do something so that LEAN_VERSION_IS_RELEASE is also included in that field? I would like to be able to differentiate between official releases and unofficial ones (and correctly ordering official releases) without looking at the githash. cc: @Kha
Okay, https://github.com/digama0/leangz/compare/olean2 seems to work based on a manually built lean executable using this PR. But I did notice one issue: Currently, manually built lean executables have the
lean_versionfield set to e.g.4.12.0, even though they are not official releases. Can we do something so thatLEAN_VERSION_IS_RELEASEis also included in that field? I would like to be able to differentiate between official releases and unofficial ones (and correctly ordering official releases) without looking at the githash. cc: @Kha
Oof, this is not exactly your question, but I see that I have screwed up the last two months and not advanced the LEAN_VERSION_MINOR on master. (Updated in #5889.)
Note, to fix this issue I think it suffices to ensure that any non-official release has a lean_version string not matching the regex [0-9]+\.[0-9]+\.[0-9]+(-rc[0-9]+)?. For example, using the lean-toolchain name verbatim would work since it starts with a repo name. Other options include just leaving the field blank for these releases, or prefixing or suffixing with custom, etc.
The above strategy is the backward compatible one, we can do that at any time after releasing olean-v2. A non-backward compatible strategy we should do now or never is to add the LEAN_IS_RELEASE flag as a bit in the new flags bitfield of the olean.