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.
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.
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?
Personally I'd use ocamldebug + step by step evaluation, with a handwritten breakpoint if the term is too complex
What are you trying to observe? A surprising behaviour or a performance issue?
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.
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.
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 13 2024 at 01:02 UTC