Failure to report proper error location

[beurdouche]

module Test

let test () =
  (if mistake then IO.print_string "Hello!\n"
  else IO.print_string "Clement\n")

The smallest example I could find, in this scenario the F* mode doesn't report properly the error location. It seems to happen in the first definitions according to @s-zanella . Not too much of a problem for small amounts code, but it is for top-level functions that can be 1000x loc, so one mistake early in the code can cause a large comment/uncomment dance : /

[beurdouche]

Note, that I checked out earlier commits of the fstar-mode but it seems to happen as well, so I suspect there might have been some change in F* itself.

[beurdouche]

There is also something about the dependencies as the following code reports the error properly:

module Test

let test () =
  (if mistake then 0 else 1)

[cpitclaudel]

As you suspected, it's an F* bug; I'd recommend reporting it there.

Here's a transcript:

{"query-id":"1","query":"vfs-add","args":{"filename":null,"contents":"module Test\n\nlet test () =\n  (if mistake then IO.print_string \"Hello!\\n\"\n  else IO.print_string \"Clement\\n\")\n"}}
{"query-id":"2","query":"push","args":{"kind":"full","code":"module Test\n","line":1,"column":0}}
{"query-id":"3","query":"push","args":{"kind":"full","code":"\nlet test () =\n  (if mistake then IO.print_string \"Hello!\\n\"\n  else IO.print_string \"Clement\\n\")\n","line":2,"column":0}}

Saving that to test.transcript.in and running fstar --ide < test.transcript.in I get this in version e89fdf1 (3 months ago):

…
{"kind":"response","query-id":"1","status":"success","response":null}
…
{"kind":"response","query-id":"2","status":"success","response":[]}
{"kind":"response","query-id":"3","status":"failure","response":[{"level":"error","message":"Identifier not found: [mistake]","ranges":[{"fname":"<input>","beg":[4,6],"end":[4,13]}]}]}

but this in version a5e410c (master):

…
{"kind":"response","query-id":"1","status":"success","response":null}
…
{"kind":"response","query-id":"2","status":"success","response":[]}
{"kind":"response","query-id":"3","status":"failure","response":[{"level":"error","message":"Identifier not found: [mistake](Also see: <input>(4,6-4,13))","ranges":[{"fname":"/build/fstar/FStar/ulib/FStar.IO.fst","beg":[5,10],"end":[5,13]}]}]}

It shouldn't be too hard to bisect over the last three months to see which commit introduced the issue :)

Since the proper location is mentioned in the "see also" part, I could add a check to use that instead of the actual range, but I'd much rather have this issue fixed properly on the F* side (the range in FStar.IO.fst points to exception EOF, which doesn't seem relevant).

If you find the faulty commit, please add a test to the interactive test suite to prevent the issue from reoccurring :)

[beurdouche]

The faulty commit is 7c459c6dbd334f1e278e5ec691f37138bcd14ae0 (that is the ocaml snapshot commit though)

Hello @mtzguido ! Do you mind having a look at your commit and take appropriate action :) ?

[beurdouche]

Fixed by Guido in https://github.com/FStarLang/FStar/commit/e7460f059bce778fde24f08c6fc15060ce3deacb : ) Thanks !

[cpitclaudel]

Probably in https://github.com/FStarLang/FStar/commit/49b1b0ddcb36fc24f4ee0bebe26b8e1785c4cff1 actually. Thanks @mtzguido !