Early stumbling blocks, FAQ

Table of Contents

• Confusing error message
• Which editor should I use?
• Include non-standard libraries when using fstar-mode
• Error message: two types differ but the same in the error message?
• Error message: complaining about projectee's.
• Error message: inconsistent OCaml object files?
• My pattern-match on a pair won't type-check!

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 other Error message: ... in table of content.

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

See fstar-mode for more information.

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.

You could also look in your Messages buffer in emacs for error messages.

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 temporary 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.

My pattern-match on a pair won't type-check!

This doesn't work because of a bug (#682)

val map2:
  n:nat ->
  f:('a -> 'b -> Tot 'c) ->
  l1:vec 'a n ->
  l2:vec 'b n ->
  Tot (vec 'c n)
let rec map2 n f l1 l2 =
  match l1, l2 with
  | Cons hd1 n1 tl1, Cons hd2 n2 tl2 ->
      Cons (f hd1 hd2) n2 (map2 n2 f tl1 tl2)
  | Nil, Nil ->
      Nil

Instead, do:

val map2:
  n:nat ->
  f:('a -> 'b -> Tot 'c) ->
  l1:vec 'a n ->
  l2:vec 'b n ->
  Tot (vec 'c n)
let rec map2 n f l1 l2 =
  match l1 with
  | Cons hd1 n1 tl1 ->
      begin match l2 with
      | Cons hd2 n2 tl2 ->
          Cons (f hd1 hd2) n2 (map2 n2 f tl1 tl2)
      end
  | Nil ->
      begin match l2 with
      | Nil ->
          Nil
      end