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: prevent compiler crash in casesOn optimization #6993

Closed
wants to merge 1 commit into from

Conversation

Rob23oba
Copy link
Contributor

@Rob23oba Rob23oba commented Feb 7, 2025

This PR fixes a crash in the old compiler during the casesOn reduction step in csimp.cpp where it incorrectly assumed that a constructor application within a casesOn would always belong to the inductive that the casesOn applies to.

Closes #6957

@Rob23oba Rob23oba requested a review from leodemoura as a code owner February 7, 2025 17:44
@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 Feb 7, 2025
@leanprover-community-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 a4ad409ae084218cb1170722884fce5b5664e7a3 --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-07 18:11:09)

@Kha
Copy link
Member

Kha commented Feb 12, 2025

Thank you for the PR! The old code generator has been frozen while @zwarich is working on the new one so I'm closing this PR. I'm looking forward to learning from Cameron whether Option.attach is even something we should allow in a sensible runtime type system :) .

@Kha Kha closed this Feb 12, 2025
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
Projects
None yet
Development

Successfully merging this pull request may close these issues.

using Option.attach can crash lean
3 participants