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

Tue Apr 7 13:00:37 UTC 2009

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 #4 from Alan Dunn <amdunn at gmail.com>  2009-04-07 09:00:37 EDT ---
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.

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