Custom Query (361 matches)

When electric-terminator is on, it's unclear how to enter an ellipsis (...) to invoke the default tactic in a "Proof with [tactic]" in Coq, except by disabling electric-terminator and re-enabling afterwards, which is inconvenient.

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)

If you have the below code, then place the caret at the end of the "Case" line and press Ctrl+J (or Enter, TAB), Emacs will spin up and use 100% of the CPU. This is on 4.1-RC4.

Theorem rev_snoc : forall X : Type, 
                     forall v : X,
                     forall s : list X,
  rev (snoc s v) = v :: (rev s).
Proof.
  simpl.
  intros X v s.
  induction s as [|s'].
  Case "s=nil".

  reflexivity.
  Qed.