[Bug 484049] Review Request: emacs-common-proofgeneral - Emacs mode for standard interaction interface for proof assistants

[bugzilla at redhat.com]

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.


https://bugzilla.redhat.com/show_bug.cgi?id=484049





--- Comment #10 from Alan Dunn <amdunn at gmail.com>  2009-07-04 19:11:30 EDT ---
It seems like a potential solution for now is to disable the X-Symbol
functionality. Since I've used Proof General for a little bit now at least, it
seems that the X-Symbol functionality is rather minor compared to the total
functionality of the package: It's merely used to render "nicer versions" of
symbols for certain provers. (Eg: in Coq mode, it will turn "->" into an actual
arrow) The functionality seems to be disabled by default, so it won't prevent
the package from being used. I have a version which excludes the X-Symbol part
at

SPEC: http://www.openproofs.org/packages/pg/emacs-common-proofgeneral.spec
SRPM:
http://www.openproofs.org/packages/pg/emacs-common-proofgeneral-3.7.1-2.fc10.src.rpm

Additionally, I looked at the Debian package for Proof General. It seems that
their support for X-Symbol in Proof General just suggests that X-Symbol should
be installed, and they have no package for it. (Actually, it seems they did at
some point and it was removed:
http://lists.debian.org/debian-devel/2006/01/msg00964.html) I'll also note that
it seems that X-Symbol upstream is also dead; the last version was released in
2003 and no fixes/updates seem forthcoming.

One thing that's new is that the package doesn't seem to build in the version
of xemacs that's now in F12. The logs reveal (from
http://koji.fedoraproject.org/koji/taskinfo?taskID=1450936):

xemacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar
(lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-3.7.1/" (symbol-name
d))) (quote (acl2 ccc coq demoisa hol98 isar lclam lego pgshell phox plastic
twelf generic lib mmm))) load-path))' -f batch-byte-compile phox/phox.el
Compiling /builddir/build/BUILD/ProofGeneral-3.7.1/phox/phox.el...
While compiling toplevel forms in file
/builddir/build/BUILD/ProofGeneral-3.7.1/phox/phox.el:
  !! Wrong type argument ((arrayp #s(char-table type generic data ())))
Done
>>Error occurred processing phox/phox.el: Wrong type argument: arrayp, #s(char-table type generic data ())

However, things seem to be fine in F11:
http://koji.fedoraproject.org/koji/taskinfo?taskID=1450956

I'll look at this part now; just thought I'd post where I am on this.

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.