fstar-mode opens new buffer upon errors about fstar-mode.el HOT 26 CLOSED

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

from fstar-mode.el.

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

from fstar-mode.el.

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?).

from fstar-mode.el.

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.

from fstar-mode.el.

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

from fstar-mode.el.

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).

from fstar-mode.el.

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?

from fstar-mode.el.

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]

from fstar-mode.el.

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?

from fstar-mode.el.

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.

from fstar-mode.el.

@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.

from fstar-mode.el.

@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.

from fstar-mode.el.

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

from fstar-mode.el.

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.

from fstar-mode.el.

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.

from fstar-mode.el.

@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.

from fstar-mode.el.

@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!

from fstar-mode.el.

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.

from fstar-mode.el.

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

from fstar-mode.el.

It doesn't.

from fstar-mode.el.

Snap. I'll look into this :)

from fstar-mode.el.

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

from fstar-mode.el.

@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.

from fstar-mode.el.

Thanks! Works great.
Those debug messages were annoying.

from fstar-mode.el.

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?)

from fstar-mode.el.

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

from fstar-mode.el.