Stream: Coq devs & plugin devs

Topic: reduction in the kernel


view this post on Zulip 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:

  1. convert the type of the function to an fconstr, reduce it to an FProd (https://github.com/coq/coq/blob/master/kernel/typeops.ml#L195)
  2. convert the the type of the argument back to a constr (https://github.com/coq/coq/blob/master/kernel/typeops.ml#L199) and call conv_leq
    2.1 conv_leq checks syntactic equality and, if that fails,
    2.2 converts both arguments to an 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?

view this post on Zulip 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.)

view this post on Zulip Gregory Malecha (Sep 14 2022 at 23:19):

It makes sense. I could try to make a patch.

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Sep 15 2022 at 15:34):

make a PR and we can run it on the CI bench

view this post on Zulip Gregory Malecha (Sep 15 2022 at 15:37):

https://github.com/coq/coq/pull/16497

view this post on Zulip Gregory Malecha (Sep 15 2022 at 15:48):

thanks!

view this post on Zulip 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)

view this post on Zulip Gregory Malecha (Sep 15 2022 at 16:16):

Thanks @Pierre-Marie Pédrot

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 12:17):

Do we really have code that uses SProp?

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Sep 16 2022 at 12:42):

sprop schemes?

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 12:45):

I mean, something that can have some effect on the bench.

view this post on Zulip Gregory Malecha (Sep 16 2022 at 13:10):

The bench result doesn't seem to be due to sprop

view this post on Zulip Gregory Malecha (Sep 16 2022 at 13:10):

I've been talking with @Janno about the diff

view this post on Zulip 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

view this post on Zulip 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: May 31 2023 at 15:01 UTC