[Bug 450323] Review Request: coq - Coq proof management system

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

Summary: Review Request: coq - Coq proof management system


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





------- Additional Comments From rjones at redhat.com  2008-07-07 13:02 EST -------
As a general comment, I think Alan has worked hard on this package,
addressing every one of the (many) comments that we have made
along the way.

Package review follows below.

+ rpmlint output

  coq.i386: W: unstripped-binary-or-object /usr/bin/coqtop.byte
  coq.i386: W: executable-stack /usr/bin/parser.opt
  coq.i386: W: executable-stack /usr/bin/coqtop.opt
  coq.i386: W: unstripped-binary-or-object /usr/bin/coq-tex
  coq.i386: W: unstripped-binary-or-object /usr/bin/parser
  coq.i386: W: unstripped-binary-or-object /usr/bin/gallina
  coq.i386: W: unstripped-binary-or-object /usr/bin/coqdoc
  coq.i386: W: unstripped-binary-or-object /usr/bin/coqwc
  coq.i386: W: executable-stack /usr/bin/coq-interface.opt
  coq.i386: W: unstripped-binary-or-object /usr/bin/coqdep
  coq.i386: W: unstripped-binary-or-object /usr/bin/coq_makefile
  coq.i386: W: unstripped-binary-or-object /usr/bin/coq-interface
  coq-coqide.i386: W: hidden-file-or-dir /usr/share/coq/ide/.coqide-gtk2rc
  coq-coqide.i386: W: executable-stack /usr/bin/coqide.opt
  coq-coqide.i386: W: unstripped-binary-or-object /usr/bin/coqide.byte

The 'executable-stack' warnings are an instance of bug 450551.
The 'unstripped-binary-or-object' warnings are because these bytecode
files shouldn't be stripped.
The 'hidden-file-or-dir' looks like it can be ignored in this case.

+ package name satisfies the packaging naming guidelines
+ specfile name matches the package base name
+ package should satisfy packaging guidelines

Because Alan isn't shipping any library, we just checked against
the rather more relaxed OCaml binary guidelines, and these are OK.

+ license meets guidelines and is acceptable to Fedora

License appears to be LGPLv2 (not '+').

+ license matches the actual package license
+ %doc includes license file
+ spec file written in American English
+ spec file is legible
+ upstream sources match sources in the srpm

84311faf7865b2eab964990cdb365dca 3003593

+ package successfully builds on at least one architecture

i386

- ExcludeArch bugs filed

Alan, please file ExcludeArch bugs for the platforms where it
doesn't compile (ie. ppc)

+ BuildRequires list all build dependencies
n/a %find_lang instead of %{_datadir}/locale/*
n/a binary RPM with shared library files must call ldconfig in %post and %postun
+ does not use Prefix: /usr
+ package owns all directories it creates
+ no duplicate files in %files
+ %defattr line
- %clean contains rm -rf $RPM_BUILD_ROOT

Alan, you don't need 'make clean' in %clean.

+ consistent use of macros
+ package must contain code or permissible content
+ large documentation files should go in -doc subpackage
+ files marked %doc should not affect package
n/a header files should be in -devel
n/a static libraries should be in -static
n/a packages containing pkgconfig (.pc) files need 'Requires: pkgconfig'
n/a libfoo.so must go in -devel
n/a -devel must require the fully versioned base
n/a packages should not contain libtool .la files
n/a packages containing GUI apps must include %{name}.desktop file
n/a packages must not own files or directories owned by other packages
+ %install must start with rm -rf %{buildroot} etc.
+ filenames must be valid UTF-8

Optional:

n/a if there is no license file, packager should query upstream
n/a translations of description and summary for non-English languages, if available
+ reviewer should build the package in mock
- the package should build into binary RPMs on all supported architectures
- review should test the package functions as described
+ scriptlets should be sane
n/a pkgconfig files should go in -devel
n/a shouldn't have file dependencies outside /etc /bin /sbin /usr/bin or /usr/sbin


Please fix the two problems noted above, before I can approve the package.

-- 
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, or are watching someone who is.