Custom Query (361 matches)

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

Hello, here is how to reproduce the bug:

open a coq file (say toto.v). proof script one line. hit C-c C-x <enter> yes <enter>

and you get this:

Debugger entered--Lisp error: (error "Buffer toto.v has no process")

process-send-eof() scomint-send-eof() (if proof-shell-quit-cmd (scomint-send-string proc (concat proof-shell-quit-cmd "\n")) (scomint-send-eof)) (catch (quote exited) (set-process-sentinel proc (lambda ... ...)) (proof-deactivate-scripting-auto) (proof-shell-wait (proof-ass quit-timeout)) (if proof-shell-quit-cmd (scomint-send-string proc ...) (scomint-send-eof)) (let (... ...) (while ... ... ...)) (when (memq ... ...) (message "%s, cleaning up and exiting...killing process" bufname) (kill-process proc))) (progn (catch (quote exited) (set-process-sentinel proc ...) (proof-deactivate-scripting-auto) (proof-shell-wait ...) (if proof-shell-quit-cmd ... ...) (let ... ...) (when ... ... ...)) (set-process-sentinel proc nil)) (if (and alive proc) (progn (catch ... ... ... ... ... ... ...) (set-process-sentinel proc nil))) (when (and alive proc) (catch (quote exited) (set-process-sentinel proc ...) (proof-deactivate-scripting-auto) (proof-shell-wait ...) (if proof-shell-quit-cmd ... ...) (let ... ...) (when ... ... ...)) (set-process-sentinel proc nil)) (let* ((alive ...) (proc ...) (bufname ...)) (message "%s, cleaning up and exiting..." bufname) (redisplay t) (when (and alive proc) (catch ... ... ... ... ... ... ...) (set-process-sentinel proc nil)) (proof-script-remove-all-spans-and-deactivate) (proof-shell-clear-state) (run-hooks (quote proof-shell-kill-function-hooks)) (if (and proof-multiple-frames-enable proof-shell-fiddle-frames) (proof-delete-other-frames)) (let (...) (dolist ... ...)) (message "%s exited." bufname)) proof-shell-kill-function() kill-buffer(#<killed buffer>) (let ((kill-buffer-query-functions nil)) (kill-buffer proof-shell-buffer)) (progn (let (...) (kill-buffer proof-shell-buffer)) (setq proof-shell-buffer nil)) (if (or dont-ask (yes-or-no-p ...)) (progn (let ... ...) (setq proof-shell-buffer nil))) (when (or dont-ask (yes-or-no-p ...)) (let (...) (kill-buffer proof-shell-buffer)) (setq proof-shell-buffer nil)) (if (buffer-live-p proof-shell-buffer) (when (or dont-ask ...) (let ... ...) (setq proof-shell-buffer nil)) (error "No proof shell buffer to kill!")) proof-shell-exit() call-interactively(proof-shell-exit nil nil)

Current compilation errors:

  !! File error (("Cannot open load file" "phox-fun"))
  !! File error (("Cannot open load file" "phox-lang"))
  !! File error (("Cannot open load file" "plastic-syntax"))
  !! File error (("Cannot open load file" "twelf-font"))
  !! Wrong type argument ((symbolp (quote local-vars-list-doc)))
  !! Invalid argument (("Character set already defined for this DIMENSION/CHARS/FINAL/DIRECTION combo" #<charset indian-is13194 "IS 13194" "Indian IS 13194" "Generic Indian charset for data exchange with IS 13194" 94 l2r cols=2 g1 final='5' reg=IS13194-Devanagari 0x4489c>))
  !! Wrong type argument ((symbolp (quote local-vars-list-doc)))
  !! File error (("Cannot open load file" "phox-fun"))
  !! File error (("Cannot open load file" "phox-lang"))
  !! File error (("Cannot open load file" "plastic-syntax"))
  !! File error (("Cannot open load file" "twelf-font"))
  !! Wrong type argument ((symbolp (quote local-vars-list-doc)))