Do not consider scrutinees of projections and cases as heads for hint mode "!" #14392
Conversation
This file contains 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
4 tasks
|
I think this question came up before, about what the "head" of a primitive projection is. IMO it would make most sense that this be treated consistently (for mode
This sentence has too many negations for me to be able to parse it.^^ |
|
Hey, I have detected that there were CI failures at commit f4d758f without any failure in the test-suite. |
|
@coqbot ci minimize |
|
I have initiated minimization at commit f4d758f for the suggested target ci-perennial as requested. |
|
Error: Could not minimize file (from ci-perennial) (full log on GitHub Actions) build log (truncated to last 26KiB; full 2.1MiB file on GitHub Actions Artifacts under
|
|
Let's try again now that the base check has finished @coqbot ci minimize |
|
Said otherwise, in mode !, an index term of a constraint matches except if it is of the shape |
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/perennial/src/program_proof/examples/inode_proof.v (from ci-perennial) (full log on GitHub Actions) Minimized Coq File (truncated to 32KiB; full 45KiB file on GitHub Actions Artifacts under
|
|
@robbertkrebbers the perenial error seems to be related to iris succeding more with this patch. On goal: Σ: gFunctors
heapG0: heapG Σ
stagedG0: stagedG Σ
allocG0: allocG Σ
inodeN, allocN: namespace
k: nat
l: loc
k': nat
P: inode.t → iProp Σ
addr, off: u64
Q: option Block → iPropI Σ
H: (S k < k')%nat
Φ: val → iPropI Σ
Φc: iPropI Σ
σ: inode.t
mb: option Block
Hσ: mb = σ.(inode.blocks) !! int.nat off
s: Slice.t
1/1
"HQ" : Q mb
"Hblock" : match mb with
| Some b => is_block s 1 b
| None => ⌜s = Slice.nil⌝
end
--------------------------------------∗
match ?Goal with
| Some b => is_block s 1 b
| None => ⌜s = Slice.nil⌝
end ∗ Q ?Goal
...
"Hblock" : match mb with
| Some b => is_block s 1 b
| None => ⌜s = Slice.nil⌝
end
--------------------------------------∗
match mb with
| Some b => is_block s 1 b
| None => ⌜s = Slice.nil⌝
endand require an explicit `iApply "Hblock" |
|
Yep, it's easy to fix perennial in a compatible way. |
|
I don't have a strong opinion on whether this works or not, and I find it hard to judge the larger consequences of this change. Seems fine for me otherwise. |
|
This generally allows to perform dependent resolution with instances of the shape |
|
I've started the bench to check this doesn't negatively impact performance. |
|
Hey, I have detected that there were CI failures at commit 3c8378b without any failure in the test-suite. |
mattam82
force-pushed
the
nohead-evar-application-head
branch
from
3c8378b to
3cd0858
Compare
|
Perennial should now work, the fixes are now on the |
|
Yep, this one should be all green, I removed the overlay |
|
I only pushed the fixes from master to |
jfehrle
reviewed
May 27, 2021
doc/changelog/02-specification-language/14392-nohead-evar-application-hea.rst
Outdated
Show resolved
Hide resolved
|
Good @coq/tactics-maintainers , please review now. |
mattam82
force-pushed
the
nohead-evar-application-head
branch
from
5b92e54 to
1a195b8
Compare
|
I rebased, but did not change anything |
Update doc/sphinx/proofs/automatic-tactics/auto.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Update doc/changelog/02-specification-language/14392-nohead-evar-application-hea.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Update doc/sphinx/proofs/automatic-tactics/auto.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
mattam82
force-pushed
the
nohead-evar-application-head
branch
from
1a195b8 to
a30289e
Compare
2 tasks
ppedrot
approved these changes
May 28, 2021
|
To be honest: I think this MR makes the behavior more uniform, hence less of a headless duck. |
|
Hey, I have detected that there were CI failures at commit a30289e without any failure in the test-suite. |
|
@mattam82 did you run a bench? I can't find it in the (notoriously cumbersome) gitlab UI. Also, if you want this to go into 8.14 it needs to be merged asap. |
|
Hey, I have detected that there were CI failures at commit a30289e without any failure in the test-suite. |
|
I triggered a bench, it's easy: just go to the bench job on the gitlab ci pipeline details link and "trigger manual action" |
|
Also, historical note: @ppedrot you were the one who added the |
SkySkimmer
changed the title
|
https://gitlab.com/coq/coq/-/jobs/1301186577 |
|
If nobody complains I will merge this tonight so as to fit into the release schedule. |
ppedrot
added
the
kind: enhancement
This was referenced Oct 26, 2021
Open
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This reverts a change that made
Proj (p, ?X)andmatch ?X withnot be considered as not headed by evars for matching a hint mode. Experience shows (e.g. in Iris) that these partial terms can usefully be considered as indices in proof search. Now, only ?X u1 ... un is considered headed by an evar.Kind: feature
https://github.com/coq/coq/blob/master/dev/ci/user-overlays/README.md for details)