dir symbol is void on leopard coq

[Ryan Wisnesky]

Proof general starts correctly with emacs but when I try to start coq with C-c C-s I get a

Symbol's value as variable is void: dir

the trace is

Loading /Users/ryan/emacs/ProofGeneral-3.7.1pre080526/ProofGeneral/generic/proof-toolbar.el (source)...done Loading /Users/ryan/emacs/ProofGeneral-3.7.1pre080526/ProofGeneral/generic/pg-user.el (source)...done Loading /Users/ryan/emacs/ProofGeneral-3.7.1pre080526/ProofGeneral/generic/proof-shell.el (source)...done Loading /Users/ryan/emacs/ProofGeneral-3.7.1pre080526/ProofGeneral/generic/proof-x-symbol.el (source)...done file-exists-p: Symbol's value as variable is void: dir [2 times]

I'm using these versions, although this same behavior happens with the stable version of Proof General and with Coq 8.1pl2:

This is GNU Emacs 22.1.1 (i386-apple-darwin9.2.2, Carbon Version 1.6.0)

The Coq Proof Assistant, version 8.1pl3 (Dec. 2007)

Version 3.7.1pre080526

[Ryan Wisnesky]

This is Mac OS X v10.5.3

[David Aspinall]

Thanks for the report. Unfortunately I can't reproduce this. Could you enable debugging to make a complete backtrace, please? See http://proofgeneral.inf.ed.ac.uk/wiki/PG/PGEmacsDebuggingTips

[Ryan Wisnesky]

The trace is:

Debugger entered--Lisp error: (void-variable dir)

(concat dir "Makefile") (file-exists-p (concat dir "Makefile")) (cond ((file-exists-p ...) ".") (t nil)) (let ((dir ...) (makedir ...)) (if makedir (let* ... ...) coq-prog-name)) (if (local-variable-p (quote coq-prog-name) (current-buffer)) coq-prog-name (let (... ...) (if makedir ... coq-prog-name))) coq-guess-command-line("/Users/ryan/Row.v") apply(coq-guess-command-line "/Users/ryan/Row.v") (setq proof-prog-name (apply proof-guess-command-line (list name))) (if (and name proof-prog-name-guess proof-guess-command-line) (setq proof-prog-name (apply proof-guess-command-line ...))) (let ((name ...)) (if (and name proof-prog-name-guess proof-guess-command-line) (setq proof-prog-name ...))) (if (proof-shell-live-buffer) nil (setq proof-included-files-list nil) (let (...) (if ... ...)) (if proof-prog-name-ask (save-excursion ...)) (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 (save-excursion ...)) (let (...) (let* ... ... ... ... ...) (let ... ... ... ... ... ...) (with-current-buffer proof-shell-buffer ... ... ... ... ... ... ... ... ... ... ... ...) (message "Starting %s process... done." proc))) proof-shell-start() call-interactively(proof-shell-start)

My .emacs has

(setq coq-prog-name "/usr/local/bin/coqtop -emacs") (load-file "/Users/ryan/emacs/ProofGeneral-3.7.1pre080526/ProofGeneral/generic/proof-site.el")

and the coq-prog-name is the correct path.

[David Aspinall]

Thanks for the backtrace. It looks as if Pierre has found this independently and fixed it now, in PG CVS and next releases.