Stream: MetaCoq

Topic: Make MetaCoq Run use a different reduction strategy

Lennard Gäher (Dec 13 2020 at 13:33):

Hi, is there some way to make MetaCoq Run use a different (less lazy) reduction strategy?
I'm in a situation where I need to debug a large chunk of plugin code and want to get out a pretty-printed version of a term from a deeply-nested function call. For anything of interest to me, the MetaCoq Run then diverges (taking up ~20GB of RAM after barely two minutes). It seems like this is due to the pretty-printing never being evaluated and thus the unevaluated thing with huge global & local environment representations gets returned (and probably the evaluation doesn't make reasonable use of sharing so the representation gets copied around all the time when returning from the many nested calls).

Do I need to look at run_template_monad.ml for that?

Edit: I just realized that I should probably just wrap what I'm doing in a tmEval before using it. However, it turns out that everything other than lazy is much too slow for even simpler things, so I'm probably looking for some magical reduction strategy which just doesn't exist :)

Matthieu Sozeau (Dec 14 2020 at 12:56):

You might have some luck using the "reduction effects" plugin allowing to put debug code anywhere in a Coq term: https://github.com/coq-community/reduction-effects

Matthieu Sozeau (Dec 14 2020 at 12:58):

You might also "force" evaluation order sometimes using CPS

Lennard Gäher (Dec 15 2020 at 14:05):

Matthieu Sozeau said:

You might have some luck using the "reduction effects" plugin allowing to put debug code anywhere in a Coq term: https://github.com/coq-community/reduction-effects

Thanks. I tried that a while back but couldn't get it to do anything in MetaCoq Run. Probably because of the lazy evaluation. E.g. the following code does not trigger the printing effect, but changing the tmEval to use cbn does:

Definition a := let a := print_id (4 + 2) in a.
Definition test : TemplateMonad unit :=
  e <- tmEval lazy a;;
  tmPrint e.
MetaCoq Run test.

(although the 4+2 is clearly evaluated here, even with lazy, as the e is printed as 6).
However, anything but lazy evaluation sadly seems to be too slow for my use case.

Matthieu Sozeau (Dec 16 2020 at 09:58):

Do you have lots of proof terms in the program you are running, or calls to the safe inference / conversion functions ?

Lennard Gäher (Dec 16 2020 at 10:09):

Matthieu Sozeau said:

Do you have lots of proof terms in the program you are running, or calls to the safe inference / conversion functions ?

I don't have any proof terms in there, but I am using the reduce_opt reduction function from the checker plugin quite a bit -- that is probably blowing everything up when I don't use lazy.
(if I can't get it done any other way, my next step would probably be to try to eliminate as many of the reduction calls as possible for now -- but since I want to have a MC implementation of the guard checker that can check mostly the same things as the OCaml implementation, that is a bit undesirable and thus a last resort).

Matthieu Sozeau (Dec 16 2020 at 11:56):

reduce_opt is doing strong reduction, maybe that's the problem and you should rather use reduce_stack_term ?

Lennard Gäher (Dec 16 2020 at 18:26):

Matthieu Sozeau said:

reduce_opt is doing strong reduction, maybe that's the problem and you should rather use reduce_stack_term ?

Thank you! That was indeed the problem. I had only briefly looked at the source code of reduce_stack and was under the wrong impression that reduce_opt was computing a weak-head nf. With reduce_stack_term it is fast enough now to use cbn and also my printing is now happening in a reasonable time frame.

Matthieu Sozeau (Dec 16 2020 at 19:34):

Cool !

Last updated: Sep 25 2023 at 12:01 UTC