Fixes #19661: incorrect reduction of inner fixpoints with extra arguments in fixpoint guard checker#19671
Merged
coqbot-app[bot] merged 2 commits intorocq-prover:masterfrom Oct 15, 2024
Conversation
coqbot-app
bot
added
the
needs: full CI
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Oct 9, 2024
jfehrle
reviewed
Oct 9, 2024
doc/changelog/01-kernel/19671-master+fix19661-guard-with-uniform-parameters.rst
Outdated
Show resolved
Hide resolved
Member
|
@herbelin the first commit has nothing to do with the sauerkraut. |
Member
Author
On second thought, the bug seems kernel-safe. Basically, what the bug does is to reduce |
herbelin
added
part: kernel
part: fixpoints
…tch. Commit 140908d (PR rocq-prover#17986, about the extrusion of uniform parameters) was passing the wrong extra arguments of a match.
herbelin
added
the
request: full CI
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Oct 10, 2024
herbelin
force-pushed
the
master+fix19661-guard-with-uniform-parameters
branch
from
266f95c to
73a6319
Compare
coqbot-app
bot
removed
request: full CI
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+fix19661-guard-with-uniform-parameters
branch
from
73a6319 to
b9e6960
Compare
coqbot-app
bot
removed
the
request: full CI
herbelin
changed the title
ppedrot
approved these changes
Oct 12, 2024
Member
ppedrot
left a comment
ppedrot
left a comment
There was a problem hiding this comment.
Probably fine, as the new code does seem to correspond to the intended semantics. Nonetheless this is the guard condition so as usual fine prints may apply.
Member
|
I'm leaving a bit of time for other kernel experts to weigh in. |
Member
|
@coqbot merge now |
proux01
pushed a commit
to proux01/rocq
that referenced
this pull request
Oct 16, 2024
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> (cherry picked from commit b9e6960)
proux01
added a commit
to proux01/rocq
that referenced
this pull request
Oct 16, 2024
…uction of inner fixpoints with extra arguments in fixpoint guard checker
proux01
added a commit
to proux01/rocq
that referenced
this pull request
Oct 17, 2024
…uction of inner fixpoints with extra arguments in fixpoint guard checker
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Was introduced in 140908d, PR #17986, 8.20.0.
Fixes / closes #19661
The original report raises an anomaly
but it is not excluded that the bug allows to bypass the guard condition without failing (one would need two nested beta-redexes across aand seems otherwise kernel-safe (see next comment).match, each respectively on an argument in the same inductive type, one having a well-founded body, the other not, and the first one being wrongly used in place of the second one or something like that).