Skip to content

fix: keep wrapInstance mvar-free#13346

Merged
Kha merged 4 commits intoleanprover:masterfrom
Kha:push-munttqmntqry
Apr 13, 2026
Merged

fix: keep wrapInstance mvar-free#13346
Kha merged 4 commits intoleanprover:masterfrom
Kha:push-munttqmntqry

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Apr 9, 2026 •
edited
Loading

Ensure fresh instance mvars are resolved by inferInstanceAs before calling into wrapInstance

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

leanprover-bot commented Apr 9, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-07 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-09 14:12:37)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-10 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-10 16:22:21)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 9, 2026
Update lean-toolchain for testing leanprover/lean4#13346
246cb7b
@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 9, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 9, 2026
Update lean-toolchain for testing leanprover/lean4#13346
7f29606
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 9, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 9, 2026

Mathlib CI status (docs):

@Kha Kha force-pushed the push-munttqmntqry branch from 91e7769 to 54cbded Compare April 9, 2026 15:53
@Kha Kha force-pushed the push-munttqmntqry branch from 54cbded to b81b581 Compare April 9, 2026 15:54
@Kha Kha added the changelog-no Do not include this PR in the release changelog label Apr 9, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 9, 2026
Update lean-toolchain for leanprover/lean4#13346
950affb
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 9, 2026
Update lean-toolchain for leanprover/lean4#13346
7dae754
@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 Apr 9, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 9, 2026

Mathlib CI status (docs):

@Kha Kha changed the base branch from master to nightly-with-mathlib April 10, 2026 13:48
@Kha Kha changed the title fix: keep wrapInstance mvar-free [REBASED] fix: keep wrapInstance mvar-free Apr 10, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 10, 2026

Mathlib CI status (docs):

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13346
a46a330
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13346
9b1fae7
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Apr 10, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 10, 2026

Mathlib CI status (docs):

@Kha Kha changed the base branch from nightly-with-mathlib to master April 10, 2026 19:13
@Kha Kha changed the title [REBASED] fix: keep wrapInstance mvar-free fix: keep wrapInstance mvar-free Apr 10, 2026
@Kha Kha marked this pull request as ready for review April 10, 2026 19:14
@Kha Kha force-pushed the push-munttqmntqry branch from 077164e to 812c173 Compare April 10, 2026 19:14
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13346
3244daa
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13346
f48d5bb
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 10, 2026

Mathlib CI status (docs):

@Kha Kha enabled auto-merge April 13, 2026 07:53
@Kha Kha added this pull request to the merge queue Apr 13, 2026
Merged via the queue into leanprover:master with commit ff19ad9 Apr 13, 2026
17 checks passed
@Kha Kha deleted the push-munttqmntqry branch April 13, 2026 09:14
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

builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog 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