Custom Query (361 matches)

The new addition

(define-key coq-mode-map (kbd ".") 'coq-colon-self-insert)

hides the generic default (proof-electric-terminator) and there is no configure option.

Hendrik

Proof general seems to stall when trying to evaluate very long (textually long) ltac declarations. See example at the end. If you remove a line or two of the "let x := match ... in" then there is no problem. Is there a limit to the size of expressions that are fed to Coq?

Ltac bar k := k tt.

Ltac foo x := 
  bar ltac:(fun a => 
  bar ltac:(fun b => 
  bar ltac:(fun c => 
  bar ltac:(fun d => 
  bar ltac:(fun e => 
  bar ltac:(fun f => 
  bar ltac:(fun g => 
  bar ltac:(fun h => 
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  idtac)))))))).

When starting PG on a .v file, or when switching from one file to another (i.e., retract current buffer, and go to point in another one), PG, generates the following error, repeatedly.

error in process filter: progn: Wrong type argument: window-live-p, nil error in process filter: Wrong type argument: window-live-p, nil

It eventually stops and behaves normally after a few seconds (1 to ten -- it seems to become longer and longer along with the process lifetime). A backtrace is included below.

I'm using the current cvs version of PG, with Aquamacs 2.4 (Emacs 23.3.50.1 inside).

Best, Damien

Debugger entered--Lisp error: (wrong-type-argument window-live-p nil)

select-window(nil norecord) (progn (select-window (get-buffer-window proof-script-buffer) (quote norecord)) (- (window-height) window-min-height)) (unwind-protect (progn (select-window ... ...) (- ... window-min-height)) (dolist (elt save-selected-window-alist) (and ... ... ...)) (when (window-live-p save-selected-window-window) (select-window save-selected-window-window ...))) (save-current-buffer (unwind-protect (progn ... ...) (dolist ... ...) (when ... ...))) (let ((save-selected-window-window ...) (save-selected-window-alist ...)) (save-current-buffer (unwind-protect ... ... ...))) (with-selected-window (get-buffer-window proof-script-buffer) (- (window-height) window-min-height)) (let ((maxhgth ...) hgt-resp nline-resp) (with-selected-window (get-buffer-window proof-response-buffer) (setq hgt-resp ...) (with-current-buffer proof-response-buffer ...) (unless ... ...) (with-current-buffer proof-response-buffer ... ...))) (progn (let (... hgt-resp nline-resp) (with-selected-window ... ... ... ... ...))) (if (and proof-three-window-enable (> ... 10) (get-buffer-window proof-response-buffer)) (progn (let ... ...))) (when (and proof-three-window-enable (> ... 10) (get-buffer-window proof-response-buffer)) (let (... hgt-resp nline-resp) (with-selected-window ... ... ... ... ...))) optim-resp-windows() run-hooks(proof-shell-handle-delayed-output-hook) (let ((start proof-shell-delayed-output-start) (end proof-shell-delayed-output-end) (flags proof-shell-delayed-output-flags)) (goto-char start) (cond (... ...) (t ... ...)) (run-hooks (quote proof-shell-handle-delayed-output-hook))) proof-shell-handle-delayed-output() (setq proof-shell-last-output-kind (proof-shell-handle-delayed-output)) (if (proof-shell-exec-loop) (setq proof-shell-last-output-kind (proof-shell-handle-delayed-output))) (if proof-shell-last-output-kind nil (setq proof-shell-delayed-output-start start) (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if (proof-shell-exec-loop) (setq proof-shell-last-output-kind ...)) (if proof-tree-external-display (proof-tree-handle-delayed-output cmd flags span))) (unless proof-shell-last-output-kind (setq proof-shell-delayed-output-start start) (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if (proof-shell-exec-loop) (setq proof-shell-last-output-kind ...)) (if proof-tree-external-display (proof-tree-handle-delayed-output cmd flags span))) (let ((span ...) (cmd ...) (flags ...)) (setq proof-shell-last-output (buffer-substring-no-properties start end)) (proof-shell-handle-immediate-output cmd start end flags) (unless proof-shell-last-output-kind (setq proof-shell-delayed-output-start start) (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if ... ...) (if proof-tree-external-display ...))) proof-shell-filter-manage-output(648 648) (progn (setq endpos (match-beginning 0)) (setq proof-shell-last-prompt (buffer-substring-no-properties endpos ...)) (goto-char (point-max)) (proof-shell-filter-manage-output startpos endpos)) (if (re-search-forward proof-shell-annotated-prompt-regexp nil t) (progn (setq endpos ...) (setq proof-shell-last-prompt ...) (goto-char ...) (proof-shell-filter-manage-output startpos endpos))) (let ((urgnt ...) (prev-prompt pos) (startpos pos) endpos) (goto-char pos) (if (and urgnt ...) (setq startpos ...) (if ... ... ...)) (if (re-search-forward proof-shell-annotated-prompt-regexp nil t) (progn ... ... ... ...))) (if proof-action-list (let (... ... ... endpos) (goto-char pos) (if ... ... ...) (if ... ...)) (if proof-shell-busy (progn ... ...))) (if (not pos) (proof-shell-filter-first-command) (if proof-action-list (let ... ... ... ...) (if proof-shell-busy ...))) (let ((pos ...)) (if (not pos) (proof-shell-filter-first-command) (if proof-action-list ... ...))) (save-excursion (and proof-shell-eager-annotation-start (proof-shell-process-urgent-messages)) (let (...) (if ... ... ...)))

proof-shell-filter("\n<prompt>Coq < 9 run-hook-with-args(proof-shell-filter "\n<prompt>Coq < 9

0 < </prompt>")

0 < </prompt>")

(let ((saved-point ...)) (goto-char (process-mark process)) (set-marker scomint-last-output-start (point)) (insert string) (set-marker (process-mark process) (point)) (goto-char saved-point) (run-hook-with-args (quote scomint-output-filter-functions) string) (set-marker saved-point (point))) (save-current-buffer (set-buffer oprocbuf) (let (...) (goto-char ...) (set-marker scomint-last-output-start ...) (insert string) (set-marker ... ...) (goto-char saved-point) (run-hook-with-args ... string) (set-marker saved-point ...))) (with-current-buffer oprocbuf (let (...) (goto-char ...) (set-marker scomint-last-output-start ...) (insert string) (set-marker ... ...) (goto-char saved-point) (run-hook-with-args ... string) (set-marker saved-point ...))) (progn (with-current-buffer oprocbuf (let ... ... ... ... ... ... ... ...))) (if (and string (buffer-live-p oprocbuf)) (progn (with-current-buffer oprocbuf ...))) (when (and string (buffer-live-p oprocbuf)) (with-current-buffer oprocbuf (let ... ... ... ... ... ... ... ...))) (let ((oprocbuf ...)) (when (and string ...) (with-current-buffer oprocbuf ...)))

scomint-output-filter(#<process coq> "\n<prompt>Coq < 9

0 < </prompt>")

accept-process-output(#<process coq> 0.01 nil 1) (while (and proof-shell-busy (not quit-flag) (if timecount ... t) (not ...)) (accept-process-output proverproc accepttime nil 1)) (progn (while (and proof-shell-busy ... ... ...) (accept-process-output proverproc accepttime nil 1)) (redisplay) (if quit-flag (error "Proof General: quit in proof-shell-wait"))) (if proverproc (progn (while ... ...) (redisplay) (if quit-flag ...))) (when proverproc (while (and proof-shell-busy ... ... ...) (accept-process-output proverproc accepttime nil 1)) (redisplay) (if quit-flag (error "Proof General: quit in proof-shell-wait"))) (let* ((proverproc ...) (accepttime 0.01) (timecount ...)) (when proverproc (while ... ...) (redisplay) (if quit-flag ...))) proof-shell-wait() (progn (message "%s buffer %s..." name buf) (funcall fn) (proof-shell-wait) (message "%s buffer %s...done." name buf) (sit-for 0)) (unwind-protect (progn (message "%s buffer %s..." name buf) (funcall fn) (proof-shell-wait) (message "%s buffer %s...done." name buf) (sit-for 0)) (unless (proof-action-completed action) (error "%s of %s failed!" name buf))) (let ((fn ...) (name ...)) (unwind-protect (progn ... ... ... ... ...) (unless ... ...))) (if (proof-action-completed action) nil (let (... ...) (unwind-protect ... ...))) (unless (proof-action-completed action) (let (... ...) (unwind-protect ... ...))) (save-current-buffer (set-buffer buf) (unless (proof-action-completed action) (let ... ...))) (with-current-buffer buf (unless (proof-action-completed action) (let ... ...))) (let ((buf ...)) (with-current-buffer buf (unless ... ...))) proof-protected-process-or-retract(retract) (if action (proof-protected-process-or-retract action)) (let* ((complete ...) (action ...)) (if action (proof-protected-process-or-retract action)) (unless (and ... ...) (setq proof-previous-script-buffer proof-script-buffer) (setq proof-script-buffer nil) (if ... ...) (if ... ...) (setq proof-active-buffer-fake-minor-mode nil) (force-mode-line-update) (run-hooks ...))) (save-current-buffer (set-buffer proof-script-buffer) (let* (... ...) (if action ...) (unless ... ... ... ... ... ... ... ...))) (with-current-buffer proof-script-buffer (let* (... ...) (if action ...) (unless ... ... ... ... ... ... ... ...))) (if (buffer-live-p proof-script-buffer) (with-current-buffer proof-script-buffer (let* ... ... ...))) (proof-with-current-buffer-if-exists proof-script-buffer (let* (... ...) (if action ...) (unless ... ... ... ... ... ... ... ...))) proof-deactivate-scripting() (progn (proof-deactivate-scripting) (if proof-script-buffer (error "You cannot have more than one active scripting buffer!"))) (if proof-script-buffer (progn (proof-deactivate-scripting) (if proof-script-buffer ...))) (when proof-script-buffer (proof-deactivate-scripting) (if proof-script-buffer (error "You cannot have more than one active scripting buffer!"))) (save-excursion (when proof-script-buffer (proof-deactivate-scripting) (if proof-script-buffer ...)) (proof-unregister-buffer-file-name (quote tell-the-prover)) (if proof-script-buffer (proof-deactivate-scripting)) (assert (null proof-script-buffer) "Bug in proof-activate-scripting: deactivate failed.") (proof-shell-ready-prover queuemode) (setq proof-script-buffer (current-buffer)) (if (proof-locked-region-empty-p) (proof-init-segmentation)) (setq proof-active-buffer-fake-minor-mode t) (force-mode-line-update) (if (and proof-query-file-save-when-activating-scripting ...) (save-some-buffers nil ...)) (if proof-activate-scripting-hook (let ... ... ... ...))) (if (equal (current-buffer) proof-script-buffer) nil (save-excursion (when proof-script-buffer ... ...) (proof-unregister-buffer-file-name ...) (if proof-script-buffer ...) (assert ... "Bug in proof-activate-scripting: deactivate failed.") (proof-shell-ready-prover queuemode) (setq proof-script-buffer ...) (if ... ...) (setq proof-active-buffer-fake-minor-mode t) (force-mode-line-update) (if ... ...) (if proof-activate-scripting-hook ...))) (unless (equal (current-buffer) proof-script-buffer) (save-excursion (when proof-script-buffer ... ...) (proof-unregister-buffer-file-name ...) (if proof-script-buffer ...) (assert ... "Bug in proof-activate-scripting: deactivate failed.") (proof-shell-ready-prover queuemode) (setq proof-script-buffer ...) (if ... ...) (setq proof-active-buffer-fake-minor-mode t) (force-mode-line-update) (if ... ...) (if proof-activate-scripting-hook ...))) proof-activate-scripting(nil advancing) proof-assert-until-point() (if (> (proof-queue-or-locked-end) (point)) (proof-retract-until-point) (if (proof-only-whitespace-to-locked-region-p) (progn ... ...)) (proof-assert-until-point)) (save-excursion (if (> ... ...) (proof-retract-until-point) (if ... ...) (proof-assert-until-point))) proof-goto-point() call-interactively(proof-goto-point nil nil)