Skip to content
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: tag prerelease builds with -pre #5943

Merged
merged 2 commits into from
Nov 6, 2024
Merged

Conversation

Kha
Copy link
Member

@Kha Kha commented Nov 4, 2024

No description provided.

@digama0
Copy link
Collaborator

digama0 commented Nov 4, 2024

Could you expand the comment in module.cpp for olean_header::lean_version to mention the string formats one can expect for normal and prerelease versions? My understanding is that legal values include 4.13.0, 4.13.0-rc1 and 4.13.0-rc2-pre, and I'm not sure where the nightly-2024-10-18 part gets involved in the version string (is the comment correct?). In particular, the version string contains neither the leading v nor the leanprover/lean4: repo marker used in elan toolchain names.

if (std::strlen(LEAN_SPECIAL_VERSION_DESC) > 0) {
out << "-" << LEAN_SPECIAL_VERSION_DESC;
}
out << LEAN_VERSION_STRING;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe this is just future proofing, but as written I think g_short_version_string is unneeded since it is equivalent to the compile time constant LEAN_VERSION_STRING.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 4, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 4, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 4, 2024
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 4, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 4, 2024

Mathlib CI status (docs):

@Kha Kha added the will-merge-soon …unless someone speaks up label Nov 5, 2024
@Kha
Copy link
Member Author

Kha commented Nov 5, 2024

Could you expand the comment in module.cpp for olean_header::lean_version to mention the string formats one can expect for normal and prerelease versions? My understanding is that legal values include 4.13.0, 4.13.0-rc1 and 4.13.0-rc2-pre, and I'm not sure where the nightly-2024-10-18 part gets involved in the version string (is the comment correct?). In particular, the version string contains neither the leading v nor the leanprover/lean4: repo marker used in elan toolchain names.

I added a bit. In particular, -rc2-pre is not an option.

is the comment correct?

You could test it!

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 5, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 5, 2024
@Kha Kha added this pull request to the merge queue Nov 6, 2024
Merged via the queue into leanprover:master with commit 345ecd2 Nov 6, 2024
16 checks passed
@Kha Kha deleted the push-lwnlpstmmozl branch November 7, 2024 12:04
@kim-em kim-em added the changelog-no Do not include this PR in the release changelog label Jan 4, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants