fstar-fstar模式和命令行上的不同结果

我正在学习F的教程* https://www.fstar-lang.org/tutorial/ 我用fstar模式设置emacs https://github.com/FStarLang/fstar-mode.el 在ubuntu我想我不知道如何正确地键入检查文件,因为当我使用两种不同的方法为教程中的文件执行此操作时:

module Ex01a

open FStar.Exn
open FStar.All
//safe-read-write


type filename = string

(** [canWrite] is a function specifying whether a file [f] can be written *)
let canWrite (f:filename) = 
  match f with 
    | "demo/tempfile" -> true
    | _ -> false

(** [canRead] is also a function ... *)
let canRead (f:filename) = 
  canWrite f               (* writeable files are also readable *)
  || f="demo/README"       (* and so is demo/README *)


val read  : f:filename{canRead f}  -> ML string
let read f  = FStar.IO.print_string ("Dummy read of file " ^ f ^ "\n"); f

val write : f:filename{canWrite f} -> string -> ML unit
let write f s = FStar.IO.print_string ("Dummy write of string " ^ s ^ " to file " ^ f ^ "\n")


let passwd : filename = "demo/password"
let readme : filename = "demo/README"
let tmp    : filename = "demo/tempfile"


val staticChecking : unit -> ML unit
let staticChecking () =
  let v1 = read tmp in
  let v2 = read readme in
  let v3 = read passwd in
  write tmp "hello!"
  (* ; write passwd "junk" // invalid write , fails type-checking *)


exception InvalidRead
val checkedRead : filename -> ML string
let checkedRead f =
  if canRead f then read f else raise InvalidRead


assume val checkedWrite : filename -> string -> ML unit


let dynamicChecking () =
  let v1 = checkedRead tmp in
  let v2 = checkedRead readme in
  let v3 = checkedRead passwd in (* this raises exception *)
  checkedWrite tmp "hello!";
  checkedWrite passwd "junk" (* this raises exception *)

let main = staticChecking (); dynamicChecking ()

然后根据使用命令行或emacs类型检查,我得到两个不同的结果(分别是不正确和正确的),如下所示:

在顶部,使用“reload and typecheck up to point”可以正确地在“write password”垃圾行中找到一个错误,而底部的控制台行则声称所有验证条件都已成功解除。

我错过了什么?