emacsgdbfstarfstar-mode

Gdb with emacs and F*


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*?


Solution

  • 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: