proofgeneral - wrong-type-argument stringp nil

[Goesele@hfph.mwn.de]

Hi,

I'm not able to use proofgeneral (3.7.) under Debian lenny - neither
with Emacs (22.2.1) nor with XEmacs (21.4.21).

I can start proofgeneral, if I open for instance a phox (.phx) I get
the proofgeneral menu and syntax highlighting, but most of the
commands don't work. I get instead the "wrong-type-argument stringp
nil" error (traceback for XEmacs below).

Is this a known issue? Is there anything I can do to make proofgeneral
work under Debian lenny?

Thanks a lot in advance!

Andreas

Traceback (XEmacs 21.4.21)

Debugger entered--Lisp error: (wrong-type-argument stringp nil)
  string-match("[       \n
]+" nil 0)
  split-string(nil)
  (if (proof-ass prog-args) (cons proof-prog-name (proof-ass prog-args)) (split-string proof-prog-name))
  (let* ((prog-name-list1 ...) (prog-name-list ...) (prog-command-line ...) (process-connection-type proof-shell-process-connection-type) (process-environment ...) (normal-coding-system-for-read ...) (coding-system-for-read ...) (coding-system-for-write coding-system-for-read)) (message "Starting process: %s" prog-command-line) (apply (quote make-comint) (append ... ...)) (setq proof-shell-buffer (get-buffer ...)) (unless (proof-shell-live-buffer) (setq proof-shell-buffer nil) (error "Starting process: %s..failed" prog-command-line)))
  (let ((proc ...)) (let* (... ... ... ... ... ... ... ...) (message "Starting process: %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 ... ... ...) (set-buffer proof-response-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-response) (proof-with-current-buffer-if-exists proof-trace-buffer ... ... ...) (set-buffer proof-goals-buffer) (proof-shell-set-text-representation) (funcall proof-mode-for-goals) (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 (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()
  proof-shell-ready-prover(advancing)
  (save-excursion (proof-shell-ready-prover queuemode) (cond (... ...) (...) (t ... ... ... ... ... ... ... ... ... ...)))
  proof-activate-scripting(nil advancing)
  (if ignore-proof-process-p nil (proof-activate-scripting nil (quote advancing)))
  (unless ignore-proof-process-p (proof-activate-scripting nil (quote advancing)))
  proof-assert-next-command()
  (progn (goto-char (proof-queue-or-locked-end)) (proof-assert-next-command))
  (if (eq proof-follow-mode (quote locked)) (progn (goto-char ...) (proof-assert-next-command)) (save-excursion (goto-char ...) (proof-assert-next-command)))
  (proof-maybe-save-point (goto-char (proof-queue-or-locked-end)) (proof-assert-next-command))
  (progn (proof-maybe-save-point (goto-char ...) (proof-assert-next-command)) (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 (proof-maybe-save-point (goto-char ...) (proof-assert-next-command)) (proof-maybe-follow-locked-end))
  (lambda nil "Process until the end of the next unprocessed command after point.\nIf inside a comment, just process until the start of the comment." (interactive) (proof-with-script-buffer (proof-maybe-save-point ... ...) (proof-maybe-follow-locked-end)))()
  call-interactively(proof-toolbar-next)
  release-and-activate-toolbar-button(#<buttonup-event button1up>)
  call-interactively(release-and-activate-toolbar-button)

-- 
Andreas Gösele