Stream: Coq users

Topic: Debugging Coq kernel code


view this post on Zulip Lennard Gäher (Nov 19 2020 at 08:43):

Hi,
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.

view this post on Zulip Michael Soegtrop (Nov 19 2020 at 09:27):

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 source dune_db.

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 run and print commands and pipe this into ocamldebug. Below is a script which creates a file one can pipe into ocamldebug setup for tracing cbv in one point - just change the breakpoint and print instruction to something else. Let me know if you find a better way.

#! /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

view this post on Zulip Lennard Gäher (Nov 19 2020 at 19:24):

Thanks! Seems like a good reason to try out dune then.


Last updated: Jan 27 2023 at 00:03 UTC