diff options
Diffstat (limited to 'dev/doc/debugging.txt')
| -rw-r--r-- | dev/doc/debugging.txt | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index e5c83139..50b3b45c 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -4,8 +4,8 @@ Debugging from Coq toplevel using Caml trace mechanism 1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte) 2. Access Ocaml toplevel using vernacular command 'Drop.' 3. Install load paths and pretty printers for terms, idents, ... using - Ocaml command '#use "base_include";;' (use '#use "include";;' for a rawer - term pretty printer) + Ocaml command '#use "base_include";;' (use '#use "include";;' for + installing the advanced term pretty printers) 4. Use #trace to tell which function(s) to trace 5. Go back to Coq toplevel with 'go();;' 6. Test your Coq command and observe the result of tracing your functions @@ -15,6 +15,15 @@ Debugging from Coq toplevel using Caml trace mechanism notations, ...), use "Set Printing All". It will affect the #trace printers too. +Note for Ocaml 3.10.x: Ocaml 3.10.x requires that modules compiled +with -rectypes are loaded in an environment with -rectypes set but +there is no way to tell the toplevel to support -rectypes. To make it +works, use "patch -p0 < dev/doc/patch.ocaml-3.10.drop.rectypes" to +hack script/coqmktop.ml, then recompile coqtop.byte. The procedure +above then works as soon as coqtop.byte is called with at least one +argument (add neutral option -byte to ensure at least one argument). + + Debugging from Caml debugger ============================ |