Dealing with F★ dependencies
When invoking F★, if the transitive dependencies of
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
When invoking F★ in batch (non-interactive) mode
- All the directories on the search path (i.e. current directory, F★'s
libdirectory, and anything passed via
--includeon the command-line) should abide by the new naming convention, wherein
Foo.Bar.fstMUST contain exactly one module directive
module Foo.Barat the beginning of the file, and vice-versa.
- Having both
Foo.fsion 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.fsis also an error. (JP: this is not an error and it should be.)
- Having both
foo.fston 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.fston the search path, then a spurious dependency on
Some.fstwill be generated. (Since pull request #772, where
Some.vhas 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 Fooand be named
- 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 Fooflag. In case the dependencies of your file change, you should kill the F★ process (
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
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
F★ currently supports only one output format for dependency graphs:
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.
graph, then the output format is for graphviz.
Things to know:
- you must pass the same
fstar --depand to
- 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.