Gdb with emacs and F*

Question

I would like to debug simple F* program using Emacs fstar-mode and gdb. At the very end of the wiki of fstar-mode https://github.com/FStarLang/fstar-mode.el is information:

The fstar-gdb command (M-x) attaches GDB to the current F* process and launches Emacs' GDB-mi interface

with no further explanation.

When in Emacs (lets assume I am editing Test.fst file) I invoke fstar-gdb command and proceed to gdb console I am trying to use commands file Test and run. They are working correctly, however break 3 (or any other line) says that it failed to find line 3 in main.c (obviously).

How do I use gdb with F*?

Answer 1

The fstar-gdb command is intended to the debug F* compiler itself, not programs compiled with F*.

For F* programs, the best would likely be:

• ocamldebug if you're using the byte-compiler
• the usual procedure for GDB debugging of OCaml programs (see https://ocaml.org/meetings/ocaml/2012/slides/oud2012-paper5-slides.pdf; this is because most F* programs are extracted to OCaml before being compiled).
• the usual procedure for debugging GDB debugging of C programs if you're using Low*.