The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

dune secretly renames the plugin ml files, because unlike the main files we 
don't use (wrapped false)
as such plugins/extraction/foo.ml is renamed to 
plugins/extraction/extraction_plugin__Foo.ml
(note the capitalization of the first letter)

If using OCaml < 4.10 you also need to statically link the plugins you want 
to step through
On Coq master this is done by adding coq-core.plugins.$name to the 
(libraries) for the executable you're debugging in topbin/dune

If using OCaml 4.10 or 4.11 ocamldebug is deathly slow to the point of 
unusability.

You may be able to debug coqtop used by PG using "loadingmode manual" 
https://ocaml.org/manual/debugger.html#ss:debugger-loading
I've not tested this thoug, generally I use ocamldebug on coqc anyway

Gaëtan Gilbert

On 08/06/2021 20:29, Tj Barclay wrote:
> Howdy,
>
> I've been trying to figure out how to debug the extraction plugin. What I'd like to do is 
> execute an Extraction vernacular command in coqtop (or PG if that's an option) and have 
> that go until hitting a breakpoint set in one of the plugin's .ml files. So far all I've 
> managed to get working is running coqtop in ocamldebug using the provided code in 
> dev/tools/coqdev.el. From there I can set breakpoints in files like toplevel/coqtop.ml 
> <http://coqtop.ml> and toplevel/coqloop.ml <http://coqloop.ml>, but can't set 
> breakpoints in plugins/extraction/*.ml even after Require Extraction.
>
> I appreciate any tips on how to get this going, or guidance on how to 
> properly go about debugging Coq plugins in general if what I'm proposing 
> doesn't work or isn't recommended.
>
>
> Best,
> TJ
>
> --
> TJ Barclay
> Electrcial Engineering & Computer Science, University of Kansas
> tjbarclay AT ku.edu <mailto:tjbarclay AT ku.edu>
> +1 316 259 2250