Buffer coq-compile-response sometimes takes over the whole window

[proofgeneral]

Buffer coq-compile-response sometimes takes over the whole window

[RalfJung]

I have just also seen this happen in sequential background compilation mode.

[Matafou]

This happens every time the pg windows are messed up. I don't really understand when this happens. Sometimes the goals window takes the whole frame, sometimes its the compilation window. Workaround: type "M-x dedicated-mode" twice. If someone understand why windows do mess sometimes, we can fix this maybe.

[hendriktews]

maybe related to #42?

[hendriktews]

Do you still see the reported behavior? Can you give some more hints for reproducing?

@Matafou What do you mean with the "pg windows are messed up" ?

[RalfJung]

I did not do very much work with Coq recently, so I can't really tell... I don't actively remember seeing this recently, but I also don't think that means much. Sorry :/

[RalfJung]

I just saw this happen again, using (slightly outdated) PG 60dcd96

[hendriktews]

What PG configuration do you use, especially how many windows? Is coq-compile-response usually in a separate window?

The issue descriptions sounds like some dedicated-window property is getting in the way. When it happens the next time, can you try evaluating

 (set-window-dedicated-p (get-buffer-window coq-compile-response-buffer t) nil)

via eval-expression?

[RalfJung]

Here's my custom-set-variables:

 '(column-number-mode t)
 '(company-coq-prettify-symbols nil)
 '(coq-compile-before-require t)
 '(coq-compile-parallel-in-background t)
 '(coq-one-command-per-line nil)
 '(default-input-method "math")
 '(electric-indent-mode nil)
 '(fill-column 80)
 '(global-auto-revert-mode t)
 '(indent-tabs-mode nil)
 '(inhibit-startup-screen t)
 '(mf-display-padding-height 75)
 '(proof-follow-mode (quote followdown))
 '(proof-next-command-insert-space nil)
 '(proof-splash-enable nil)
 '(proof-three-window-enable t)
 '(reftex-plug-into-AUCTeX t)
 '(show-paren-mode t)
 '(standard-indent 4)
 '(tab-stop-list (quote (4 8)))
 '(tool-bar-mode nil))

If "window" here means "X11 window", then the answer this that all the three buffers are in the same window, the left left of which is taken over by the .v file, the right half is vertically split between *goals* and *response*. (Sorry I may not be using emacs terminology properly here.) This is what "Refresh Windows Layout" does here.

[RalfJung]

So it just happened again and I did the eval and it print nil. After this, I was able to switch the buffer on the left again to the .v file and use C-c C-l to get back to the normal view.

[hendriktews]

OK, this seems to confirm that the dedicated flag is the problem.

How about using C-x 0 (which invokes delete-window) or C-x 1 (delete-other-windows)? This works at least for me when three-window-mode messes up.

[hendriktews]

... I meant to use C-x 0 and C-x 1 until you have one emacs window left and then use C-x b to switch to you coq code and then use C-x 1?

[RalfJung]

Yeah, "C-x 0 C-C C-l" works to fix the mess. (Btw, currently, the issue seems to be 100% reproducible.)

[hendriktews]

Ralf Jung [email protected] writes:

(Btw, currently, the issue seems to be 100% reproducible.)

Would you mind telling how to reproduce?

[RalfJung]

• Check out https://gitlab.mpi-sws.org/FP/iris-coq.git
• Open prelude/orders.v
• Go to the first free line (the one right after the imports), C-c C-Ret (it will compile the dependencies)
• Open prelude/tactics.v and break the file (e.g. I added an s after the first Lemma on line 9, turning it into Lemmas) and save it
• Go back to prelude/orders.v, go to the first free line again and do C-c C-Ret

I am now getting the following Coq error displayed in the window where the .v file used to be:

-*- mode: compilation; -*-

/home/r/bin/coq-8.5/bin/coqc -Q ... iris .../prelude/tactics.v
File ".../prelude/tactics.v", line 9, characters 50-51:
Syntax error: '.' or '...' expected after [tactic:tactic] (in [proof_mode:subgoal_command]).

The layout is "messed up", I cannot switch buffers in this window, etc.

[hendriktews]

Just to confirm, after doing the final C-c C-Ret the emacs frame
is split vertically with coq-compile-response on the left. The
right side is split horizontally again with goals on top and
response below. You see the same?

BTW, the proper PG way to fix broken window layouts is
proof-layout-windows, usually bound to C-c C-l and in the menu
PG->Buffers-layout windows.

I just pushed a partial fix that makes this issue a bit less
critical. The coq-compile-response buffer should now not be in a
dedicated window.

A proper solution is a bit more involved. We first have to decide
where the coq-compile-response buffer should show up in
3-windows-mode:

• in the window of the response buffer
• in a new window
• somewhere else?

Then of course it should disappear again at the right time.

[RalfJung]

Just to confirm, after doing the final C-c C-Ret the emacs frame
is split vertically with coq-compile-response on the left. The
right side is split horizontally again with goals on top and
response below. You see the same?

I do.

BTW, the proper PG way to fix broken window layouts is
proof-layout-windows, usually bound to C-c C-l and in the menu
PG->Buffers-layout windows.

I know; however, that binding is not available when the coq-compile-response buffer is active.

I just pushed a partial fix that makes this issue a bit less
critical. The coq-compile-response buffer should now not be in a
dedicated window.

So this means I can just C-c C-b back to the buffer that I was in previously? That would indeed help a lot.

We first have to decide
where the coq-compile-response buffer should show up in
3-windows-mode:

I would think it should appear where Coq output always appears, in the bottom right quarter. I actually wasn't even aware that this is not the same buffer.

[hendriktews]

Ralf Jung [email protected] writes:

BTW, the proper PG way to fix broken window layouts is
proof-layout-windows, usually bound to C-c C-l and in the menu
PG->Buffers-layout windows.

I know; however, that command is not available when the
coq-compile-response buffer is active.

But it is bound in Goals and response, you could do C-x o first, right?

You can also always do M-x proof-layout-windows.

So this means I can just C-c C-b back to the buffer that I was in
previously? That would indeed help a lot.

Yes.

I would think it should appear where Coq output always appears, in the
bottom right quarter. I actually wasn't even aware that this is not
the same buffer.

I agree. The problem is to ensure the response buffer will show up in the same window when there is some response from the toplevel later on.

There are good reasons to have two different buffers. One shows response from the toplevel and the other shows standard output from coqc or coqdep. The latter one is in compilation-mode to enable the next-error feature.

[RalfJung]

But it is bound in Goals and response, you could do C-x o first, right?

I guess I could. Any reason it is not bound in coq-compile-response?

One shows response from the toplevel and the other shows standard output from coqc or coqdep. The latter one is in compilation-mode to enable the next-error feature.

I see. What is that next-error feature? If PG is able to automatically jump to where the background compilation error occurred, then I wasn't aware of that.

[hendriktews]

Ralf Jung [email protected] writes:

I guess I could. Any reason it is not bound in coq-compile-response?

Good point - no there is no reason.

I see. What is that next-error feature? If PG is able to automatically
jump to where the background compilation error occurred, then I wasn't
aware of that.

Yes, it's C-x `. There is not always a line number, but if there
is, it jumps to the error location.