I'm trying to understand parts of the Coq kernel code, in particular the implementation of inductives & the guardedness checker (with the goal of re-implementing the guardedness check in MetaCoq). Since parts of the code are a bit hard to understand, I would like to get some traces of what the code does when it is checking some fixpoints and how exactly the representation of inductives is working.
What are good debugging workflows for the Ocaml code to facilitate this? Are these documented anywhere?
Ideally, I'd just add
print mind_body (or similar) expressions at some points, to print the term structure of the inductive representations used in the Ocaml implementation, but Ocaml seems to lack the capabilities for this (and writing print functions by hand for the representations used in the kernel seems quite laborious).
ocamldebug does not seem to be that useful for me, but maybe I'm just lacking the right workflow.
I usually look into higher layers - there Coq seems to come with a nice set of debug printers for terms. I would imagine that this is the same for kernel structures, but I don't know. If you build Coq with dune, dune creates a file you can source into ocamldebug to load all the printers via
I do use ocamldebug for tracing but it requires some rather grotesque hacks around it because (afaik) it doesn't have the concept of a watch point. So what I do is create a large file with say 1 million
#! /bin/sh # Usage: # Possibly (if dune complains about unwanted files) # ATTENTION: this kills all untracked files! # git clean -d -f -X # Build Coq # make -f Makefile.dune world # Create ocamldebug script # ./make_ocamldebug_run.sh # Run coqtop in ocamldebug # dune exec -- dev/dune-dbg coqtop # Run ocamldebug script # (ocd) source cbv_debug.od # Run Coq command # Coq < Eval compute in (2*2). # Note: you get out of coqtop and ocamldeubg with 2x Ctrl+D # Alternative to get the output to a file: # Run coqtop in ocamldebug # dune exec -- dev/dune-dbg coqtop > trace.log # Run ocamldebug script (you won't see a ocamldebug prompt) # source cbv_debug.od # Run Coq command (you will see a Coq prompt) # Coq < Eval compute in (2*2). # CAVEATS: # - this will print the sub terms seen in the evaluation - not the complete terms # - the trace might contain at the begin and end evaluations which are run for pretty printing # - in case the evaluation takes more than 1 million steps run "source run_20.od" again # or simply create even larger files (or use a shell script with I/O redirection) # This might be easier to do without redirection of the output to trace.log, # so I would first use it without redirection # Load Coq specific debug printers echo source dune_db > cbv_debug.od # Run Coq so far that Cbv module is loaded echo goto 8000000 >> cbv_debug.od # Set breakpoint in Cbv module at central evaulation function # You can experiment with that but then might have to adjust the print command echo break Cbv.norm_head >> cbv_debug.od # Source ocamdebug command file to trace 2^20 evaluation steps echo source run_20.od >> cbv_debug.od > run_10.od for i in $(seq 1 1024) do echo run >> run_10.od echo print t >> run_10.od done for i in $(seq 10 19) do cat run_$i.od run_$i.od > run_$(expr $i + 1).od cat run_$i.od run_$i.od > run_$(expr $i + 1).od done
Thanks! Seems like a good reason to try out dune then.
Last updated: Dec 05 2023 at 11:01 UTC