I've been looking at the code of reduction in the kernel and it seems like when you type an application you:
fconstr
, reduce it to an FProd
(https://github.com/coq/coq/blob/master/kernel/typeops.ml#L195)constr
(https://github.com/coq/coq/blob/master/kernel/typeops.ml#L199) and call conv_leq
conv_leq
checks syntactic equality and, if that fails,fconstr
s and begins to reduce I'm wondering about the relationship between 2 and 2.2. it seems like the round-trip could be eliminated. If fconstr
is mutating to reduce terms, then not doing the round trip would maintain more sharing.
Does this make sense, or is there something that I am missing?
It makes sense, I think I was the one who wrote this precise piece of code (to prevent a quadratic blowup). I'm not sure how to do that without exposing messy bits of the reduction machine though, and it's easy to get this wrong. Also you'd lose the equality check and would have to resort to conversion always. (Not sure it matters.)
It makes sense. I could try to make a patch.
I managed to make a patch. It seems like the best evaluation metric is to get it to run on coq-bench?
make a PR and we can run it on the CI bench
https://github.com/coq/coq/pull/16497
thanks!
As commented in the PR I think you must remove the equality check from the fconstr variant to see any difference. Otherwise you're just doing the same thing as before (except you compute the conversion to constr twice in case of error)
Thanks @Pierre-Marie Pédrot
It seems like assert (!Flags.in_debugger)
is failing now. @Pierre-Marie Pédrot can you tell me what that is about and why there is a kernel assertion about it?
some fterms cannot be turned back into constr
in the debugger we still allow it producing some dummy variables for debug printing
Thanks @Gaëtan Gilbert ! I managed to work around the issue by removing the update
in skip_irrelevant_stack
. I believe, but can't quite figure it all out, that with the new code we get a lot more sharing and that sharing enables terms to be reduced in irrelevant context as well as used in relevant contexts which results in FIrrelevant
showing up in the final type of the application causing the fault.
Do we really have code that uses SProp?
(also, more sharing doesn't mean faster conversion. There are many cases where it's much faster to compare unreduced terms, but sharing forces the reduction across calls)
sprop schemes?
I mean, something that can have some effect on the bench.
The bench result doesn't seem to be due to sprop
I've been talking with @Janno about the diff
More sharing could result in slower conversions in some instances, I agree, but it seems like the opposite is more likely to me
One option is to still have the syntactic check but then to use the existing fconstr
if you fall back to a conversion check.
Last updated: May 31 2023 at 15:01 UTC