Debugging FStar

This wiki page explains how to debug problems in F* itself or in the verification of your program.

For debugging problems in extracted code use a normal OCaml, F#, or C debugger, depending on what you extract to.

Debug output

Debugging in F* works by selecting:

1. via --debug: a set of modules to debug, and
2. via --debug_level: a set of debug levels that we are interested in.

Debug messages will be printed only for the enabled modules and only when they are relevant to the level, so both usually need to be provided. Note that levels are case-sensitive (but module names are not).

As an exception to the rule above, simply providing --debug X without any level does have a small effect: it prints some top-level messages (e.g. loading of plugins and opening of files). In fact, X can be anything to enable these messages, so --debug y is a common way to do so.

Also, there are (currently) two levels which are module independent: CheckedFiles and Dep; simply providing --debug_level Dep will print information on the dependency analysis without needing any --debug.

There are Low, Medium, High and Extreme levels, each of which is contained in the next one.These print increasingly detailed information on the typechecking process. If you're trying to figure out when a crash or infinite loop happens, starting from --debug_level Low and moving upwards is a good idea. Setting --error_contexts true can also help.

Aside from this linear hierarchy, other levels are usually completely independent. See Debugging flags for a list.

Debugging interactive-mode-specific issues

• Start Emacs, open your F* file (e.g. test.fst)
• Press M-x fstar-toggle-debug; notice the new, empty *fstar-debug* window
• Reproduce the error/crash/issue; queries and responses are logged to the *fstar-debug* window.
• Exit F* with C-c C-x, move to the *fstar-debug* window, and press M-x fstar-write-transcript and chose a name for the transcript (e.g. test); notice two new files, test.in and test.out.
• Ensure that the bug is reproducible on the command line by running fstar --ide test.fst < test.in. The output should match that found in test.out

You can now use extra debugging options and flags to figure out what the issue is, without replaying the bug steps by hand every time.

Tip: Flycheck and Eldoc tend to generate a lot of queries, which clutter the logs. If your bug isn't related to one of these two, turning them off helps. To do that, press M-x flycheck-mode and M-x eldoc-mode.