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

fix: export symbols needed by Verso #4884

Merged

Conversation

david-christiansen
Copy link
Contributor

Verso needed a symbol that was unexported - this exposes it again.

@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 Jul 31, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6a4159c4a792ed2e74f20aecf73974dc3e314e2c --onto 8acdafd5b3957382c02779ada451c14da44e2aca. (2024-07-31 13:52:34)

@kim-em kim-em added the will-merge-soon …unless someone speaks up label Jul 31, 2024
@kim-em
Copy link
Collaborator

kim-em commented Jul 31, 2024

No opinion on the solution, but unless someone objects I will make sure this is in in time for v4.11.0-rc1.

@david-christiansen david-christiansen added this pull request to the merge queue Aug 1, 2024
@david-christiansen
Copy link
Contributor Author

Thanks! We should do a stage0 update before rc1 as well, because otherwise Verso will only work on stage2 builds from master (the exported symbols are determined by the prior stage's compiler).

Merged via the queue into leanprover:master with commit 32b9de8 Aug 1, 2024
14 checks passed
@david-christiansen david-christiansen deleted the unbreak-subverso branch August 1, 2024 06:42
@david-christiansen
Copy link
Contributor Author

Stage0 update triggered.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
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.

3 participants