Gregory Malecha (Sep 14 2022 at 20:32): Gregory Malecha (Sep 14 2022 at 20:32):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_leqconv_leq checks syntactic equality and, if that fails,fconstrs 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?
Pierre-Marie Pédrot (Sep 14 2022 at 20:39):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.)
Gregory Malecha (Sep 14 2022 at 23:19):It makes sense. I could try to make a patch.
Gregory Malecha (Sep 15 2022 at 15:11):I managed to make a patch. It seems like the best evaluation metric is to get it to run on coq-bench?
Gaëtan Gilbert (Sep 15 2022 at 15:34):make a PR and we can run it on the CI bench
Gregory Malecha (Sep 15 2022 at 15:37):https://github.com/coq/coq/pull/16497
Gregory Malecha (Sep 15 2022 at 15:48):thanks!
Pierre-Marie Pédrot (Sep 15 2022 at 16:00):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)
Gregory Malecha (Sep 15 2022 at 16:16):Thanks @Pierre-Marie Pédrot
Gregory Malecha (Sep 15 2022 at 17:20):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?
Gaëtan Gilbert (Sep 15 2022 at 17:26):some fterms cannot be turned back into constr
in the debugger we still allow it producing some dummy variables for debug printing
Gregory Malecha (Sep 16 2022 at 11:36):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.
Pierre-Marie Pédrot (Sep 16 2022 at 12:17):Do we really have code that uses SProp?
Pierre-Marie Pédrot (Sep 16 2022 at 12:17):(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)
Gaëtan Gilbert (Sep 16 2022 at 12:42):sprop schemes?
Pierre-Marie Pédrot (Sep 16 2022 at 12:45):I mean, something that can have some effect on the bench.
Gregory Malecha (Sep 16 2022 at 13:10):The bench result doesn't seem to be due to sprop
Gregory Malecha (Sep 16 2022 at 13:10):I've been talking with @Janno about the diff
Gregory Malecha (Sep 16 2022 at 13:21):More sharing could result in slower conversions in some instances, I agree, but it seems like the opposite is more likely to me
Gregory Malecha (Sep 16 2022 at 13:31):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: Dec 05 2023 at 11:01 UTC