Skip to content

chore: add an assertion about mkValueTypeClosure #10954

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
nomeata merged 1 commit into from
Oct 25, 2025
Merged

chore: add an assertion about mkValueTypeClosure #10954

nomeata merged 1 commit into from
Oct 25, 2025

Conversation

@eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Oct 25, 2025 •
edited
Loading

This is a guard against #10705; if a kernel error is raised when the return value of this function is eventually checked, it is often silenced downstream, making it hard to spot the failure.
If we panic here via assert!, then the diagnostic cannot be missed.

@eric-wieser eric-wieser mentioned this pull request Oct 25, 2025
Closed
@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 Oct 25, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 25, 2025

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-10-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-25 12:17:26)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 25, 2025

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-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. (2025-10-25 12:17:28)

@nomeata nomeata added this pull request to the merge queue Oct 25, 2025
Merged via the queue into leanprover:master with commit b3ef7c9 Oct 25, 2025
22 checks passed
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Oct 27, 2025
@eric-wieser @wkrozowski
chore: add an assertion about mkValueTypeClosure (leanprover#10954)
0792220 
This is a guard against leanprover#10705; if a kernel error is raised when the
return value of this function is eventually checked, it is often
silenced downstream, making it hard to spot the failure.
If we panic here via `assert!`, then the diagnostic cannot be missed.
kim-em pushed a commit that referenced this pull request Oct 27, 2025
@eric-wieser @kim-em
chore: add an assertion about mkValueTypeClosure (#10954)
bf910a2 
This is a guard against #10705; if a kernel error is raised when the
return value of this function is eventually checked, it is often
silenced downstream, making it hard to spot the failure.
If we panic here via `assert!`, then the diagnostic cannot be missed.
@nomeata nomeata mentioned this pull request Oct 29, 2025
Merged
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

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.

4 participants

@eric-wieser @leanprover-community-bot @leanprover-bot @nomeata