fstar-mode opens new buffer upon errors

[kkohbrok]

This might be a design decision, but I find that opening a (new) split buffer to display error messages is a bit intrusive.
Type checking the following code in interactive-mode, it opens a new buffer to display the error instead of displaying it at the bottom of the existing buffer.

module Test

open FStar.Seq

type x = na

[cpitclaudel]

Can you try reproducign this in a clean Emacs (-Q)? The behavior your describe is not what fstar-mode does by default, so I'd tend to blame your config (Did you customize show-help-function?).

[kkohbrok]

Sorry, I'm not that familiar with emacs, which makes my config a likely candidate, however, the only thing that changed before those splits started appearing was an update of fstar-mode.
so what I did now was the following:

• get a clean .emacs and .emacs.d
• start emacs, install fstar-mode
• restart emacs, try verifying a file
  -> got the same error

I would also try it with emacs -Q, but I did not manage using/installing fstar-mode with that method.
Again, sorry for my inaptitude with emacs. I will gladly provide logs/configs, whatever you need.

[cpitclaudel]

Thanks for your help. I think a screenshot would help :) It might also be my config that makes things work nicely for me :)

[kkohbrok]

You have the config in the terminal on the left and minimal F* example on the right.
Upon pressing C-x C-n, the window splits and displays the warning on the lower buffer.
The behaviour is the same in X emacs (as opposed to emacs with the -nw flag that is visible in the screenshot).

[cpitclaudel]

Thanks, that clarifies it a lot :) This sounds like an F* issue, at least in part. F* mode warns you loudly (as you can see) when F* warns about an error in a file that isn't the current file. Here, F* claims that the error came from FStar.Seq.Properties.fst, which isn't the current file. @aseemr, ideas?

[kkohbrok]

I do get the same buffer split with warnings such as:

Warning (emacs): Non-empty response despite prover success: [(46,8-46,55): (Warning) Top-level let-bindings must be total; this term may have effects]

[cpitclaudel]

up; that one is on the fstar-mode side. When I originally wrote it, F* didn't issue warnings like this one. An update would be good. I wonder what the UI should be like, though: should the warnings persist (like errros?), or should they be displayed in the echo area and fade after a small amount of time? I'd guess persisting would be better, right?

[kkohbrok]

For my taste, I would like the warning to persist in the echo area. It would be nice to hear some more opinions on this, though. I guess it's a matter of preference/workflow.

[s-zanella]

@cpitclaudel: See #45 for F* reporting errors in other files (in that case, F* is to blame).
I prefer warnings to persist like errors do.

[cpitclaudel]

@s-zanella Woops, not sure how I missed that other thread. Thanks!
I'll close this issue when I implement support for (Warning) messages then, and we can track the other one in #45.

[markulf]

Persisting warnings is good. Maybe the mini-buffer should display the first error rather than the first warning, to ease navigation.

[cpitclaudel]

Ok, I've pushed a draft to https://github.com/FStarLang/fstar-mode.el/tree/46-warning-popups :) @kkohbrok, can you have a look? It should show warnings as orange underlines.

[kkohbrok]

Ok, so I removed the elpa pkg fstar-mode and manually loaded the patched fstar-mode.el version.
After going into fstar-mode, it still displays the warnings in a separate buffer.

[s-zanella]

@kkohbrok It seems that you're still using the unpatched version. Are you sure your Emacs is not loading a stale .elc file?

@cpitclaudel The behaviour improved somewhat for me: I no longer get a new Emacs windows for warnings, but warnings don't persist in the echo area as error messages do. Some warnings don't have proper location info (e.g. FStarLang/FStar#836), so they can go easily unnoticed since they will show only in the Messages buffer and there will be no highlighting in the source buffer.

[cpitclaudel]

@s-zanella Thanks for testing!

I tried FStarLang/FStar#836, and indeed I get unknown(0,0-0,0): (Warning) M: Unexpected output from Z3: (error "line 48305 column 20: unknown constant @x0"). What do you think we should do in that case? Highlight the entire overlay? (Currently it highlights the first character of the file)

Regarding persistence: can you post an example file? Thanks!

[s-zanella]

I completely missed the line under the first character!

All cases of unknown(0,0-0,0) warnings I know of are F* bugs. Depending on whether you want to make further bugs easier to be caught in fstar-mode, you can either highlight the whole overlay or do nothing.

Best to explain the persistence issue with pictures.
The first screenshot shows an error, with the persistent message in the echo area.
The second one shows a warning, with no indication in the echo area.

[cpitclaudel]

Thanks for the screenshot! Does C-h . bring the message back?

[s-zanella]

It doesn't.

[cpitclaudel]

Snap. I'll look into this :)

[kkohbrok]

@s-zanella you were right. I forgot to check out the correct branch.
It works for me now and looks like this:

[cpitclaudel]

@kkohbrok Thanks for testing. What you're seeing is still clearly not ideal, but it'll go away too once #45 is fixed.

[cpitclaudel]

@s-zanella Ah, that keybinding was introduced in Emacs 25. I pushed the corresponding change.
I also made sure that debugging messages are only printed to the *Messages* buffer, and not to the echo area. This should prevent the message from disappearing in the first place.

[s-zanella]

Thanks! Works great.
Those debug messages were annoying.

[cpitclaudel]

Thanks. I'll close this then :)
(The messages should be off by default, btw; do you have something turning fstar-subp-debug on or calling fstar-subp-toggle-debug in your .emacs?)

[s-zanella]

Yes, I did have a (setq fstar-subp-debug t). Forgot to turn it off.

[cpitclaudel]

I merged the warnings branch. Let me know if new errors pop up :)