Skip to content

chore: follow up on #8173 post-stage0 update #8722

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.

Sign up for GitHub

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

Jump to bottom
Merged
david-christiansen merged 1 commit into from
Jun 16, 2025
Merged

chore: follow up on #8173 post-stage0 update #8722

david-christiansen merged 1 commit into from
Jun 16, 2025

Conversation

@david-christiansen
Copy link
Contributor

@david-christiansen david-christiansen commented Jun 11, 2025

This PR un-does the temporary changes made in #8173 for bootstrapping purposes.

@david-christiansen david-christiansen added the changelog-no Do not include this PR in the release changelog label Jun 11, 2025
@david-christiansen
Copy link
Contributor Author

david-christiansen commented Jun 11, 2025

@Rob23oba This was the extent of the post-stage0-update changes, right?

@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 Jun 11, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jun 11, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 551e755d231b405ee79a8c4b5b525b28facb1f71 --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-11 12:24:57)

@Rob23oba
Copy link
Contributor

Rob23oba commented Jun 11, 2025

Yes, if these are all occurrences of private def init.

@david-christiansen david-christiansen added this pull request to the merge queue Jun 16, 2025
Merged via the queue into leanprover:master with commit 8ed6824 Jun 16, 2025
19 checks passed
algebraic-dev pushed a commit to algebraic-dev/lean4 that referenced this pull request Jun 18, 2025
@david-christiansen @algebraic-dev
chore: follow up on leanprover#8173 post-stage0 update (leanprover#8722)
74c5a8d 
This PR un-does the temporary changes made in leanprover#8173 for bootstrapping
purposes.
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 24, 2025
@david-christiansen @wkrozowski
chore: follow up on leanprover#8173 post-stage0 update (leanprover#8722)
bab59ac 
This PR un-does the temporary changes made in leanprover#8173 for bootstrapping
purposes.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

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

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@david-christiansen @leanprover-community-bot @Rob23oba