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.

I get an error complaining about projectee's. What should I do?

This is a temporal workaround. Please remove this QaA entry once it is no longer needed.

Expected expression of type "(Module.entry (Module.property(Module.Entry.elem1 projectee)))";
got expression "elem2" of type "(Module.entry (Module.property elem1))"

You can use " --__temp_no_proj Module" to disable the creation of projectee's.

What to do about inconsistent OCaml object files?

Sometimes OCaml files are inconsistent and need to be deleted, here is an example with its specific solution:

Error: Files FStar_Mul.cmx and ./prims.cmx
       make inconsistent assumptions over interface Prims

run make -C ulib/ml clean in the F* main directory.