-
Notifications
You must be signed in to change notification settings - Fork 415
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
chore: CI: build 64-bit platforms consistently with GMP #5144
base: master
Are you sure you want to change the base?
Conversation
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is the hex-encoded git hash rather than the raw 20-byte SHA, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There is no padding here, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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