Dealing with F★ dependencies

When invoking F★, if the transitive dependencies of Foo.fst are Bar₁…Barₙ.fst, you previously had to call fstar Bar₁…Barₙ.fst Foo.fst. This was tedious, error-prone, and posed a maintenance burden. Fortunately, F★ can now figure out dependencies automatically.

Note: this behavior can always be disabled using --explicit_deps.

When invoking F★ in batch (non-interactive) mode

• All the directories on the search path (i.e. current directory, F★'s lib directory, and anything passed via -I on the command-line) should abide by the new naming convention, wherein Foo.Bar.fst MUST contain exactly one module directive module Foo.Bar at the beginning of the file, and vice-versa.
• Having both Foo.fsti and Foo.fsi on the search path is forbidden (the dependency analysis can't figure out which of the two it should use, so this is a hard error).
• Having both Foo.fst and foo.fst on the search path is an error.
• Caveat: if you use the projector syntax (Some.v) and you also happen to have Some.fst on the search path, then a spurious dependency on Some.fst will be generated.

When invoking F★ in interactive mode

• The file you're editing should exist on the filesystem.
• The file you're editing should start with module Foo and be named Foo.fst
• The file you're editing must be, when sending the first chunk, a syntactically valid F★ file.
• F★ initially runs a dependency analysis on your file, then starts itself with all the dependencies it found. In case the dependencies of your file change, you should kill the F★ process (C-c C-x).

One way to easily deal with these requirements is, when starting a new file, to write out:

module Foo

open FStar.List
// other dependencies

then save the file, and send the first chunk to F★.

When invoking F★ in dependency mode

The fstar executable takes an extra --dep X argument; when called in this mode, fstar builds a dependency graph for all the files listed on the command-line. This is useful if you want to run the dependency analysis once and for all, then encode the dependency graph in a Makefile in order to, say, make verification more parallel; in that case, you would call fstar --explicit_deps.

F★ can dump the graph in one of two formats.

• If X is make, then the output format is the classic Makefile format target.fst: dependency1.fst … dependencyₙ.fst. There is one line per node in the dependency graph.
• If X is nubuild, then the tool outputs a topologically-sorted, newline-separated list of all the files in the graph, that is, all the files passed on the command-line along with their dependencies.

Things to know:

• you must pass the same -I flags to fstar --dep and to fstar;
• indeed, the tool relies on the filesystem; therefore, the files you work with must abide by the new naming convention (as above)
• if there's exactly one file on the command-line, fstar prepends several .fst files to the file list; therefore, you will get extra lines in your Makefile-style output;
• files found in the current directory are printed as relative paths; files found in other include directories are printed as absolute paths; files passed on the command-line are printed as-is in the output.