Stream: Coq devs & plugin devs

Topic: Ocaml trace of cbv runs in endless loop


view this post on Zulip Michael Soegtrop (Aug 11 2020 at 21:15):

I wated to debug what cbv is doing in a certain case. What I do is:

coqtop.byte
Set Printing All.
Drop.
#use "base_include";;
#trace Cbv.norm_head;;
go();;
Eval cbv in (2+2).

it never ends - at least not in 5 minutes. I guess the debug printers are calling cbv now since numeral notations are now computed in gallina, but I don't get why it still doesn't work when I do Set Printing All.
Also interesting: when I do something similar (a bit tricky but doable in ocamldebug, I see the cbv for the notations (wit Unset Printing All) once on input ant once on output as expected.

view this post on Zulip Pierre-Marie Pédrot (Aug 11 2020 at 21:18):

Normally, in the debugger, the code for printing and the code being run are two different programs so this kind of issue shouldn't happen. That's one of the reasons I never use tracing btw.

view this post on Zulip Michael Soegtrop (Aug 11 2020 at 21:26):

What about notations being evaluated in gallina? As far as I understand the printers print these (at least it is said so in dev/doc/debugging.md) - I guess this must be the same cbv then.
What would you do to debug cbv?

view this post on Zulip Pierre-Marie Pédrot (Aug 11 2020 at 21:27):

Personally I'd use ocamldebug + step by step evaluation, with a handwritten breakpoint if the term is too complex

view this post on Zulip Pierre-Marie Pédrot (Aug 11 2020 at 21:28):

What are you trying to observe? A surprising behaviour or a performance issue?

view this post on Zulip Michael Soegtrop (Aug 12 2020 at 07:20):

What are you trying to observe? A surprising behaviour or a performance issue?

A performance issue - mostly cases where cbv takes a very long time for relatively simple terms.

One issue with ocamldebug I have is that I need to debug a development which needs libraries which take a long time to compile (say all in all one hour). Also these libraries are best compiled with Opam. It is easy to use ocamldebug with a freshly compiled coq, especially via dune, but I can't manage to:

What I didn't try as yet is to tell opam to use a manually compiled Coq.

view this post on Zulip Michael Soegtrop (Aug 12 2020 at 07:35):

Btw.: it is the input which ends up in an endless loop - not the output. If I set "Set Printing All" the output works as expected. It is expected that when I use notations on input the parser runs once, but it seems to use notations when printing the traces of the parser, which results into additional evaluations. This looks like a bug - I will create an issue.

view this post on Zulip Michael Soegtrop (Aug 12 2020 at 08:25):

P.S.: actually the input does not run into an endless loop - it just takes very long, almost 6 minutes to parse 32 with tracing enabled. The solution is to input terms without numeral notations.

Time Eval cbv in 32.
     : nat
     = S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S ...)))))))))))))))))))))))
     : nat
Finished transaction in 342.399 secs (336.516u,0.411s) (successful)

Last updated: Oct 16 2021 at 09:07 UTC