Debugging dune utop

utop
dune
#1

I am trying to invoke dune utop and it immediately fails with exception caused by failWith somewhere in my code. I am trying to debug where exactly this is happening. I do not see a way to get a backtrace. I tried various dune utop flags, like --debug-backtraces to no avail. Any suggestions how to debug this?

$ dune utop
Fatal error: exception Failure("AXIOM TO BE REALIZED")

$ grep -R "AXIOM TO BE REALIZED"| wc -l 
29
#2

Did you try with

OCAMLRUNPARAM='b' dune utop

also make sure your bytecode objects are compiled with -g.

1 Like
#3

Thanks! that helped a little. It gave me a liitle more info:

$ OCAMLRUNPARAM='b' dune utop --debug-backtraces
Fatal error: exception Failure("AXIOM TO BE REALIZED")
Raised at file "stdlib.ml", line 33, characters 22-33
Called from file "extracted/Rdefinitions.ml", line 8, characters 2-33

I still do not know why this particular function was invoked. I would like to see the full backtrace from toplevel.

#4

Do you have a repository that we can use to reproduce the stack trace? I would like to see why the stack trace is being truncated.

#5

Yes. Here is the repo:

It requires some Coq packages. They are installable via OPAM, but you need to add Coq’s repository:

https://coq.inria.fr/opam-using.html

After building, try dune utop in src/ml

#6

it seems like there’s nothing wrong with the backtraces and your exception is raised as a module loading side effect. Here’s your definition:


(** val coq_R0 : coq_R **)

let coq_R0 =
  failwith "AXIOM TO BE REALIZED"

coq_R0 isn’t a function, but this module is being linked to the bytecode binary which raises the exception.

2 Likes