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!
• Inconsistent implicit argument annotation on argument x
• What do these symbols mean?

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 to look in your *Messages* buffer in emacs for error messages.

You might also try 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 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

Inconsistent implicit argument annotation on argument x

Mixing OCaml-style type variables ('a) and implicit arguments is brittle. The best is to avoid mixing them, unless source compatibility with OCaml is required.

Results vary and are not very predictable. For instance, this doesn't type check

val f: #u:unit -> x:'a -> Tot unit
let f #u x = ()

whereas it type checks swapping the order of arguments

val f: x:'a -> #u:unit -> Tot unit
let f x #u = ()

What do these symbols mean?

While the F* symbols reference is incomplete, for most commonly used symbols, a short description exists there.