Stream: Coq devs & plugin devs

Topic: ocamldebug on newer ocaml

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?

Gaëtan Gilbert (Oct 18 2021 at 20:00):

anyone know more about this?

Emilio Jesús Gallego Arias (Oct 18 2021 at 20:07):

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

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?

Emilio Jesús Gallego Arias (Oct 18 2021 at 20:08):

Simple compiler can work without thread

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

Emilio Jesús Gallego Arias (Oct 18 2021 at 20:11):

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

Emilio Jesús Gallego Arias (Oct 18 2021 at 20:12):

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

Emilio Jesús Gallego Arias (Oct 18 2021 at 20:12):

in the other issue

Gaëtan Gilbert (Oct 18 2021 at 20:15):

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

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"

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).

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:

• it stops at each module dynamically loaded: this makes about 50 steps to do manually
• in Emacs, I don't have any more stepping done directly in the file. Instead, I just have lines of the form:

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?

Gaëtan Gilbert (May 30 2022 at 16:57):

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

Gaëtan Gilbert (May 30 2022 at 16:58):

put set break_on_load off in your .ocamldebug

Gaëtan Gilbert (May 30 2022 at 16:59):

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

Gaëtan Gilbert (May 30 2022 at 16:59):

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

Gaëtan Gilbert (May 30 2022 at 17:00):

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

Hugo Herbelin (May 31 2022 at 06:45):

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

Last updated: Dec 06 2023 at 13:01 UTC