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 --include 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.fs is also an error. (JP: this is not an error and it should be.)
• Having both Foo.fst and foo.fst on the search path is an error.
• Precedence is determined as follows: FStar's standard library directory has precedence zero. The first --include argument has precedence one. The last --include argument has precedence n. The current directory has precedence n+1. If at least an interface exists, we generate a dependency on the interface with the highest precedence. If no interface exists, we generate a dependency on the implementation with the highest precedence.
• 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. (Since pull request #772, where Some.v has now been superseded with Some?.v, this should no longer happen.) (MK: if someone agrees with me that this bullet should be removed, please remove it +1)

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 along with the --verify_module Foo flag. 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★ currently supports only one output format for dependency graphs:

• When 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.
• When X is graph, then the output format is for graphviz.

Things to know:

• you must pass the same --include 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)
• 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.

Legacy 'build-config' feature.

Build-config headers have been removed in favour of the fstar --dep* options. A list of removed headers is available in issue #478 : https://github.com/FStarLang/FStar/issues/478

Note for F★ hackers

When editing files that fall within the FStar. namespace, you only get open Prims open FStar prepended to your file. Everyone else gets open Prims open FStar open FStar.All open FStar.ST.