Cache the relevance flag in rel contexts in an efficient way. #11152
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
|
Also, @SkySkimmer next time you use lists for an access-based data structure, you'll be publicly whipped against the Wall of Complexity™. |
|
Maybe worth resurrecting the question of how to add regression tests for complexity? |
|
Here is a less invasive version that relies on a somewhat hidden invariant of the reduction machine: every rel variable known in the context of the fconstr creation is static, and only those introduced after are handled in an untyped way. Thus we simply reuse the environment to check irrelevance of I wouldn't mind somebody double-checking my DeBruijn mangling though, we've been bitten enough times never to be overly cautious... |
ppedrot
added
kind: fix
|
(If people are fine with this variant I'll squash before merging.) |
SkySkimmer
approved these changes
Nov 21, 2019
|
I am running a bench, just in case: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/806/. |
@ppedrot can this invariant and the dependence be documented? I'm assuming this is what justifies using the empty range in some places, but that's a total guess on my part and I can imagine someone coming in and thinking it's suspicious and not realizing it's okay because of this invariant. (Or breaking this invariant and being confused.) I think dropping the text you already wrote in a comment in a relevant place would already be much better than nothing. |
|
This invariant is not specific to the irrelevance marks. I think we can document it somehow, even though I have no idea about the actual invariants of the conversion machine. We do seem to be preserving that global rels are compiled to (To give a terrifying example, conversion does not preserve the fact that the two terms being compared have a common supertype. This is close from preventing me to sleep at night.) |
Rels that exist inside the environment at the time of the closure creation are fetched in the global environment, while we only use the local list of relevance for FRels. All the infrastructure was implicitly relying on this kind of behaviour before the introduction of SProp. Fixes coq#11150: pattern is 10x slower in Coq 8.10.0
|
Bench said |
|
The bench seems to show the impact of the PR is noise. @JasonGross where is the code that got slower? Is there a opam package to test? |
|
No opam package. I could probably bring https://github.com/mit-plv/reification-by-parametricity up to date and add it to the CI and opam; it's a bunch of performance benchmarks. As far as I know there is no significant use of this code in the wild, at present. The two bug reports have small examples though. |
|
(FTR, I consider this ready.) |
SkySkimmer
added a commit
to SkySkimmer/coq
that referenced
this pull request
Nov 24, 2019
…ficient way. Reviewed-by: SkySkimmer
1 task
ppedrot
added a commit
to ppedrot/coq
that referenced
this pull request
Nov 25, 2019
… efficient way.
ppedrot
added a commit
to ppedrot/coq
that referenced
this pull request
Nov 25, 2019
… efficient way.
coqbot
moved this from Request 8.11+beta1 inclusion
to Shipped in 8.11+beta1
in Coq 8.11
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.
Fixes #11150: pattern is 10x slower in Coq 8.10.0
No test because performance tests suck in our infrastructure, but see @JasonGross's proposal.
Fixes #6502