Stream: Coq devs & plugin devs

Topic: ocamldebug on newer ocaml


view this post on Zulip Gaëtan Gilbert (Oct 12 2021 at 12:44):

it seems ocamldebug fails with "debugger does not support channel locks" on ocaml 4.13.1
is debugging with newer ocaml versions impossible?

view this post on Zulip Gaëtan Gilbert (Oct 18 2021 at 20:00):

anyone know more about this?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 20:07):

Other than https://github.com/ocaml/ocaml/issues/10517 ?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 20:08):

I guess we need to ping OCaml experts, maybe it was working before by chance?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 20:08):

Simple compiler can work without thread

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 20:09):

threads, so worst case we can use that, submitting a PR is on my todo

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 20:11):

But if that's new in 4.13 seems like a funny stuff

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 20:12):

See also https://github.com/ocaml/ocaml/pull/10594 as pointed out

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 20:12):

in the other issue

view this post on Zulip Gaëtan Gilbert (Oct 18 2021 at 20:15):

could be new in 4.12 as I don't think I tested that one

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 20:16):

So indeed seems maybe that 4.12/4.13 broke the old behavior "don't bail out until a thread is created"

view this post on Zulip Enrico Tassi (Oct 19 2021 at 08:36):

Gaëtan Gilbert said:

it seems ocamldebug fails with "debugger does not support channel locks" on ocaml 4.13.1
is debugging with newer ocaml versions impossible?

(troll) Printf is your best friend (/troll).

view this post on Zulip Hugo Herbelin (May 30 2022 at 16:48):

Hi, I'm a bit lost with ocamldebug which I just upgraded from 4.06 to 4.11.2. I have two problems:

Time: 13385948 - pc: 0:4009448 - module Tactics
Breakpoint: 3
1507   <|b|>let indsort = Inductive.inductive_sort_family (snd (Global.lookup_inductive ind)) in

but without the file tactics.ml to be automatically opened at line 1507 as expected. Has anyone experimented the same behavior and/or know what to do?

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 16:57):

https://v2.ocaml.org/manual/debugger.html#ss:debugger-stop-at-new-load

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 16:58):

put set break_on_load off in your .ocamldebug

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 16:59):

the emacs problem is probably because dune started removing the INSIDE_EMACS env var

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 16:59):

see https://github.com/coq/coq/pull/15878

view this post on Zulip Gaëtan Gilbert (May 30 2022 at 17:00):

so you have to call dune-dbg -emacs coqc instead of dune-dbg coqc

view this post on Zulip Hugo Herbelin (May 31 2022 at 06:45):

Thanks a lot (and looking forward debugging dynamically loaded code).


Last updated: Feb 06 2023 at 19:03 UTC