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).
The loading of printers can be worked around by removing some libraries from the db file
As for the slowness, it's a known bug that was fixed in OCaml master IIRC
does 4.12.0 beta solve it?
didn't try it yet
I only use 4.11 for the memtrace profiling
https://github.com/ocaml/ocaml/issues/9606
4.12.0 seems to have some non-trivial trouble with our ocamldebug suppot
You mean, the dynlink errors?
That's easy to solve, stuff such as Loading program... done.
Fatal error: debugger does not support channel locks
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?
@ejgallego: is 4.12 thus not usable for Coq debugging also?
we have a few dune_db versions for different ocaml version, I guess making non-dune db versions was skipped
building db at configure time would be interesting but doesn't work great with dune insisting on building stuff in _build
maybe we could have dune_db source _build/.../generated_db
@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.
So I'm not very worried about that, tho it is annoying now
@Gaëtan Gilbert you can make the db a promoted file and add a version link
but it would be more cost effective to actually write the rules down in Dune itself
so dune ocaml debug topbin/coqc.exe
just works
should be fairly easy to do once you get a bit familiar with the rule language
For reference, that's the issue where most recent discussion has happened https://github.com/ocaml/dune/issues/3818
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?
(w/o the inline, it complains on threads)
looks like that's what we do for dune_db_408
I don't remember if we know why
cc @Emilio Jesús Gallego Arias
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?
dune also has a byterun.cma to load afaict
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?
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 13 2024 at 01:02 UTC