Auto compile fails if coq-compile-response-buffer has been killed

[Erik Martin-Dorel]

To reproduce the bug:

1. Create an empty file one.v, using for example [M-! touch one.v];

2. Create another file two.v with the text

Require Import one.

3. Ensure coq-compile-before-require is true, then script two.v;

the automatic compilation succeeds.

4. Modify one.v, for example by writing something like

Require Export List.

5. Kill buffer *coq-compile-response*, then script again two.v;

the compilation fails with error

condition-case: Selecting deleted buffer

Thanks to the help of the Emacs debugger, I have found the source of the bug:

In function coq-init-compile-response-buffer from coq/coq.el, the first test

(if (bufferp coq-compile-response-buffer)
    …
  …)

is problematic as in this particular state, coq-compile-response-buffer is neither nil nor a relevant buffer value (namely, it is #<killed buffer>, for which bufferp holds).

Moreover, coq-init-compile-response-buffer must beheave well if the user has opened buffer *coq-compile-response* by hand while coq-compile-response-buffer is still nil or #<killed buffer>.

To conclude, I guess we ought to write something like

(if (setq coq-compile-response-buffer
          (get-buffer coq-compile-response-buffer-name))
    …
  …)

to fix both problems.

Kind regards,

Erik Martin-Dorel

[David Aspinall]

Thanks for the report and investigation.

I think buffer-live-p instead of buffer-p ought to do the trick here. I've committed this as a fix, please reopen if you disagree.

[Erik Martin-Dorel]

Replying to da:

Thanks for the report and investigation.

I think buffer-live-p instead of buffer-p ought to do the trick here. I've committed this as a fix, please reopen if you disagree.

I reopen the ticket since using buffer-live-p solves only part of the problems at stake.

Indeed, the function coq-init-compile-response-buffer won't beheave very well in the following situations:

1. If the user has renamed *coq-compile-response* into

*coq-compile-response*<2> (using for example M-x rename-uniquely), he should expect the auto-compile responses does not alter the renamed buffer any more, as M-x shell-command beheaves w.r.t. the buffer *Shell Command Output* ;

2. If the user has killed *coq-compile-response*, reopened it and

modified its content, (buffer-live-p coq-compile-response-buffer) won't hold as coq-compile-response-buffer equals #<killed buffer>, and yet the buffer does exist, is nonempty, and should be erased by the function coq-init-compile-response-buffer...

Hence the piece of code (if (setq ..) ..) I have suggested just now.

Kind regards,

Erik

[David Aspinall]

Thanks Erik. Personally I find some of the situations you're suggesting a bit bizarre but there's no predicting what Emacs users will like to do! We did put code into PG to protect around the response buffer etc being killed.

Could you upload a patch? I don't really understand the around if because it seems like the test will always succeed.

[coquser]

When I wrote the code I considered *coq-compile-response* an internal buffer, which the user should not touch. Therefore I used the optimization to store the buffer object in the extra variable coq-compile-response-buffer. Then, of course, if the user starts renaming/changing *coq-compile-response*, there are all kinds of inconsistencies between coq-compile-response-buffer-name and coq-compile-response-buffer.

I'll fix this as follows: get rid of coq-compile-response-buffer and access *coq-compile-response* always via its buffer name in coq-compile-response-buffer-name.

Hendrik

[coquser]

Killing and renaming *coq-compile-response* is now possible. The next compilation will put error messages always into the buffer in coq-compile-response-buffer.

If the user creates *coq-compile-response* it is his duty to set an appropriate major mode. If the major mode is wrong, next-error does not work.

Set state to fixed, hopefully forever now.

Hendrik