Stream: Coq devs & plugin devs

Topic: Debugging with `ocamldebug`


view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 09:11):

Hi! :wave: I am trying to debug Coq on the command line following https://github.com/coq/coq/blob/master/dev/doc/debugging.md#debugging-with-ocamldebug-from-the-command-line. I tried both macOS and Linux and I also tried -no-custom (even though it is said to be required only on Windows), but I keep getting this error after run:

(ocd) run
Fatal error: debugger does not support channel locks

Couldn't find any info about this error in Google... What am I doing wrong?

I am using OCaml 4.12.0 64-bit version.

view this post on Zulip Gaëtan Gilbert (Jul 15 2021 at 09:16):

never seen this error
can you try (in a temporary directory):

touch foo.ml
ocamlc foo.ml -g -o foo
ocamldebug foo

and in ocamldebug run
it should quickly say "program exit"
(basically testing ocamldebug on a trivial program)

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 09:17):

Yes, that one worked.

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

how did you configure exactly?

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 09:19):

./configure -prefix $(current_dir) -native-compiler no -bytecode-compiler no -coqide no -no-custom

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 09:19):

with and without -no-custom

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 09:24):

Oh, also, I'm using Dune to build Coq. Should that matter?

view this post on Zulip Gaëtan Gilbert (Jul 15 2021 at 09:25):

those instructions are for the legacy build system (also they're probably broken)
also never configure when using pure dune build, and always do make -f Makefile.dune

view this post on Zulip Gaëtan Gilbert (Jul 15 2021 at 09:26):

dune instructions for ocamldebug https://github.com/coq/coq/blob/master/dev/doc/build-system.dune.md#ocamldebug

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 09:29):

Ok I will try the legacy build and also your instructions for Dune, thanks!!

view this post on Zulip Gaëtan Gilbert (Jul 15 2021 at 09:32):

no don't try the legacy build

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 09:42):

heh too late :) already tried and it didn't work

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 09:46):

hmm now I am unable to find dune-dbg... I have dune-dbg.in. I did run make -f Makefile.dune world.

view this post on Zulip Gaëtan Gilbert (Jul 15 2021 at 09:54):

are you using dune exec? do not call it directly

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:18):

yes I did try dune exec, but I think I ruined something during my earlier attempts, so now it complains that it does not have coqide_gui; I'm going to try a fresh build.

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:18):

Can I tell Makefile.dune that I don't need CoqIDE?

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:31):

Gah same result :sob:

view this post on Zulip Ali Caglayan (Jul 15 2021 at 10:34):

passing dune-dbg to dune exec does the same thing as dune exec dune-dbg.in

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:34):

yes, it just copies it...

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:35):

it does make sure coqc_bin.bc etc are built though

view this post on Zulip Ali Caglayan (Jul 15 2021 at 10:35):

Have a look at dev/doc/build-system.dune.md for the dune targets

view this post on Zulip Ali Caglayan (Jul 15 2021 at 10:35):

There is a cheat sheet at the bottom

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:36):

Yes, that was the reference I was going by

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:51):

I am not getting the error with Dune on OCaml 4.10.2. It does seem to take it forever to start up, is that usual? I will try a fresh switch of 4.12.0 now.

view this post on Zulip Ali Caglayan (Jul 15 2021 at 10:53):

Yeah, dune seems to do a bit of thinking at first, I'm not sure if that's normal

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:53):

I was actually talking about coqtop's startup, after issuing run.

view this post on Zulip Gaëtan Gilbert (Jul 15 2021 at 10:53):

ocamldebug is terrible in ocaml 4.10 and 4.11

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:54):

Oh snap :D

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:56):

It takes about a minute to print Welcome to Coq and then the program exits and I get the (ocd) prompt back...

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 10:57):

oh I see it does not exit. It stops whenever a plugin is loaded.

view this post on Zulip Ali Caglayan (Jul 15 2021 at 10:57):

If you opam install ocaml-variants and create a switch for ocaml-option-flambda.1 it turns on the flambda flag for the ocaml compiler. This takes a bit longer to build, but supposedly the binary is faster.

view this post on Zulip Ali Caglayan (Jul 15 2021 at 10:58):

At the moment that should be targetting ocaml 4.12 I believe

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 11:03):

Yes except that I haven't been able to use dev/dune-dbg on 4.12 yet

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 11:04):

Shachar Itzhaky said:

oh I see it does not exit. It stops whenever a plugin is loaded.

Any way to avoid that? There are tons of plugins loaded on init.

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

Shachar Itzhaky said:

oh I see it does not exit. It stops whenever a plugin is loaded.

never seen that

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

btw I generally use ocamldebug with coqc not coqtop

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 11:08):

I noticed that coqc is the common case for debugging. I will try although I was trying to debug an error that as of now only happens in coqtop (has to do with printing the goal)

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

you can use Show. to print the goal

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 11:10):

After typing r about a hundred times I finally got the Coq < prompt lol.

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 11:10):

Oh good thinking! I should try that.

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 11:15):

Well at least 4.09.1 works nicely :laughing:

view this post on Zulip Emilio Jesús Gallego Arias (Jul 15 2021 at 11:32):

Yeah, the ocaml debugger is a pain, and in 4.10 and 4.11 is very slow. If that doesn't work in 4.12 please open a bug report and I'll fix it.

view this post on Zulip Shachar Itzhaky (Jul 15 2021 at 15:37):

Should that be a bug in Coq's build or in the debugger?


Last updated: Oct 21 2021 at 21:03 UTC