Early stumbling blocks, FAQ

FStar gives me a confusing error message. What can I do?

This will happen quite often. Don't PANIC. Often making sure that you re-compiled fstar after a pull will help.

Here is a, not necessarily representative example:

$ fstar <some-fst-file>
E:\FStar\bin\..\ulib\prims.fst(628,14-628,14) : Error
Syntax error: Failure("unexpected char")

Which editor should I use?

It is up to you, see Editor-support-for-F*, but currently fstar-mode is the most actively developed.

How can I include non-standard libraries when using fstar-mode?

Add the following line to your .emacs.

(setq fstar-subp-prover-args '("--include" "<your-path>"))

Note that under cygwin, fstar is a windows program and expects windows pathnames. For example,

(setq fstar-subp-prover-args '("--include" "E:\\FStar\\ucontrib\\Platform\\fst")

('\\' is used to escape a Windows pathname.) See fstar-subp-prover-args for more documentation.

fstar-mode gives error message "F*: subprocess exited". What shall I do?

The first thing to try is running fstar <file-name> in a terminal to see whether you get a more meaningful error message.

How to debug an error message complaining about two types being different that look the same in the error message?

E.g. Expected type "(Prims.list entry)"; got type "(Prims.list entry)"

Use --print_universes and --print_implicits options to see hidden differences.