Adrian Dapprich (Nov 26 2020 at 10:22): Adrian Dapprich (Nov 26 2020 at 10:22):Hi all, I'm trying to develop a plugin for coq at the moment and I have a question about using the ocaml debugger with a plugin.
I built coq v8.12 using dune and based my plugin on the coq-plugin-template by Emilio Arias and the ltac plugin in the plugins/ directory.
When I run the debugger using dune exec -- dev/dune-dbg coqtop I can have ocamldebug know about the directories of my built plugin _build/default/plugins/myplugin, _build/default/plugins/myplugin/.my_plugin.objs/byte using the directory command and even list the source code using list Mymodule but there seems to be no other debugging information in the compiled files since info events Mymodule does not print any events so I can't set a breakpoint as I planned. Curiously, this seems to be the same for the other plugins as well. ltac is the only one whose build directory ocamldebug knows about by default and calling info events Rewrite (or other modules of the ltac plugin) also results in an empty events list. But it works for other non-plugin coq libraries like info events Constrextern in interp.
So are these files built without debug information? I did not see anything relevant to that in the dune files of my plugin and the ltac plugin which would make them different from libraries like interp, where it shows events. And afaik dune compiles with -g by default so the events should be there. I'm afraid this might just be a problem with the directories that ocamldebug looks for compiled files but I don't know enough about that to debug (same result when using make instead of dune btw)
Gaëtan Gilbert (Nov 26 2020 at 10:26):what ocaml version?
note that plugins are "wrapped" so Rewrite is called Ltac_plugin.Rewrite or some such thing
Gaëtan Gilbert (Nov 26 2020 at 10:27):ocamldebug until recently had issues with dynlinked plugins, I found recent enough ocamldebug to be horribly slow so never got to see it work
Adrian Dapprich (Nov 26 2020 at 10:36):I'm on ocaml 4.09.1. with Ltac_plugin.Rewrite I can still list the source but it shows no events in the module. For my own plugin I was prefixing the modules so I had wrapping disabled anyways
Gaëtan Gilbert (Nov 26 2020 at 10:38):09 isn't new enough
you need to figure out how to statically link the plugin in coqc/coqtop
if using dune adding it to the right (libraries) list in topbin/dune may work
for wrapped plugins breakpoints may still get confused in my experience, maybe just the emacs breakpoint setter though
Adrian Dapprich (Nov 26 2020 at 11:32):Thank you very much. After upgrading ocaml to 4.11.1 and adding my plugin to the libraries of coqtop_byte_bin I can see the events. I will try debugging now.
Adrian Dapprich (Nov 26 2020 at 15:01):Also why do you say that 4.09.1 is too old? according to opam, coq 8.12.1 should support everything from 4.05 on right? fwiw it still works when I add my plugin to the library stanza when using ocaml 4.09.1. With 4.11.1 the debugger really is painfully slow (like 100x than at 4.09.1 when I tried to compile a simple test.v)
Gaëtan Gilbert (Nov 26 2020 at 15:04):too old for ocamldebug to understand dynlinked plugins
Gaëtan Gilbert (Nov 26 2020 at 15:04):so irrelevant when you add the plugin to static libraries
Last updated: Oct 13 2024 at 01:02 UTC