Bug 484049 - Review Request: emacs-common-proofgeneral - Emacs mode for standard interaction interface for proof assistants
Summary: Review Request: emacs-common-proofgeneral - Emacs mode for standard interacti...
Keywords:
Status: CLOSED ERRATA
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: Jerry James
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2009-02-04 14:42 UTC by Alan Dunn
Modified: 2012-11-16 16:12 UTC (History)
4 users (show)

Fixed In Version: 3.7.1-4.fc11
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2009-08-20 21:01:49 UTC
Type: ---
Embargoed:
loganjerry: fedora-review+
j: fedora-cvs+


Attachments (Terms of Use)
New display-table support (5.73 KB, patch)
2009-07-06 22:15 UTC, Jerry James
no flags Details | Diff

Description Alan Dunn 2009-02-04 14:42:30 UTC
Spec URL: http://www.phy.duke.edu/~amd34/pg/emacs-common-proofgeneral.spec
SRPM URL: http://www.phy.duke.edu/~amd34/pg/emacs-common-proofgeneral-3.7.1-1.fc10.src.rpm

Description: See after description for comments on things I have already done to test this spec file.

(from spec file)
Proof General is a generic front-end for proof assistants (also known
as interactive theorem provers) based on Emacs.

Proof General allows one to edit and submit a proof script to a proof
assistant in an interactive manner:
- It tracks the goal state, and the script as it is submitted, and
  allows for easy backtracking and block execution.
- It adds toolbars and menus to Emacs for easy access to proof
  assistant features.
- It integrates with X-Symbol for some provers to provide output using
  proper mathematical symbols.
- It includes utilities for generating Emacs tags for proof scripts,
  allowing for easy navigation.

Proof General supports a number of different proof assistants
(Isabelle, Coq, PhoX, and LEGO to name a few) and is designed to be
easily extendable to work with others.

Tests:
- Runs on my machine (F10 i386) in both emacs and xemacs (even when both packages are simultaneously installed)
- Builds in mock
- rpmlint output:

[adunn@localhost rpmbuild]$ rpmlint SPECS/emacs-common-proofgeneral.spec RPMS/noarch/*proofgeneral*
emacs-proofgeneral.noarch: W: no-documentation
emacs-proofgeneral-el.noarch: W: no-documentation
xemacs-proofgeneral.noarch: W: no-documentation
xemacs-proofgeneral-el.noarch: W: no-documentation
5 packages and 1 specfiles checked; 0 errors, 4 warnings.

I am under the impression that the separate subpackages for compiled elisp and elisp files do not need separate documentation (which is the source of these warnings). I saw this warning in other emacs-involved RPMS that I downloaded. If that is not correct, it can be easily corrected.

Concerns: I think this spec file is essentially correct, but I thought I might point out an issue or two for any potential reviewer:
1) There is a desktop file to run the "proofgeneral" script. I can imagine the script being useful for other programs to call, but I'm not sure the gui way of running this has any real purpose (all it is going to do is run emacs/xemacs - the proofgeneral script with no arguments). I have not currently installed the desktop file but left it in the package for those that might want to examine it. Does that sound like a reasonable compromise?
2) I added a somewhat Fedora-specific patch that modifies the "proofgeneral" script just mentioned. It might be good to examine whether this is an alright way of accomplishing what was desired: independence of emacs variant (emacs/xemacs) in a way that works for Fedora.

Comment 1 Jerry James 2009-04-06 18:55:48 UTC
There was a small error in the XEmacs template (since fixed); there is supposed to be a "lisp" directory after %{_datadir}/xemacs/site-packages.  That is, please fix the following definitions at the top of the spec file:

%if %($(pkg-config xemacs) ; echo $?)
%define xemacs_version 21.5
%define xemacs_lispdir %{_datadir}/xemacs/site-packages/lisp
%define xemacs_startdir %{_datadir}/xemacs/site-packages/lisp/site-start.d

This doesn't cause any problems because pkg-config gives the right values, but it doesn't hurt to be safe...

The file %{emacs_lispdir}/proofgeneral/images/README is installed as a regular file in the emacs-proofgeneral package.  Shouldn't that be a documentation file?

The entire mmm and x-symbol distributions are included in the emacs-proofgeneral and xemacs-proofgeneral packages.  (And the x-symbol .el files are NOT included in (x)emacs-proofgeneral-el!)  I think this is wrong.  The mmm and x-symbol packages should be submitted separately, with the proofgeneral package depending on them.

Furthermore, mmm and x-symbol are already available for XEmacs in xemacs-packages-extra, so they only need to be made available for Emacs.  If the provides/requires have been setup properly, all you should need to do is NOT install them for XEmacs and add "Requires: xemacs-package-extra" to the xemacs-proofgeneral package.

I will do a full review shortly.

Comment 2 Jerry James 2009-04-06 19:22:29 UTC
MUST items:
- rpmlint output:
emacs-proofgeneral.noarch: W: no-documentation
emacs-proofgeneral-el.noarch: W: no-documentation
xemacs-proofgeneral.noarch: W: no-documentation
xemacs-proofgeneral-el.noarch: W: no-documentation
5 packages and 1 specfiles checked; 0 errors, 4 warnings.
- package name
- spec file name matches base package name
X packaging guidelines: as noted in comment #1, we may have a problem with https://fedoraproject.org/wiki/Packaging/Guidelines#Bundling_of_multiple_projects.  Also note that some files in the top-level lib directory may violate this rule, too.
- good license
- license field matches actual license
- include license file in %doc
- spec file in American English
- spec file legible
- sources match upstream
- builds on at least one primary arch
- use ExcludeArch as necessary (N/A)
- all build dependencies in BuildRequires
- proper locale handling (N/A)
- call ldconfig as necessary (N/A)
- rationale if relocatable (N/A)
- own all created directories
- no duplicate %file listings
- proper file permissions
- %clean section
- consistent use of macros
- code or permissible content
- large documentation files in a subpackage (N/A)
- nothing in %doc needed at runtime
- header files in -devel (N/A)
- static libraries in -static (N/A)
- require pkgconfig if necessary (N/A)
- .so files in -devel (N/A)
- -devel requires base package (N/A)
- no libtool archives
- desktop files for GUI apps: rationale given in the description above
- don't own files or dirs created by other packages
- clean at top of %install
- filenames are UTF-8

SHOULD items:
- query upstream for license file (N/A)
- description and summary contain available translations (N/A)
? package builds in mock: not checked
? package builds on all suppported arches: not checked
- package functions as described
- sane scriptlets
- subpackages require main package
- pkgconfig files in -devel (N/A)
- package dependencies instead of file dependencies

So we just need to investigate the use of bundled software and this package is good to go.  Thanks for submitting it!  This will make a great addition to the other prover-related software that has been pushed into Fedora recently.

Comment 3 Alan Dunn 2009-04-06 19:43:02 UTC
Thank you for reviewing this. I've been so busy with other things I haven't even had the time to search around for a reviewer and this has been sitting here quite a while. I'll try to tackle these as soon as I possibly can - good catch with the template error btw, guess that reveals that I've mainly used Emacs before eh? (though, of course, I did test that the package works in XEmacs)

(In reply to comment #2)
> MUST items:
> - rpmlint output:
> emacs-proofgeneral.noarch: W: no-documentation
> emacs-proofgeneral-el.noarch: W: no-documentation
> xemacs-proofgeneral.noarch: W: no-documentation
> xemacs-proofgeneral-el.noarch: W: no-documentation
> 5 packages and 1 specfiles checked; 0 errors, 4 warnings.
> - package name
> - spec file name matches base package name
> X packaging guidelines: as noted in comment #1, we may have a problem with
> https://fedoraproject.org/wiki/Packaging/Guidelines#Bundling_of_multiple_projects.
>  Also note that some files in the top-level lib directory may violate this
> rule, too.
> - good license
> - license field matches actual license
> - include license file in %doc
> - spec file in American English
> - spec file legible
> - sources match upstream
> - builds on at least one primary arch
> - use ExcludeArch as necessary (N/A)
> - all build dependencies in BuildRequires
> - proper locale handling (N/A)
> - call ldconfig as necessary (N/A)
> - rationale if relocatable (N/A)
> - own all created directories
> - no duplicate %file listings
> - proper file permissions
> - %clean section
> - consistent use of macros
> - code or permissible content
> - large documentation files in a subpackage (N/A)
> - nothing in %doc needed at runtime
> - header files in -devel (N/A)
> - static libraries in -static (N/A)
> - require pkgconfig if necessary (N/A)
> - .so files in -devel (N/A)
> - -devel requires base package (N/A)
> - no libtool archives
> - desktop files for GUI apps: rationale given in the description above
> - don't own files or dirs created by other packages
> - clean at top of %install
> - filenames are UTF-8
> 
> SHOULD items:
> - query upstream for license file (N/A)
> - description and summary contain available translations (N/A)
> ? package builds in mock: not checked
> ? package builds on all suppported arches: not checked
> - package functions as described
> - sane scriptlets
> - subpackages require main package
> - pkgconfig files in -devel (N/A)
> - package dependencies instead of file dependencies
> 
> So we just need to investigate the use of bundled software and this package is
> good to go.  Thanks for submitting it!  This will make a great addition to the
> other prover-related software that has been pushed into Fedora recently.

Comment 4 Alan Dunn 2009-04-07 13:00:37 UTC
I remember now that I had looked at the X-Symbol part before, and was wondering if it should be left in as the X-Symbol distribution in Proof General is modified from the original:

----------------------------------------------
(in x-symbol.README.x-symbol-for-ProofGeneral:)

The code in this directory is taken from

        http://x-symbol.sourceforge.net/

This is version 4.5.1-beta (dated 2003-05-11 15:00)

Several changes have been made for Proof General, including:

* the addition of 18pt and 24pt fonts, see etc/bigfonts.
  (thanks to Clemens Ballarin).
* the addition of a mechanism to use Norbert Voelker's isaxsymb1.ttf
  (see etc/fonts-ttf) automatically on Mac using Carbon Emacs.
  You need to install isaxsymb1.ttf into Font Book
  This is experimental support and may have some issues.
* Experimental (not yet working) support for Emacs 23
* Addition of `x-symbol-image-converter-required' which defaults to nil,
  to avoid X-Symbol giving warnings when it doesn't find ImageMagick convert.
  Images aren't used in Proof General, but if you want to use the same
  X-Symbol in LaTeX, you might want to customize this setting to t.
* addition of the string "[Proof General]" to x-symbol-version


The following rearrangements from the package directory layout have
been made:

  for f in etc lisp man; do mv $f/x-symbol/* $f; rmdir $f/x-symbol; done

Moreover, lisp/Makefile and lisp/makefile.pkg were copied from
X-Symbol source package, and lisp/makefile.pkg edited to remove
x-symbol-emacs from list of compiled files (since it breaks
on XEmacs compile).
----------------------------------------------

Is there a good solution to this problem? We don't necessarily want these changes to persist when it's used in other programs... I suppose I can try and encourage upstream to rewrite this in a way that should work with a separate version of x-symbol. (I could also try and do this myself, but it might not be obvious whether the changes that are listed here are the only ones anyway.)

I definitely missed mmm when I looked before though, and it claims to not be modified from the original, so I'll look into packaging that separately.

(In reply to comment #2)
> MUST items:
> - rpmlint output:
> emacs-proofgeneral.noarch: W: no-documentation
> emacs-proofgeneral-el.noarch: W: no-documentation
> xemacs-proofgeneral.noarch: W: no-documentation
> xemacs-proofgeneral-el.noarch: W: no-documentation
> 5 packages and 1 specfiles checked; 0 errors, 4 warnings.
> - package name
> - spec file name matches base package name
> X packaging guidelines: as noted in comment #1, we may have a problem with
> https://fedoraproject.org/wiki/Packaging/Guidelines#Bundling_of_multiple_projects.
>  Also note that some files in the top-level lib directory may violate this
> rule, too.
> - good license
> - license field matches actual license
> - include license file in %doc
> - spec file in American English
> - spec file legible
> - sources match upstream
> - builds on at least one primary arch
> - use ExcludeArch as necessary (N/A)
> - all build dependencies in BuildRequires
> - proper locale handling (N/A)
> - call ldconfig as necessary (N/A)
> - rationale if relocatable (N/A)
> - own all created directories
> - no duplicate %file listings
> - proper file permissions
> - %clean section
> - consistent use of macros
> - code or permissible content
> - large documentation files in a subpackage (N/A)
> - nothing in %doc needed at runtime
> - header files in -devel (N/A)
> - static libraries in -static (N/A)
> - require pkgconfig if necessary (N/A)
> - .so files in -devel (N/A)
> - -devel requires base package (N/A)
> - no libtool archives
> - desktop files for GUI apps: rationale given in the description above
> - don't own files or dirs created by other packages
> - clean at top of %install
> - filenames are UTF-8
> 
> SHOULD items:
> - query upstream for license file (N/A)
> - description and summary contain available translations (N/A)
> ? package builds in mock: not checked
> ? package builds on all suppported arches: not checked
> - package functions as described
> - sane scriptlets
> - subpackages require main package
> - pkgconfig files in -devel (N/A)
> - package dependencies instead of file dependencies
> 
> So we just need to investigate the use of bundled software and this package is
> good to go.  Thanks for submitting it!  This will make a great addition to the
> other prover-related software that has been pushed into Fedora recently.

Comment 5 Alan Dunn 2009-04-07 17:39:11 UTC
I packaged mmm for emacs:

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

I still have to figure out what to do for the other.

Comment 6 Jerry James 2009-04-07 19:17:38 UTC
Bummer that they modified X-Symbol without pushing their modifications upstream.  Do you have any idea what they did to it?  Maybe there is some way we can keep the namespace from getting polluted if their changes are localized.

If nobody beats me to mmm, I'll try to get to it tomorrow.

Comment 7 Jason Tibbitts 2009-06-27 06:38:27 UTC
Is anything happening with this review?  Please set the fedora-review flag to '?' if a review is in progress.

Comment 8 Jerry James 2009-07-02 14:46:23 UTC
Somebody needs to figure out what to do about the modified X-Symbol embedded in ProofGeneral.

I've set the flag.  Don't know how I missed that.

Comment 9 Alan Dunn 2009-07-02 14:52:43 UTC
I apologize for having let this one sit around for so long - I'll be able to address this shortly (and hopefully I'll be able to figure out what needs to be done).

Comment 10 Alan Dunn 2009-07-04 23:11:30 UTC
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.

Comment 11 Jerry James 2009-07-06 22:15:33 UTC
Created attachment 350698 [details]
New display-table support

The problem with Rawhide XEmacs is that the implementation of char-tables, and therefore display-tables, has changed.  They are no longer vectors, but objects.  The vector implementation was okay for ASCII/ISO8859-1, when we could limit the length to 256 and be okay.  That approach does not scale for international character sets, hence the new implementation.

I'm attaching a patch that starts dealing with the problem.  This isn't a complete solution, because the new file (generic/pg-display-table.el) isn't in the right place.  The x-symbol code needs it, so the compile fails.  If you can find a good place to put that file so it can be (require)d at need, I think it will work.

Comment 12 Alan Dunn 2009-07-09 23:34:42 UTC
Thanks for the patch. After adding a change to the Makefile (to not compile their modified copy of the X-Symbol code, though your changes to their files that use X-Symbol are still compiled) the rest of the code now compiles. Thus, again with the caveat that the X-Symbol functionality won't yet work due to the changes that they made to X-Symbol needing to be present, the main functionality for the package now works and compiles in rawhide.

new specfile in the same location as before, new SRPM at

http://www.openproofs.org/packages/pg/emacs-common-proofgeneral-3.7.1-3.fc10.src.rpm

Comment 13 Jerry James 2009-07-27 21:52:58 UTC
Sorry to take so long with this.  I've been out on vacation for the last 2 weeks.

Two more changes are needed.  First, patch comments should appear in the header rather than on the %patch invocations in the %prep section.  See https://fedoraproject.org/wiki/Packaging:Guidelines#All_patches_should_have_an_upstream_bug_link_or_comment.

Second, the handling of patch2 is broken in two ways.  First, it isn't inserted into the source RPM when building on Fedora <= 11.  Indeed, the link you gave in comment #12 leads to a source RPM without the patch.  Unconditionally list the patch, so that it is always present in the source RPM.  Second, choosing to apply the patch based on Fedora release number will break soon; I'm preparing to push XEmacs 21.5.29 to F-11.  The patch I sent should compile and run successfully on all versions of XEmacs; the point of the wrappers was to hide the differences between Emacs/older XEmacs and newer XEmacs.  I think you can drop the conditionals and the BR on xemacs >= 21.5.29 and everything should work.

Everything else looks fine.  Make those changes and I'll approve it.  Thanks for your hard work.

Comment 14 Alan Dunn 2009-07-30 01:04:16 UTC
I made the changes you suggested. New SRPM version is just 3 -> 4, while spec is in the same location as before. Minor comments below.

(In reply to comment #13)
> Sorry to take so long with this.  I've been out on vacation for the last 2
> weeks.
> 
> Two more changes are needed.  First, patch comments should appear in the header
> rather than on the %patch invocations in the %prep section.  See
> https://fedoraproject.org/wiki/Packaging:Guidelines#All_patches_should_have_an_upstream_bug_link_or_comment.

Noted and changed.

> Second, the handling of patch2 is broken in two ways.  First, it isn't inserted
> into the source RPM when building on Fedora <= 11.  Indeed, the link you gave
> in comment #12 leads to a source RPM without the patch. Unconditionally list
> the patch, so that it is always present in the source RPM.  Second, choosing to
> apply the patch based on Fedora release number will break soon; I'm preparing
> to push XEmacs 21.5.29 to F-11.  The patch I sent should compile and run
> successfully on all versions of XEmacs; the point of the wrappers was to hide
> the differences between Emacs/older XEmacs and newer XEmacs.  I think you can
> drop the conditionals and the BR on xemacs >= 21.5.29 and everything should
> work.

I was trying to only patch things in the versions where I knew things wouldn't work without the patch. (As you point out, my solution would really also necessitate rebuilding the SRPM per distro version, which is bad.) I originally was trying to patch by xemacs EVR available in the distro, but I didn't know how to do this (I started a thread on Fedora-devel about this). Ultimately it's probably easier to apply the patch everywhere as you suggest.

> Everything else looks fine.  Make those changes and I'll approve it.  Thanks
> for your hard work.  

I may be hard to contact for a day or two (moving to a new place half-way across the US tomorrow), but I'll try to be as responsive as possible if there are any further issues. Thanks for reviewing this.

Comment 15 Jerry James 2009-07-30 14:44:38 UTC
Looks great. APPROVED.

Good luck with your move.

Comment 16 Alan Dunn 2009-07-31 02:45:55 UTC
New Package CVS Request
=======================
Package Name: emacs-common-proofgeneral
Short Description: Emacs mode for standard interaction interface for proof assistants
Owners: amdunn
Branches: F-10 F-11

Comment 17 Jason Tibbitts 2009-07-31 21:14:28 UTC
CVS done.

Comment 18 Fedora Update System 2009-08-05 00:30:41 UTC
emacs-common-proofgeneral-3.7.1-4.fc10 has been pushed to the Fedora 10 testing repository.  If problems still persist, please make note of it in this bug report.
 If you want to test the update, you can install it with 
 su -c 'yum --enablerepo=updates-testing update emacs-common-proofgeneral'.  You can provide feedback for this update here: http://admin.fedoraproject.org/updates/F10/FEDORA-2009-8265

Comment 19 Fedora Update System 2009-08-05 00:37:18 UTC
emacs-common-proofgeneral-3.7.1-4.fc11 has been pushed to the Fedora 11 testing repository.  If problems still persist, please make note of it in this bug report.
 If you want to test the update, you can install it with 
 su -c 'yum --enablerepo=updates-testing update emacs-common-proofgeneral'.  You can provide feedback for this update here: http://admin.fedoraproject.org/updates/F11/FEDORA-2009-8288

Comment 20 Fedora Update System 2009-08-20 21:01:40 UTC
emacs-common-proofgeneral-3.7.1-4.fc10 has been pushed to the Fedora 10 stable repository.  If problems still persist, please make note of it in this bug report.

Comment 21 Fedora Update System 2009-08-22 01:05:59 UTC
emacs-common-proofgeneral-3.7.1-4.fc11 has been pushed to the Fedora 11 stable repository.  If problems still persist, please make note of it in this bug report.

Comment 22 Benjamin Kreuter 2012-11-16 16:12:02 UTC
Package Change Request
======================
Package Name: emacs-common-proofgeneral
New Branches: el5 el6
Owners: amdunn

This is needed to branch coq to EPEL.


Note You need to log in before you can comment on or make changes to this bug.