search

FStarLang / fstar-mode.el

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

"Main" vs. "related" error locations #59

Closed nikswamy closed 7 years ago

nikswamy commented 7 years ago

Hi Clement,

Consider this program:

module Test
assume val test : x:int{x >= 0} -> Type0
assume val f : x:int -> test x

It has a verification error on the last occurrence of x, since we can't prove that x>=0 as required by the type of test.

If you run this program through F*'s batch mode, it says:

.\test.fst(3,29-3,30): (Error) Subtyping check failed; expected type (x:int{ b2t (x >= 0) }); got type int (see also .\test.fst(2,24-2,30))

i.e., the "main" error location reported (\test.fst(3,29-3,30)) is on the last occurrence of x (as expected), but it also reports a "related" source location (.\test.fst(2,24-2,30)), which corresponds to the x >= 0 refinement formula in the type of test.

Using fstar --ide and fstar-mode.el we see different behavior:

The main error location presented in editor is actually the "related" source location, i.e., \test.fst(2,24-2,30). I have a patch in fstar to fix this so that it instead reports the main location as .\test.fst(3,29-3,30). That's easy and I'll push it to fstar shortly.

Now, to the main point of this issue: by presenting only the main error location, the editor doesn't show the useful information in the related location. Would it be possible in fstar-mode.el to associate with each main error location its corresponding related location? For instance, we could put a squiggly on the main error location (as we do now) but if the user places their cursor on the squiggly, then perhaps we could peek at the text reported in the related error location? Or, provide a way for the user to jump to the related location etc.

What do you think?

nikswamy commented 7 years ago

Update:

I just pushed a change to FStarLang/FStar master so that it now responds like this:

{"kind":"response","query-id":"4","status":"failure","response":[{"level":"error","message":"Subtyping check failed; expected type (x:int{ b2t (x >= 0) }); got type int","ranges":[{"fname":"<input>","beg":[5,29],"end":[5,30]}],"related_ranges":[{"fname":"<input>","beg":[2,24],"end":[2,30]}]}]}

Notice the new field "related_ranges". I checked that fstar-mode.el safely ignores them right now. But, it would be great if it could show those related ranges somehow to the user.

cpitclaudel commented 7 years ago

I think that's great, and in fact I already have some ad-hoc support for that because @fournet requested that https://github.com/FStarLang/fstar-mode.el/issues/56.

I initially created https://github.com/FStarLang/FStar/issues/998, but quick attempts at propagating the data that was encoded in "see also" proved to require changes in a large fraction of the code, so I miostly gave up, and instead went for a solution on the fstar-mode side: In the currently available code (since https://github.com/FStarLang/fstar-mode.el/commit/ed1163f3db491e99ed0d0fbd5bcff98988008ebd), if an error message includes "see also …", fstar-mode will parse that location and let you jump to it using C-c C-' (it's in the README under "browse to secondary location of current error").

Of course, a properly structured error location is much better than the current regexp-based parsing, so the change is very welcome :) Two quick questions:

(Bonus: if you just move the related range into the "ranges" list, everything should already be supported by fstar-mode :)

cpitclaudel commented 7 years ago

Can we put the related range in the existing "ranges" field? I originally made it a list precisely so that we could include more than one location (the idea being that the first location was the important one, and the other ones the secondary (related) locations).

I'll make a PR for this.

cpitclaudel commented 7 years ago

Merged, so nothing more to do on the fstar-mode side ATM.