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
Did you try with
OCAMLRUNPARAM='b' dune utop
also make sure your bytecode objects are compiled with -g
.
1 Like
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.
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.
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
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