chore: CI: build 64-bit platforms consistently with GMP #5144
Conversation
Kha
added
the
release-ci
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
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. |
|
Such information could be used in digama0/oleandump#4, instead of the user having to tell |
src/library/module.cpp
Outdated
| false; | ||
| #endif | ||
| bool:7 unused = 0; | ||
| // 41 bytes: build githash, padded with `\0` to the right |
There was a problem hiding this comment.
This is the hex-encoded git hash rather than the raw 20-byte SHA, right?
There was a problem hiding this comment.
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.)
|
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 |
|
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):
|
|
@digama0 @eric-wieser Final Comment Period :) |
|
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. |
| // e.g. "4.12.0-nightly-2024-10-18" | ||
| char lean_version[33]; | ||
| // 81b008650766442a0dfa9faa796e4588c9d7d3a1 | ||
| // 40 bytes: build githash, padded with `\0` to the right |
There was a problem hiding this comment.
There is no padding here, right?
There was a problem hiding this comment.
There can be, if the githash is empty. I don't think there is anything syntactically restricting it to be exactly 40 bytes, although it will be for actual lean releases.
| // address at which the beginning of the file (including header) is attempted to be mmapped | ||
| size_t base_addr; | ||
| // payload, a serialize Lean object graph; `size_t` has same alignment requirements as Lean objects | ||
| size_t data[]; | ||
| }; | ||
| // make sure we don't have any padding bytes, which also ensures `data` is properly aligned | ||
| static_assert(sizeof(olean_header) == 5 + 1 + 42 + sizeof(size_t), "olean_header must be packed"); | ||
| static_assert(sizeof(olean_header) == 5 + 1 + 1 + 33 + 40 + sizeof(size_t), "olean_header must be packed"); |
There was a problem hiding this comment.
Perhaps worth having an static_assert(offsetof(olean_header,data) % 40 == 0) or whatever the actual alignment requirements are.
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. |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
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. |
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