Skip to content

fix: record instances unfolded by wrapInstance as shake dependencies#13579

Open
Kha wants to merge 3 commits intoleanprover:masterfrom
Kha:push-mrwrnvskyusz
Open

fix: record instances unfolded by wrapInstance as shake dependencies#13579
Kha wants to merge 3 commits intoleanprover:masterfrom
Kha:push-mrwrnvskyusz

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Apr 29, 2026

No description provided.

@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 Apr 29, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 29, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-29 17:40:48)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-01 17:17:49)

@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Apr 29, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 29, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Apr 29, 2026 •
edited
Loading

Mathlib CI status (docs):

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 1, 2026
Update lean-toolchain for leanprover/lean4#13579
a489a1b
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 1, 2026
Update lean-toolchain for leanprover/lean4#13579
0d7ec1b
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels May 1, 2026
@Kha Kha marked this pull request as ready for review May 4, 2026 15:13
@Kha Kha enabled auto-merge May 4, 2026 15:13
@Kha Kha mentioned this pull request May 5, 2026
Closed
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

backport releases/v4.30.0 breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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.

2 participants

@Kha @leanprover-bot