Dear Maintainer,

I have the option to automatically compiled dependant Coq files in import enabled. However,
when there is an error compiling these files, ProofGeneral does not show that error. Instead,
the following appears in the minibuffer at the bottom:

  Buffer is read-only: #<buffer *coq-compile-response*>

This used to work fine quite a while ago, but at some point, it broke.

Kind regards,
Ralf

Thanks for reporting this.

I remember having problems with this when I originally wrote the
compilation feature for Coq. IIRC, the problem is that there is
no clear interface for inserting text in write protected buffers.
Probably the hack that I used for this broke in the newest emacs
version. I have to check this.

Bye,

Hendrik

Hi,

Weird enough, it shows that error even when there is nothing to do: A
"make" of the respective .vo files says they are up-to-date, and
disabling the automatic compilation of dependent files works around the
issue. I don't know how that makes sense.

The current "upstream" ProofGeneral snapshot (150202) also has the same
issue. However, after enabling concurrent compilation of dependent
files, things are working - errors reported by Coq are shown in emacs.
Again, I don't know how that makes sense.

Kind regards,
Ralf

Ralf Jung <post@ralfj.de> writes:

This might be because the buffer is always initialized, see
coq-init-compile-response-buffer.

Looking quickly over the code, all usages of this buffer seem to
be guarded with (inhibit-read-only t), which should disable the
read-only check. I don't know what is going on, I have to look
more carefully.

Bye,

Hendrik

Hi,
there is nothing to do. Often, things just work as long as there is no
error from Coq.

As far as I'm concerned, the issue is not really pressing - since
everything is all right with concurrent compilation.

Kind regards,
Ralf