Bug#544436: marked as done (proofgeneral-misc: All actions in phox-mode fail: "Wrong type argument: stringp, nil")
Your message dated Tue, 28 Feb 2012 21:11:28 +0000
with message-id <E1S2UKW-0000XK-Sg@franck.debian.org>
and subject line Bug#544436: fixed in proofgeneral 4.2~pre120206-1
has caused the Debian Bug report #544436,
regarding proofgeneral-misc: All actions in phox-mode fail: "Wrong type argument: stringp, nil"
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)
--
544436: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=544436
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message ---
Package: proofgeneral-misc
Version: 3.7-3
Severity: important
When I open a PhoX file in Proof-General, I get the Proof-General menu
and syntax highlighting normally, but all interactions with the PhoX
prover (process a proof command, or simply start PhoX with C-c C-s) fail
with an error message "Wrong type argument: stringp, nil" (a full
backtrace is given below).
I use the latest version (0.87.080623) of PhoX, which works normally from the
command line. The bug occurs using either emacs22 (22.2+2-5) or xemacs21
(21.4.21-4). I didn't test the Plastic or Twelf modes, but at least PG
interacts nicely with Coq using proofgeneral-coq (3.7-3).
This problem was previously mentionned by Andreas Gösele on debian-user
http://lists.debian.org/debian-user/2009/05/msg00707.html
Thanks in advance for fixing this annoying bug,
iouri.
-- Emacs backtrace:
Debugger entered--Lisp error: (wrong-type-argument stringp nil)
string-match("[ \f \n^M^K]+" 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))
proof-toolbar-next()
call-interactively(proof-toolbar-next)
-- System Information:
Debian Release: 5.0.2
APT prefers stable
APT policy: (900, 'stable')
Architecture: i386 (i686)
Kernel: Linux 2.6.26-2-686 (SMP w/2 CPU cores)
Locale: LANG=fr_FR.UTF-8, LC_CTYPE=fr_FR.UTF-8 (charmap=UTF-8)
Shell: /bin/sh linked to /bin/bash
Versions of packages proofgeneral-misc depends on:
ii proofgeneral 3.7-3 generic interface for proof assist
proofgeneral-misc recommends no packages.
proofgeneral-misc suggests no packages.
-- no debconf information
--- End Message ---
--- Begin Message ---
Source: proofgeneral
Source-Version: 4.2~pre120206-1
We believe that the bug you reported is fixed in the latest version of
proofgeneral, which is due to be installed in the Debian FTP archive:
proofgeneral-doc_4.2~pre120206-1_all.deb
to main/p/proofgeneral/proofgeneral-doc_4.2~pre120206-1_all.deb
proofgeneral_4.2~pre120206-1.debian.tar.gz
to main/p/proofgeneral/proofgeneral_4.2~pre120206-1.debian.tar.gz
proofgeneral_4.2~pre120206-1.dsc
to main/p/proofgeneral/proofgeneral_4.2~pre120206-1.dsc
proofgeneral_4.2~pre120206-1_all.deb
to main/p/proofgeneral/proofgeneral_4.2~pre120206-1_all.deb
proofgeneral_4.2~pre120206.orig.tar.gz
to main/p/proofgeneral/proofgeneral_4.2~pre120206.orig.tar.gz
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to 544436@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Hendrik Tews <hendrik@askra.de> (supplier of updated proofgeneral package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512
Format: 1.8
Date: Tue, 28 Feb 2012 12:53:12 +0100
Source: proofgeneral
Binary: proofgeneral proofgeneral-doc
Architecture: source all
Version: 4.2~pre120206-1
Distribution: unstable
Urgency: low
Maintainer: Hendrik Tews <hendrik@askra.de>
Changed-By: Hendrik Tews <hendrik@askra.de>
Description:
proofgeneral - generic frontend for proof assistants
proofgeneral-doc - generic frontend for proof assistants - documentation
Closes: 544436 642048 660353
Changes:
proofgeneral (4.2~pre120206-1) unstable; urgency=low
.
* new upstream prerelease (Closes: #642048)
* moved to section editors
* standards version 3.9.3
* fix compilation with emacs-nox (Closes: #660353)
* don't support broken PhoX anymore (Closes: #544436)
Checksums-Sha1:
f72783cec06eac9585cfc4cf91d0468455acca51 1959 proofgeneral_4.2~pre120206-1.dsc
fea22b7bed1dda39eda84aa687b79bd32731c30e 952848 proofgeneral_4.2~pre120206.orig.tar.gz
db395e481fd6cc75e0ca828616d29a1ec3abc12d 19341 proofgeneral_4.2~pre120206-1.debian.tar.gz
f10c00836a8323dc59fb81961e7cd3279d8299bd 430074 proofgeneral_4.2~pre120206-1_all.deb
692e963daa7d45a09f89dfe0ab89b8e15807c60e 676030 proofgeneral-doc_4.2~pre120206-1_all.deb
Checksums-Sha256:
2522708aab2edab2a876dfc4f69d964aa94b31c76d6527f16ff3edc483e143f2 1959 proofgeneral_4.2~pre120206-1.dsc
cc6d4b0a83d9459d516541653839fd9873f6a96a3c574879780d06b2022482d5 952848 proofgeneral_4.2~pre120206.orig.tar.gz
83505c9ab40bcccfa6f6cb0f988c11e5b7f80e13d2ac97bf792a6654c139b7d5 19341 proofgeneral_4.2~pre120206-1.debian.tar.gz
612caa6886f6ea8ba430fc2a331bfcf18b69bc944e1d111b206472da521697b8 430074 proofgeneral_4.2~pre120206-1_all.deb
f38f3884854ab5f246e1dd1ff282d7f8238d016842303f71384553a2e4917622 676030 proofgeneral-doc_4.2~pre120206-1_all.deb
Files:
b0c76e5489275e6783a7a48eb4b531db 1959 editors optional proofgeneral_4.2~pre120206-1.dsc
6d582b949f37b6a65ed3e656450f7021 952848 editors optional proofgeneral_4.2~pre120206.orig.tar.gz
0839232ed8e1326a73dbcc6eaca24f52 19341 editors optional proofgeneral_4.2~pre120206-1.debian.tar.gz
0468f57e747f765a2b2b0d283704a4d1 430074 editors optional proofgeneral_4.2~pre120206-1_all.deb
b6dd6a7744d94bf7b3238725bb85d9ef 676030 doc optional proofgeneral-doc_4.2~pre120206-1_all.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
iQIcBAEBCgAGBQJPTTKzAAoJEHhT2k1JiBrT59wQAIwoX6wO4rqhhUenOO9X51n1
DUeL6LBU/TuW8LcNPULUHQkqXWd73Zd71bRiI015ehM1kz/7kGwfruusDGwQupLy
88AnzbCEOFiDFzagfd+clMBasZVm/5jV4hGi5KsSM57gcEwAlMnEcJGQ6LI3MpOr
Vnr3dVvlE7mrF/zBW37Bs6G/h6qX30lZboNiplVkXg/81BvBl01dR/91FgZGgFlA
LHQ4Ja64u9BUbMAsbjf/EqFx1hMcnWfUvARTSDkZFOr6z4FHWtvh+ChcSrUeKLlV
cRZzmZsVywjJAGI/1W4PA6YpdS1N+eVjIaefnoZVG6r1MI2jeDerxu78uJV/j8LD
dfsDrRipCCqmRQqN7zcCTuMb/rpfp2Oqlt6rAYxZlTGEs5LktsGVdhLa/dFS84Sj
29+GGm+RNROu3zCzV3x3wUZB7/f0xnnssBmvLNlcVN5c7VlebCcOHG/sRXvqCycU
O0IOprD4aioKmgjg6KLuph5/MeC1quA2WStWivw+oq4BD/bVpGCXFDbup7MoCFKe
19YlL7S6QrDI7exbKHMs+ULAzvABcxG3XSWEMr1vxWjCcZ0ElNatOA6qkBKHOGL5
3ony28U7MlnuMlCye7C8rtMfgMNzfoumtXPAQq8K1FocVzDZfTai+8scTOq92cfm
8t7PmcWS8uOKJCxNvrCg
=fOV1
-----END PGP SIGNATURE-----
--- End Message ---
Reply to: