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@xxxxxxxxxxxxxxxxx ReportedBy: amdunn@xxxxxxxxx QAContact: extras-qa@xxxxxxxxxxxxxxxxx CC: notting@xxxxxxxxxx, fedora-package-review@xxxxxxxxxx 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@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. _______________________________________________ Fedora-package-review mailing list Fedora-package-review@xxxxxxxxxx http://www.redhat.com/mailman/listinfo/fedora-package-review