Custom Query (361 matches)

I am on a brand new MacBook Pro (OS 10.5.3) using Isabelle 2007 and the current release of Carbon Emacs.

x-symbol fails to load (from the ProofGeneral menu) under Carbon Emacs. In the bottom window, I get the error:

Warning (emacs): X-Symbol characters with registry "xsymb-xsymb1" are not used

On the line at the very bottom, I get:

Symbol's value as variable is void: ccl-encode-fake-xsymb1-font

Thanks.

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 ?

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)