[Bug 484049] New: 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.

Summary: Review Request: emacs-common-proofgeneral - Emacs mode for standard interaction interface for proof assistants

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

           Summary: Review Request: emacs-common-proofgeneral - Emacs mode
                    for standard interaction interface for proof
                    assistants
           Product: Fedora
           Version: rawhide
          Platform: All
        OS/Version: Linux
            Status: NEW
          Severity: medium
          Priority: medium
         Component: Package Review
        AssignedTo: nobody at fedoraproject.org
        ReportedBy: amdunn at gmail.com
         QAContact: extras-qa at fedoraproject.org
                CC: notting at redhat.com, fedora-package-review at redhat.com
   Estimated Hours: 0.0
    Classification: Fedora


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 at 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.

-- 
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.