Opened 9 years ago

Closed 9 years ago

#408 closed defect (fixed)

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

Reported by: Erik Martin-Dorel Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-4.1
Component: 2:pg-emacs Keywords:
Cc: Erik Martin-Dorel


To reproduce the bug:

  1. Create an empty file one.v, using for example [M-! touch one.v];
  1. Create another file two.v with the text
Require Import one.
  1. Ensure coq-compile-before-require is true, then script two.v;

the automatic compilation succeeds.

  1. Modify one.v, for example by writing something like
Require Export List.
  1. 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

Change History (5)

comment:1 Changed 9 years ago by David Aspinall

Resolution: fixed
Status: newclosed

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.

comment:2 in reply to:  1 Changed 9 years ago by Erik Martin-Dorel

Resolution: fixed
Status: closedreopened

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* ;

  1. 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,


comment:3 Changed 9 years ago by David Aspinall

Priority: majorminor
Resolution: needmoreinfo
Status: reopenedclosed

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.

comment:4 Changed 9 years ago by coquser

Resolution: needmoreinfo
Status: closedreopened

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.


comment:5 Changed 9 years ago by coquser

Resolution: fixed
Status: reopenedclosed

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.


Note: See TracTickets for help on using tickets.