Early stumbling blocks, FAQ

Table of Contents

• Confusing error message
• Which editor should I use?
• What to do about inconsistent OCaml object files?
• [Error message: two types differ but look the same in the error message?][#equal-types-different]
• I get an error complaining about projectee's.

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")

See also

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.