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 :)
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
You might also "force" evaluation order sometimes using CPS
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.
Do you have lots of proof terms in the program you are running, or calls to the safe inference / conversion functions ?
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).
reduce_opt is doing strong reduction, maybe that's the problem and you should rather use reduce_stack_term
?
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.
Cool !
Last updated: Sep 25 2023 at 12:01 UTC