search

FStarLang / fstar-mode.el

Emacs support for F*
Apache License 2.0
67 stars 17 forks source link

Code that typechecks normally from the command line can crash fstar-mode #109

Closed felixbreton closed 5 years ago

felixbreton commented 5 years ago

The following code (put in a file called Foo.fst) can be typechecked normally with the 

fstar.exe Foo.fst

command, but when the last line is typechecked in fstar-mode, it crashes and the subprocess must be killed.

module Foo

open FStar.Buffer

let wat buff =assert( buff.(0ul) % 2 = 0)

Also, the following error message appears in emacs : "error in process filter : Not enough arguments for format string".

cpitclaudel commented 5 years ago

Thanks for the report!