fstar-mode error message attributes error to exernal module

[kkohbrok]

When reporting an error (in a newly opened split buffer, but this is probably a separate issue), fstar-mode includes the name of the most recently open'd module like this: Example code, which causes an error due to the missing 't' at the end of "nat":

module Test

open FStar.Seq

type x = na

/home/kk/repositories/everest/FStar/ulib/FStar.Seq.Properties.fst(716,0-723,49): (Error) Identifier not found: [na](Also see: (5,9-5,11))] (FIXME)

Without opening FStar.Seq, the error is just

F*: subprocess exited.

(without openeing a split buffer). While running fstar.exe Test.fst from the command line just outputs:

./Test.fst(5,9-5,11) : (Error) Identifier not found: [na]

in both cases Or maybe this is due to a configuration error on my part?

[kkohbrok]

When using hints, the error message becomes:

Warning (emacs): F* checker reported issues in other files: [/home/kk/repositories/everest/FStar/ulib/FStar.Seq.Properties.fst(716,0-723,49): (Error) Identifier not found: [na](Also see: <\ input>(5,9-5,11))] (FIXME)

[s-zanella]

This seems to be an issue with F* itself, not fstar-mode.el

$ cat transcript
#push 1 0
module M
open FStar.Seq
let x = x 
#end #done-ok #done-nok

$ cat transcript | bin/fstar.exe --in M.fst
desugar_partial_module curmod=None
[...]/FStar.Seq.Properties.fst(716,0-723,49): (Error) Identifier not found: [x](Also see: <input>(3,8-3,9))
#done-nok

[s-zanella]

Closing this since we're tracking it in FStar.