The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I believe your problem is an issue with dynamically loaded code not showing up in the debugger. I heard of a patch of the Ocaml compiler meant to fix this, but I have no idea on its status. I'm not sure if it will work with bytecode compilation (though the Makefile suggests it will), but you may try to compile Coq with the "-natdynlink no" passed to "./configure" to avoid dynamic linking.

Another debugging tool you can use is tracing: open a coqtop.byte session. Type the "Drop." command to reveal an ocaml toplevel. Type the pragma "#use "include";;" to load the printers. Use the pragma "#trace Extract_env.separate_extraction;;" to trace "separate_extraction". Use the procedure "go ();;" to revert to the coq toplevel. When you do your extraction command you will now be able to see the arguments and returned value of each Extract_env.separate_extraction.

On 7 December 2013 17:33, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Hi Hugo,

Ok, ocamldebugger-coq was a typo and -debug is configured.
Anyway, I have some supposition about the source of problems, will write about it now in other topic.

Sincerely,
Kirill Taran

On Sat, Dec 7, 2013 at 1:20 PM, Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

Hi,

> I am trying to explore behaviour and fix a patch, so I am using debugger.
> I have read dev/doc/debugging.txt and as it says I use "ocamldebugger-coq"
> wrapper, but CLI version (not with emacs). Coq is configured with "-local
> -debug".

I don't know how to have the debugger running with CLI. If you
eventually find some, you might create a page on cocorico (e.g. in
section Miscellaneous at
http://coq.inria.fr/cocorico/CoqDevelopment/Public).

At least, the correct name of the wrapper is "ocamldebug-coq" in "dev'.

Also, be sure that all .ml files have been recompiled after you added
"-debug" to the configure script.

Best regards,

Hugo Herbelin