emacs - 带有 emacs 和 F* 的 Gdb

Question

我想使用 Emacs fstar-mode 和 gdb 调试简单的 F* 程序。在 fstar-mode https://github.com/FStarLang/fstar-mode.el的 wiki 的最后是信息：

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

没有进一步的解释。

在 Emacs 中（假设我正在编辑 Test.fst 文件）我调用fstar-gdb命令并继续到gdb控制台我正在尝试使用命令file Test和run. 他们工作正常，但是break 3（或任何其他行）说它main.c（显然）找不到第 3 行。

如何gdb与 F* 一起使用？

Answer 1

fstar-gdb 命令旨在调试 F* 编译器本身，而不是使用 F* 编译的程序。

对于 F* 程序，最好的可能是：

• ocamldebug 如果您使用的是字节编译器
• OCaml 程序的 GDB 调试的常用程序（参见https://ocaml.org/meetings/ocaml/2012/slides/oud2012-paper5-slides.pdf；这是因为大多数 F* 程序在编译之前被提取到 OCaml） .
• 如果您使用的是 Low*，则通常用于调试 C 程序的 GDB 调试过程。