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.

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

Move the static check of evaluability in unfold tactic to runtime. #12256

Merged
merged 6 commits into from
May 14, 2020
Merged

Move the static check of evaluability in unfold tactic to runtime. #12256

merged 6 commits into from
May 14, 2020

Conversation

ppedrot
Copy link
Member

@ppedrot ppedrot commented May 5, 2020 •
edited
Loading

See #11840 for a motivation. I had to fix Floats.FloatLemmas because it uses the same name for a notation and a term, and the fact this unfold was working on this was clearly a bug. I hope nobody relies on this kind of stuff in the wild.

Depends on #12254.

Fixes #5764: "Cannot coerce ..." should be a runtime error.
Fixes #5159: "Cannot coerce ..." should not be an error.
Fixes #4925: unfold gives error on Admitted.
Fixes #11727: documentation lies about example tactic notation taking a reference.

@ppedrot ppedrot added kind: fix This fixes a bug or incorrect documentation. needs: merge of dependency This PR depends on another PR being merged first. labels May 5, 2020
@ppedrot ppedrot added this to the 8.12+beta1 milestone May 5, 2020
@ppedrot ppedrot requested review from a team as code owners May 5, 2020 15:02
@herbelin herbelin self-assigned this May 5, 2020
@ppedrot ppedrot mentioned this pull request May 8, 2020
Merged
2 tasks
@ppedrot ppedrot force-pushed the unfold-dyn-check branch 2 times, most recently from 424d10f to 3e7ee00 Compare May 8, 2020 14:12
@ppedrot
Copy link
Member Author

ppedrot commented May 8, 2020 •
edited
Loading

Unfortunately, it seems that many developments in the CI rely on the design pattern of Notation foo := foo arg1 ... argn to override a constant with its application. I think it's probably better w.r.t. backwards-compatibility that as a special case, interp_global_reference extracts the head of an applied constant when the argument is a syntactic notation. I'll tweak the PR accordingly.

@ppedrot ppedrot requested review from a team as code owners May 8, 2020 14:35
@ppedrot
Copy link
Member Author

ppedrot commented May 8, 2020

Let's see how it fares now.

@ppedrot
Copy link
Member Author

ppedrot commented May 8, 2020

This seems much better, now the CI passes fully, much to my surprise...

herbelin
herbelin approved these changes May 9, 2020
View reviewed changes
Copy link
Member

@herbelin herbelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's indeed concise.

I think it's probably better w.r.t. backwards-compatibility that as a special case, interp_global_reference extracts the head of an applied constant when the argument is a syntactic notation.

OK

I would also suggest to add also the example from #11727.

The refman would have to be changed, but that can be continued in #11840.

test-suite/bugs/closed/bug_4925.v
@@ -0,0 +1,6 @@
Axiom a: bool.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Ltac unfold_ x := unfold x.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this go into another, different test?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, it can.

test-suite/bugs/closed/bug_4925.v

Goal a = true.
Proof.
try unfold a.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
try unfold a.
try unfold a.
try unfold_ a.

plugins/ltac/tacintern.ml Outdated Show resolved Hide resolved
@Zimmi48 Zimmi48 removed the needs: merge of dependency This PR depends on another PR being merged first. label May 12, 2020
@Zimmi48
Copy link
Member

Zimmi48 commented May 12, 2020

It looks like both the refman and the test-suite are broken.

@Zimmi48 Zimmi48 added the needs: fixing The proposed code change is broken. label May 12, 2020
@ejgallego
Copy link
Member

test-suite are broken.

Test-suite failure seems due to the with_strategy PR.

@JasonGross
Copy link
Member

Indeed, there's probably some "this thing should work but it fails" line in one of the with_strategy tests that this PR makes work, and the solution should just be to remove the relevant Fail (and the comment before it, if there is one).

@herbelin herbelin mentioned this pull request May 12, 2020
Closed
3 tasks
@ppedrot ppedrot requested a review from a team as a code owner May 13, 2020 08:18
@ppedrot
Copy link
Member Author

ppedrot commented May 13, 2020

Indeed there were tests and documentation introduced by @JasonGross precisely about the limitations of unfold internalization. I've tweaked the former and removed the latter.

@Zimmi48 Zimmi48 removed the needs: fixing The proposed code change is broken. label May 13, 2020
@ppedrot
Copy link
Member Author

ppedrot commented May 13, 2020

The offending developments have passed, this seems ready.

@ejgallego
Copy link
Member

Just relaunched VST just in case.

JasonGross
JasonGross previously requested changes May 13, 2020
View reviewed changes
doc/sphinx/proof-engine/tactics.rst Show resolved Hide resolved
test-suite/success/with_strategy.v Outdated Show resolved Hide resolved
@ppedrot ppedrot force-pushed the unfold-dyn-check branch 2 times, most recently from a0350d3 to ee9dcff Compare May 13, 2020 14:31
@ppedrot
Copy link
Member Author

ppedrot commented May 13, 2020

@JasonGross done.

@JasonGross JasonGross dismissed their stale review May 13, 2020 14:45

Requested changes made, thanks!

@ppedrot
Move the static check of evaluability in unfold tactic to runtime.
be56f39 
See coq#11840 for a motivation. I had to fix Floats.FloatLemmas because
it uses the same name for a notation and a term, and the fact this
unfold was working on this was clearly a bug. I hope nobody relies
on this kind of stuff in the wild.

Fixes coq#5764: "Cannot coerce ..." should be a runtime error.
Fixes coq#5159: "Cannot coerce ..." should not be an error.
Fixes coq#4925: unfold gives error on Admitted.
@ppedrot
Generalize the interpretation of syntactic notation as reference to t…
3af3409 
…heir head.

This seems to be a pattern used quite a bit in the wild, it does not hurt
to be a bit more lenient to tolerate this kind of use. Interestingly the
API was already offering a similar generalization in some unrelated places.

We also backtrack on the change in Floats.FloatLemmas since it is an instance
of this phenomenon.
@ppedrot
Add test for coq#11727, which was indirectly fixed by this PR.
2e53445
@ppedrot
Tweak the error message of reference internalization.
5e1da5b
@ppedrot
Remove an outdated piece of documentation about limitations of unfold.
ec14db8
@ppedrot
Adding changelog.
b5ecd2e
@ppedrot
Copy link
Member Author

ppedrot commented May 14, 2020

@herbelin I've added a changelog, this is ready.

@herbelin
Copy link
Member

OK, will merge tonight.

@herbelin herbelin merged commit 56e2384 into coq:master May 14, 2020
@ppedrot ppedrot deleted the unfold-dyn-check branch May 14, 2020 19:55
@herbelin herbelin mentioned this pull request Jul 15, 2020
Merged
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@herbelin herbelin herbelin approved these changes

@JasonGross JasonGross JasonGross left review comments

Assignees

@herbelin herbelin

Labels
kind: fix This fixes a bug or incorrect documentation.
Projects
None yet
Milestone
8.12+beta1
5 participants
@ppedrot @Zimmi48 @ejgallego @JasonGross @herbelin