Stream: Coq devs & plugin devs

Topic: Debugging Coq with OCaml 4.11


view this post on Zulip Hugo Herbelin (Nov 27 2020 at 16:51):

Did someone succeed to use ocamldebug 4.11 on coqtop.byte? On one side it is unusably slow (several minutes to get the Coq prompt). On the other side, loading of printers fails (error Dynlink_compilerlibs is already loaded).

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 16:55):

The loading of printers can be worked around by removing some libraries from the db file

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 16:56):

As for the slowness, it's a known bug that was fixed in OCaml master IIRC

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 16:56):

does 4.12.0 beta solve it?

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 16:56):

didn't try it yet

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 16:56):

I only use 4.11 for the memtrace profiling

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 16:57):

https://github.com/ocaml/ocaml/issues/9606

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 17:24):

4.12.0 seems to have some non-trivial trouble with our ocamldebug suppot

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 17:51):

You mean, the dynlink errors?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 18:01):

That's easy to solve, stuff such as Loading program... done. Fatal error: debugger does not support channel locks

view this post on Zulip Hugo Herbelin (Nov 27 2020 at 20:13):

Thanks for the informations. Removing dynlink.cma _and_ inlining core.dbg in db seems to work (w/o the inline, it complains on threads). Don't know exactly what procedure to have the debugger working the different versions of OCaml? Building a different db file at configure time?
@ppedrot, @ejgallego: I suppose that 4.10 is the version from which the dynlink change appears, right?

view this post on Zulip Hugo Herbelin (Nov 27 2020 at 20:16):

@ejgallego: is 4.12 thus not usable for Coq debugging also?

view this post on Zulip Gaëtan Gilbert (Nov 27 2020 at 20:22):

we have a few dune_db versions for different ocaml version, I guess making non-dune db versions was skipped

view this post on Zulip Gaëtan Gilbert (Nov 27 2020 at 20:22):

building db at configure time would be interesting but doesn't work great with dune insisting on building stuff in _build

view this post on Zulip Gaëtan Gilbert (Nov 27 2020 at 20:23):

maybe we could have dune_db source _build/.../generated_db

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 22:58):

@ejgallego: is 4.12 thus not usable for Coq debugging also?

I found some problems that I don't understand.

Regarding the db / rules, at some point I hope all that is automatically handled by dune, already there is support for installing printers for example.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 22:59):

So I'm not very worried about that, tho it is annoying now

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 22:59):

@Gaëtan Gilbert you can make the db a promoted file and add a version link

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 22:59):

but it would be more cost effective to actually write the rules down in Dune itself

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 22:59):

so dune ocaml debug topbin/coqc.exe just works

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 23:00):

should be fairly easy to do once you get a bit familiar with the rule language

view this post on Zulip Emilio Jesús Gallego Arias (Nov 28 2020 at 17:52):

For reference, that's the issue where most recent discussion has happened https://github.com/ocaml/dune/issues/3818

view this post on Zulip Hugo Herbelin (Jan 15 2021 at 11:16):

Hi, coming back to this thread, now with OCaml 4.08 which seems to require the inlining of core.dbg into db so that source db works in the debugger. Is this confirmed? Is it worth a PR?

view this post on Zulip Hugo Herbelin (Jan 15 2021 at 11:17):

(w/o the inline, it complains on threads)

view this post on Zulip Gaëtan Gilbert (Jan 15 2021 at 11:29):

looks like that's what we do for dune_db_408
I don't remember if we know why

view this post on Zulip Gaëtan Gilbert (Jan 15 2021 at 11:29):

cc @Emilio Jesús Gallego Arias

view this post on Zulip Hugo Herbelin (Jan 15 2021 at 11:31):

You mean that it is enough to do source dune_db_408 instead? Then, why not to do it in standard, since using the debugger is independent per se of using dune, right?

view this post on Zulip Gaëtan Gilbert (Jan 15 2021 at 11:37):

dune also has a byterun.cma to load afaict

view this post on Zulip Hugo Herbelin (Jan 15 2021 at 12:28):

Ah, ok that's the difference. Where does byterun.cma come from? Is it otherwise part of kernel.cma? Why isn't there no byterun.cma w/o dune?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2021 at 23:17):

Don't remember all the details, actually now that you mention it byterun.cma should be empty so I'm not sure why we load it, likely we can drop it.

Dune creates and empty cma for a library with only stubs, IIANM.


Last updated: Oct 16 2021 at 03:02 UTC