Custom Query (361 matches)

When starting the coq process, I get an error (wrong-type-argument stringp nil) displayed in the mini-buffer. It keeps flashing, as if it were repeated. If I "C-g" then I can start using Proof General normally, with no further problem.

This is with Aquamacs 2.4 and Proof General Emacs 4.2

Here is a debugger trace.

Debugger entered--Lisp error: (wrong-type-argument stringp nil)
  get-buffer(nil)
  switch-to-buffer(nil)
  (let* ((nbgoals ...) (dummy ...) (toclean ...)) (while toclean (setq minor-mode-alist ...) (setq toclean ...)) (setq minor-mode-alist (append ... minor-mode-alist)))
  (save-window-excursion (switch-to-buffer proof-goals-buffer) (let* (... ... ...) (while toclean ... ...) (setq minor-mode-alist ...)))
  coq-update-minor-mode-alist()
  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 ...)))
  (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 ...)))
  (let ((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 ... ...)))
  proof-shell-filter-manage-output(226 226)
  (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 < 2 || 0 < </prompt>")
  run-hook-with-args(proof-shell-filter "\n<prompt>Coq < 2 || 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 < 2 || 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()
  (if wait (proof-shell-wait))
  (progn (unless (or ... ... ...) (setq cmd ...)) (if wait (proof-shell-wait)) (proof-shell-ready-prover) (let* (...) (proof-start-queue nil nil ...)) (if wait (proof-shell-wait)))
  (if cmd (progn (unless ... ...) (if wait ...) (proof-shell-ready-prover) (let* ... ...) (if wait ...)))
  proof-shell-invisible-command("Unset Printing All. " t)
  (lambda (c) (proof-shell-invisible-command c t))("Unset Printing All. ")
  mapcar((lambda (c) (proof-shell-invisible-command c t)) ("Unset Printing All. " "Unset Printing Implicit. " "Unset Printing Coercions. " "Set Printing Wildcard. " "Set Printing Synth. " "Set Printing Depth 50 . " "Set Undo 200 . "))
  (if proof-assistant-settings (mapcar (lambda ... ...) (proof-assistant-settings-cmds)))
  (progn (run-hooks (quote proof-shell-init-hook)) (when proof-shell-init-cmd (if ... ... ...)) (proof-shell-wait) (if proof-assistant-settings (mapcar ... ...)))
  (unwind-protect (progn (run-hooks ...) (when proof-shell-init-cmd ...) (proof-shell-wait) (if proof-assistant-settings ...)))
  (progn (setq proof-action-list nil) (proof-maybe-askprefs) (unwind-protect (progn ... ... ... ...)))
  (if (memq (process-status proc) (quote ...)) (progn (setq proof-action-list nil) (proof-maybe-askprefs) (unwind-protect ...)))
  (let ((proc ...)) (add-hook (quote kill-buffer-hook) (quote proof-shell-kill-function) t t) (set-process-sentinel proc (quote proof-shell-bail-out)) (if proof-shell-pre-sync-init-cmd (proof-shell-insert proof-shell-pre-sync-init-cmd ...)) (while (and ... ...) (accept-process-output proc 1)) (if (memq ... ...) (progn ... ... ...)))
  (save-current-buffer (set-buffer proof-shell-buffer) (dolist (sym proof-shell-important-settings) (proof-warn-if-unset "proof-shell-config-done" sym)) (setq font-lock-defaults (quote ...)) (set (make-local-variable ...) (list ... proof-mode-for-shell)) (let (...) (add-hook ... ... t t) (set-process-sentinel proc ...) (if proof-shell-pre-sync-init-cmd ...) (while ... ...) (if ... ...)))
  (with-current-buffer proof-shell-buffer (dolist (sym proof-shell-important-settings) (proof-warn-if-unset "proof-shell-config-done" sym)) (setq font-lock-defaults (quote ...)) (set (make-local-variable ...) (list ... proof-mode-for-shell)) (let (...) (add-hook ... ... t t) (set-process-sentinel proc ...) (if proof-shell-pre-sync-init-cmd ...) (while ... ...) (if ... ...)))
  proof-shell-config-done()
  coq-shell-mode-config()
  (let ((delay-mode-hooks t)) (proof-shell-mode) (setq major-mode (quote coq-shell-mode)) (setq mode-name "Coq Shell") (progn (if ... ...) (unless ... ...) (let ... ...)) (use-local-map coq-shell-mode-map) (set-syntax-table coq-shell-mode-syntax-table) (setq local-abbrev-table coq-shell-mode-abbrev-table) (coq-shell-mode-config))
  (progn (make-local-variable (quote delay-mode-hooks)) (let (...) (proof-shell-mode) (setq major-mode ...) (setq mode-name "Coq Shell") (progn ... ... ...) (use-local-map coq-shell-mode-map) (set-syntax-table coq-shell-mode-syntax-table) (setq local-abbrev-table coq-shell-mode-abbrev-table) (coq-shell-mode-config)))
  (delay-mode-hooks (proof-shell-mode) (setq major-mode (quote coq-shell-mode)) (setq mode-name "Coq Shell") (progn (if ... ...) (unless ... ...) (let ... ...)) (use-local-map coq-shell-mode-map) (set-syntax-table coq-shell-mode-syntax-table) (setq local-abbrev-table coq-shell-mode-abbrev-table) (coq-shell-mode-config))
  coq-shell-mode()
  funcall(coq-shell-mode)
  (save-current-buffer (set-buffer proof-shell-buffer) (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-shell) (unless (proof-shell-live-buffer) (switch-to-buffer proof-shell-buffer) (error "%s process exited!" proc)) (with-current-buffer proof-response-buffer (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response)) (with-current-buffer proof-goals-buffer (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-goals)) (proof-with-current-buffer-if-exists proof-trace-buffer (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response) (setq pg-response-eagerly-raise nil)) (if proof-shell-fiddle-frames (save-selected-window ...)))
  (with-current-buffer proof-shell-buffer (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-shell) (unless (proof-shell-live-buffer) (switch-to-buffer proof-shell-buffer) (error "%s process exited!" proc)) (with-current-buffer proof-response-buffer (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response)) (with-current-buffer proof-goals-buffer (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-goals)) (proof-with-current-buffer-if-exists proof-trace-buffer (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response) (setq pg-response-eagerly-raise nil)) (if proof-shell-fiddle-frames (save-selected-window ...)))
  (let ((proc ...)) (let* (... ... ... ... ... ... ... ... ...) (message "Starting: %s" prog-command-line) (apply ... ...) (setq proof-shell-buffer ...) (unless ... ... ...)) (let (... ... ... ...) (setq proof-goals-buffer ...) (setq proof-response-buffer ...) (if proof-shell-trace-output-regexp ...) (if proof-shell-thms-output-regexp ...) (setq pg-response-special-display-regexp ...)) (with-current-buffer proof-shell-buffer (erase-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-shell) (unless ... ... ...) (with-current-buffer proof-response-buffer ... ... ...) (with-current-buffer proof-goals-buffer ... ... ...) (proof-with-current-buffer-if-exists proof-trace-buffer ... ... ... ...) (if proof-shell-fiddle-frames ...)) (message "Starting %s process... done." proc))
  (if (proof-shell-live-buffer) nil (setq proof-included-files-list nil) (let (...) (if ... ...)) (if proof-prog-name-ask (setq proof-prog-name ...)) (let (...) (let* ... ... ... ... ...) (let ... ... ... ... ... ...) (with-current-buffer proof-shell-buffer ... ... ... ... ... ... ... ...) (message "Starting %s process... done." proc)))
  (unless (proof-shell-live-buffer) (setq proof-included-files-list nil) (let (...) (if ... ...)) (if proof-prog-name-ask (setq proof-prog-name ...)) (let (...) (let* ... ... ... ... ...) (let ... ... ... ... ... ...) (with-current-buffer proof-shell-buffer ... ... ... ... ... ... ... ...) (message "Starting %s process... done." proc)))
  proof-shell-start()
  proof-shell-ready-prover(advancing)
  (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()
  (save-excursion (goto-char (proof-queue-or-locked-end)) (skip-chars-forward " 	\n") (proof-assert-until-point))
  (progn (save-excursion (goto-char ...) (skip-chars-forward " 	\n") (proof-assert-until-point)) (proof-maybe-follow-locked-end))
  (cond ((eq proof-buffer-type ...) (progn ... ...)) ((buffer-live-p proof-script-buffer) (with-current-buffer proof-script-buffer ... ...)))
  (proof-with-script-buffer (save-excursion (goto-char ...) (skip-chars-forward " 	\n") (proof-assert-until-point)) (proof-maybe-follow-locked-end))
  proof-assert-next-command-interactive()
  call-interactively(proof-assert-next-command-interactive nil nil)

I wonder if there is an issue with the treatment of the colon? Below is my report (copied from the ssreflect mailing list):

A similar problem [see the quoted message below] occurred today with ssrcoq trunk on my machine after updating to proofgeneral 4.2pre120112. Neither executables of ssreflect nor the (trunk) libraries did change.

Calling from the command line by "ssrcoq -compile" succeeds as usual. Only the emacs mode is broken.

The lemma

Lemma inord_rshift n (i : 'I_n) : inord i.+1 = rshift 1 i. by rewrite rshift1 -lift0 inord_val. Qed.

now yields in proofgeneral:

Toplevel input, characters 34-41:

Error: In environment

n : nat

i : 'I_n

The term "inord i" has type "'I_?19.+1" which should be Set, Prop or Type.

The relevant lines in the *coq* buffer:

Toplevel input, characters 34-41:

Lemma inord_rshift n (i : 'I_n) : inord i.+

Error: In environment

n : nat

i : 'I_n

The term "inord i" has type "'I_?9.+1" which should be Set, Prop or Type.

Regards, Vladimir

On 25 January 2012 10:51, Vincent Siles <vincent.siles@…> wrote:

Hi there, since lots of stuff have changed in coq-svn v8.3 recently, I decided to upgrade it this morning and recompile ssr, but I have the following error (dynamic plugin compilation):

/home/vinz/boulot/coq/v8.3/bin/coqc -q -R theories Ssreflect -R src Ssreflect theories/fintype File "/home/vinz/boulot/coq/ssreflect-svn/trunk/ssreflect/ssreflect1.3_v8.3/theories/fintype.v", line 131, characters 44-45: Error: In environment T : eqType e : seq ?15 The term "T" has type "eqType" while it is expected to have type

"pred_sort ?21".

make: * [theories/fintype.vo] Erreur 1

I'm using the svn version of Coq 8.3

[vinz@hauru ssreflect1.3_v8.3]$ $COQBIN/coqtop.byte -v The Coq Proof Assistant, version 8.3pl3 (January 2012) compiled on janv. 25 2012 11:17:29 with OCaml 3.12.1

svn info gives:

Révision : 3533 Révision de la dernière modification : 3466 Date de la dernière modification: 2011-11-21 15:14:22 +0100 (lun. 21 nov. 2011)

Do I have to backtrack to pl2 ? My goal is to use Coq 8.3 and the librairies of ssr 1.3 (I don't want to use the thoeries of the trunk since I want other people to be able to compile my files).

Any suggestions ?

I installed PhoX 0.88.100524 and tried to step through phox/square-root-2.phx, but nothing works. Looks like the prompt is not recognized...

Hendrik