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.
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)
Yes, that one worked.
how did you configure exactly?
./configure -prefix $(current_dir) -native-compiler no -bytecode-compiler no -coqide no -no-custom
with and without -no-custom
Oh, also, I'm using Dune to build Coq. Should that matter?
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
dune instructions for ocamldebug https://github.com/coq/coq/blob/master/dev/doc/build-system.dune.md#ocamldebug
Ok I will try the legacy build and also your instructions for Dune, thanks!!
no don't try the legacy build
heh too late :) already tried and it didn't work
hmm now I am unable to find dune-dbg
... I have dune-dbg.in
. I did run make -f Makefile.dune world
.
are you using dune exec? do not call it directly
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.
Can I tell Makefile.dune
that I don't need CoqIDE?
Gah same result :sob:
passing dune-dbg
to dune exec
does the same thing as dune exec dune-dbg.in
yes, it just copies it...
it does make sure coqc_bin.bc
etc are built though
Have a look at dev/doc/build-system.dune.md for the dune targets
There is a cheat sheet at the bottom
Yes, that was the reference I was going by
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.
Yeah, dune seems to do a bit of thinking at first, I'm not sure if that's normal
I was actually talking about coqtop
's startup, after issuing run
.
ocamldebug is terrible in ocaml 4.10 and 4.11
Oh snap :D
It takes about a minute to print Welcome to Coq
and then the program exits and I get the (ocd)
prompt back...
oh I see it does not exit. It stops whenever a plugin is loaded.
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.
At the moment that should be targetting ocaml 4.12 I believe
Yes except that I haven't been able to use dev/dune-dbg on 4.12 yet
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.
Shachar Itzhaky said:
oh I see it does not exit. It stops whenever a plugin is loaded.
never seen that
btw I generally use ocamldebug with coqc not coqtop
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)
you can use Show.
to print the goal
After typing r
about a hundred times I finally got the Coq <
prompt lol.
Oh good thinking! I should try that.
Well at least 4.09.1 works nicely :laughing:
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.
Should that be a bug in Coq's build or in the debugger?
Last updated: Oct 13 2024 at 01:02 UTC