Fix #5351: Intuition does not work with universe polymorphism. #8905
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
coqbot
added
the
needs: rebase
coqbot
removed
the
needs: rebase
|
Why not expose |
|
I am not super fond of globally exporting tactics. I know this is the current model but this should be pondered seriously. |
|
Another advantage is that this PR is backportable as-is. |
|
Failures are spurious. I'll rebase this PR when the fiat fix lands. |
|
Benchmark show an observable slowdown on some developments: This is not good... And it also forecasts a bigger slowdown if we change Ltac non-linear variable matching to universe-unifying conversion. |
Maybe this is a good use case for an attribute on the match? |
Ltac match is already quite complex in its own right, it has a quite a combinatorics: multi / lazy / nothing, reverse / nothing... I was more in favour of deprecating non-linear matching, as there are too many possible interpretations, i.e. about as many as there are notions of equalities on terms. (Also, this is Ltac, so there are no attributes in there. Yet.) |
mattam82
reviewed
Nov 16, 2018
theories/Init/Tauto.v
Outdated
| (* generalize (id0 id1); intro; clear id0 does not work | ||
| (see Marco Maggiesi's BZ#301) | ||
| so we instead use Assert and exact. *) | ||
| is_conv X1 X3; |
There was a problem hiding this comment.
I believe you're hitting this because you replaced a syntactic equality test by a conversion (the strategy is different in constr_matching and tactic_matching). I guess you could recover compatibility and performance by also exporting a constr_eq, I guess using it in axioms above.
There was a problem hiding this comment.
I don't think so, all of the equalities here are performed by conversion because they live in tactic_matching. Actually I first tried to use a syntactic equality and it broke in the stdlib because some part of the code was relying on conversion.
There was a problem hiding this comment.
Ah right, we call extended_matches on the conclusion and use conversion in tactic_matching to related the two instances of the meta. So the "specific" case using constr_eq is only for non-linear occurrences in the goal if I'm not mistaken.
There was a problem hiding this comment.
In non-linear occurrences from the same hypothesis as well, also, but indeed.
|
@mattam82 The reason why it is slower is really that we perform universe unification instead of mere syntactic equality during conversion. It's common knowledge that |
|
Ah, I didn't realize you were calling universe unification here and not just conversion with inference of constraints, i.e. just adding a bit of inference compared to what Reductionops.is_conv in tactic_matching is doing. Did you try calling Reduction.infer_conv instead, which avoids the mumbo-jumbo with algebraics/flexibles etc? |
|
@mattam82 If we do that, don't we just sidestep the bug? Like, what's the reason we use the universe-unifying conversion elsewhere and don't go directly for |
|
Tactics.convert is just a wrapper around infer_conv. |
|
So there is no way out? |
|
No way out unless the slowdown is about some different backtracking
behaviour / cost of enter / some other universe unrelated thing
Gaëtan Gilbert
…On 17/11/2018 13:19, Pierre-Marie Pédrot wrote:
So there is no way out?
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#8905 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/ACWQ7I6H5givTwzisqgBU1A2Ms3Sgtueks5uv_7DgaJpZM4YOVWg>.
|
|
According to my experiments this was really due to the call on universe processing, so I guess we're fried. What do? |
SkySkimmer
reviewed
Nov 17, 2018
theories/Init/Tauto.v
Outdated
| (* generalize (id0 id1); intro; clear id0 does not work | ||
| (see Marco Maggiesi's BZ#301) | ||
| so we instead use Assert and exact. *) | ||
| is_conv X1 X3; | ||
| assert X2; [exact (id0 id1) | clear id0] |
There was a problem hiding this comment.
What happens if we don't check convertibility and just let it fail when it tries to exact id0 id1?
There was a problem hiding this comment.
Probably going to be worse performance-wise because now you call full-blown unification. Fast failure matters a lot.
|
It's a bit tricky indeed: Tactics.convert wraps Reductionops.infer_conv which calls universe unification while Reduction.infer_conv has a simpler universe inference (the one used by module subtyping). The main difference between the two if that Reductionops calls process_universe_constraints directly so it can handle algebraics and flexible universe variables that appear during typechecking, keeping universe equality information in the UState structure while Reduction.infer_conv does not care about this and just generates constraints. However to put these constraints in the Evd you'd have to go through process_universe_constraints again, so I guess there would be no difference. The only way to improve performance would be to optimize process_universe_constraints/the uState to avoid maintaining the substitution separately from the graph. I don't see immediately how to do that while maintaining the algebraic universe support, but it can maybe be done: one needs to be able to instantiate a universe variable |
github-actions
bot
added
the
needs: rebase
coqbot-app
bot
added
needs: full CI
|
@coqbot bench |
|
🏁 Bench results: INFO: failed to install coq-vst 🐢 Top 25 slow downs🐇 Top 25 speed ups |
ppedrot
added
the
request: full CI
coqbot-app
bot
removed
request: full CI
|
@coqbot bench |
|
🏁 Bench results: INFO: failed to install coq-iris-examples 🐢 Top 25 slow downs🐇 Top 25 speed ups |
|
My last trick to reduce the slowdown seems to have worked. I prevent generating gazillions of case analysis by hardcoding in the exposed OCaml tactic the behaviour of the corresponding match goal rule. |
Instead of using non-linear pattern-matching in tauto, we use a tauto-specific conversion function so as to add the missing universe constraints. We cannot use constr_eq as the current implementation of non-linear matching uses conversion rather than syntactic equality.
Instead of doing it in the branch after having pattern-matched on types that look like functions, we perform the match directly within the built-in primitive. Hopefully this should cut many trivial branches in match goal.
ppedrot
added
request: full CI
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
approved these changes
Mar 18, 2023
|
@coqbot merge now |
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.
Instead of using non-linear pattern-matching in tauto, we use a tauto-specific conversion function so as to add the missing universe constraints. We cannot use constr_eq as the current implementation of non-linear matching uses conversion rather than syntactic equality.
Fixes / closes #4721.
Fixes / closes #5351.