auto compile bugs when some outputs is done by coqc

[courtieu]

To reproduce the bug:

1) have in file foo.v the following:

Eval compute in 0.

2) Have in file bar.v the following:

Require Import foo.

3) then try to script bar.v (with auto-compilation on), compilation of foo.v is started automatically but then there is an error due to the read-only status of coq-compile-response buffer. I think this is due to the fact that coqc compilation *does* the output.

Cheers, P.

---

excerpt of buffer *Messages*:

Check /home/courtieu/titi.vo Recompile /home/courtieu/titi.v Waiting for process to die...done condition-case: Buffer is read-only: #<buffer *coq-compile-response*>

[coquser]

an error due to the read-only status of coq-compile-response buffer. I think this is due to the fact that coqc compilation *does* the output.

I cannot reproduce this problem with emacs 23.2.1 and current Proof General cvs head. When I try there is no error and *coq-compile-respose* contains

-*- mode: compilation; -*-

/usr/local/bin/coqc -I /home/tews/coq/ /home/tews/coq/a.v

0

: nat

In my emacs version call-process does not pay attention to the read-only status of a buffer. What emacs version do you use?

Please try the following:

• assert some Require command with auto-compilation to make sure the *coq-compile-response* buffer does exist
• do M-x eval-expression

(call-process "/bin/cat" "/proc/cpuinfo" "*coq-compile-response*" t)

• check that *coq-compile-response* contains the contents of /proc/cpuinfo

Additionally, can you try to reproduce the bug with coq-debug-auto-compilation set to t? What messages are generated? What is the contents of *coq-compile-response*? Please cvs update before you try, because I fixed coq-debug-auto-compilation.

Bye,

Hendrik

[coquser]

only accidently closed

[courtieu]

Hi,

I have emacs 23.1.1 and I still have this error.

I cannot reproduce this problem with emacs 23.2.1 and current Proof General cvs head. When I try there is no error and *coq-compile-respose* contains

-*- mode: compilation; -*- /usr/local/bin/coqc -I /home/tews/coq/ /home/tews/coq/a.v

0 : nat

My *coq-compile-response* buffer also contains this.

(call-process "/bin/cat" "/proc/cpuinfo" "*coq-compile-response*" t)

This also gives me the same read-only error.

check that *coq-compile-response* contains the > contents of

/proc/cpuinfo

it does.

Here is the output I get with 1) starting emacs with -q option, 2) loading pg then 3) set debug on 4) set auto compile on 5) trying to script bar.v

Pierre

---

Loading 00debian-vars...done Loading /etc/emacs23/site-start.d/50auctex.el (source)... Loading /usr/share/emacs/23.1/site-lisp/auctex.el (source)...done Loading /usr/share/emacs/23.1/site-lisp/preview-latex.el (source)...done Loading /etc/emacs23/site-start.d/50auctex.el (source)...done Loading /etc/emacs/site-start.d/50autoconf.el (source)...done Loading /etc/emacs/site-start.d/50dictionaries-common.el (source)... Loading debian-ispell... Loading /var/cache/dictionaries-common/emacsen-ispell-default.el (source)...done Loading debian-ispell...done Loading /var/cache/dictionaries-common/emacsen-ispell-dicts.el (source)...done Loading /etc/emacs/site-start.d/50dictionaries-common.el (source)...done Loading /etc/emacs/site-start.d/50el-get.el (source)...done Loading /etc/emacs/site-start.d/50emacs-goodies-el.el (source)...done Loading /etc/emacs/site-start.d/50festival.el (source)...done Loading /etc/emacs/site-start.d/50git-core.el (source)...done Loading /etc/emacs/site-start.d/50magit.el (source)...done Loading /etc/emacs/site-start.d/50ocaml-mode.el (source)...done Loading /etc/emacs/site-start.d/50prolog-el.el (source)...done Loading /etc/emacs/site-start.d/50psvn.el (source)...done Loading /etc/emacs/site-start.d/51tuareg-mode.el (source)...done For information about GNU Emacs and the GNU system, type C-h C-a. Loading /home/courtieu/pg/actual/coq/coq.el (source)... Source file `/home/courtieu/pg/actual/coq/coq-abbrev.el' newer than byte-compiled file Coq abbrevs already exists, default not loaded Loading /home/courtieu/pg/actual/coq/coq.el (source)...done Starting: /home/courtieu/coq/actual/bin/coqtop -emacs-U M-x proof-prf for goals; M-x proof-display-some-buffers rotates output; M-x proof-layout-windows refreshes [2 times] Starting coq process... done. (No files need saving) call coqdep arg list: (-I /home/courtieu/coq/bugs/ /tmp/ProofGeneral-coq2793JAY.v) coqdep output on /tmp/ProofGeneral-coq2793JAY.v: /tmp/ProofGeneral-coq2793JAY.vo /tmp/ProofGeneral-coq2793JAY.glob: /tmp/ProofGeneral-coq2793JAY.v /home/courtieu/coq/bugs/foo.vo

Check /home/courtieu/coq/bugs/foo.vo call coqdep arg list: (-I /home/courtieu/coq/bugs/ /home/courtieu/coq/bugs/foo.v) coqdep output on /home/courtieu/coq/bugs/foo.v: /home/courtieu/coq/bugs/foo.vo /home/courtieu/coq/bugs/foo.glob: /home/courtieu/coq/bugs/foo.v

Recompile /home/courtieu/coq/bugs/foo.v call coqc arg list: (-I /home/courtieu/coq/bugs/ /home/courtieu/coq/bugs/foo.v) Waiting for process to die...done condition-case: Buffer is read-only: #<buffer *coq-compile-response*> Mark set byte-code: Beginning of buffer [3 times] byte-code: Beginning of buffer

[courtieu]

I just tested with 23.3.1, the bug is still there.

[David Aspinall]

I am on 23.3.1, I cannot reproduce this either, I see the same as Hendrik.

Pierre, your Emacs is loading a lot of non-standard stuff. Can you try from emacs -q -no-site-file and see if you can still reproduce?

[coquser]

I installed several packages, such that my Emacs now loads a superset of the files that Pierres Emacs loads. But I can still not reproduce this bug (with Emacs 23.2.1 on Debian squeeze).

I find it very strange that you get a read-only error although the buffer contains the expected material. This sounds like some advice or hook is trying to modify *coq-compile-response* after call-process modified it.

What does the emacs debugger say, if you execute {{{(call-process "/bin/cat" "/proc/cpuinfo" "*coq-compile-response*" t)}}} as described above?

Hendrik

[coquser]

After a bug hunting session with together with Pierre, we came to the conclusion to blame the Emacs in Debian Sid unstable. There, call-process seems to trigger some hook which gives the buffer-read-only-error. For the time being a simple workaround is wrap all call-process calls with (let ((inhibit-read-only t)) .. ) .

[coquser]

In order to check for the bug eval

(let ((buf (get-buffer-create "xxx")))
  (with-current-buffer buf 
    (compilation-mode))
  (condition-case err
      (progn 
	(call-process "/bin/cat" 
		      "/proc/cpuinfo"
		      buf
		      t)
	(message "No call-process error"))
    (error
     (message "call-process error: %s %s" (car err) (cdr err)))))

in a fresh, vanilla Emacs. Normal Emacsen give no error on this, but Pierre's Emacs does.

The plan is now to check whether the problem does also show up in the newest emacs version in Debian unstable, and, if yes, to submit a bug report to debian.

I tried emacs-23.1 and emacs-23.3a from GNU, no one showing the error.

Hendrik

[coquser]

Finally I found out that call-process changes its behavior wrt. read-only buffers depending on the coding system for read operations. Using a non-utf8 locale triggers the bad case, see debian bug #651420.

If you have problems with this consider using an utf8 locale, eg

export LANG=en_US.UTF-8

[David Aspinall]

Closing this. The link to the Debian bug discussion is here: ​http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=651420