[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


amdunn at gmail.com changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|NEEDINFO                    |ASSIGNED
               Flag|needinfo?(amdunn at gmail.com) |




------- Additional Comments From amdunn at gmail.com  2008-06-09 06:22 EST -------
(In reply to comment #14)

Thanks for looking at the package. I have some questions and comments about what
you said.

> These bits of the spec file are all wrong:
> 
>   # Test for emacs site_lisp directory, if so, add relevant files to roster,
else, don't try and install
>   ...
>   # Test for tex directory, if so, add relevant files to roster, else, don't
try and install
>   ...
> 
> It's not acceptable to have different RPMs being produced depending on what
> happens to be installed at the time.  Instead, assume those directories / packages
> are installed and ensure this by having a complete list of BuildRequires.
> 
> Your BuildRequires is missing at least emacs, texlive-latex, another texlive-*
> package which provides /usr/share/texmf/tex/latex/misc (I couldn't find
> which one).

I put things the way I did in the spec file to attempt to reduce the list of
BuildRequires. It seems a bit odd to require someone to have emacs installed
just to put a .el file in the appropriate place. What if, for the sake of
argument, the user is a vi person and doesn't feel like installing emacs?
However, you are right, it would certainly affect the built binary RPM. Is there
a way to do what I would actually like here? I suppose things like that could be
subpackaged, but that seemed excessive for such a low number of files.

> Once you think you've got a complete list of BuildRequires, you should then
> scratch-build the package in koji:
> 
>   koji build --scratch dist-f10 coq-8.1pl3-1.fc9.src.rpm
> 
> This will almost certainly fail, but it should fail in a way which tells you which
> extra BuildRequires you are missing and any other problems that you'll
> encounter in the real build.

Just to clarify, you're saying that you think that when I change to acting as
though the person has TeX and emacs installed that I'll be missing appropriate
BuildRequires, right? As is, I did a test build with mock to see if the
BuildRequires were appropriately satisfied, and things seemed to work.

> When you have a successful scratch-build in Koji, please attach a link to
> the Koji build here.
> 
> Next thing you should do is to run rpmlint on all the RPMs (source and binary
> RPMs).  rpmlint output should be nil for this package.

I knew that there was a bit of rpmlint output - it fell into three categories,
two of which are related:

1) One of the graphics files appears to be corrupted
2) Some of the text files are not in UTF-8

I could repackage the main coq source, but I wasn't sure if this was a good idea
as this changes the signature of the main source, thus denying anyone the
ability to check for a match. I thought a solution would be to include a
separate icon and I wasn't sure how necessary the UTF-8 conversion is - perhaps
I should be including separate versions of those files too?

3) Inclusion of .cmxa files in a "non-devel" package

I'm not sure about that one. I didn't think it was really appropriate to make a
separate package for those.

> Another thing I notice in the spec file:
> 
>   %{_bindir}/parser
>   %{_bindir}/parser.opt
>   # I suppose technically we might not have built parser.opt, but my efforts
to fix this problem re: accounting for this in 
> the file manifest have failed
> 
> This is against the OCaml packaging policy which requires that you package the
> best possible binary (ie. native, if available, else bytecode).  You can easily do
> this by testing for the presense of ocamlopt.  See the first line of our sample
> specfile:
> 
>   http://fedoraproject.org/w/uploads/5/5c/Packaging_OCaml_ocaml-foolib.spec

Their main configuration file always attempts to build with the best possible
binary. I originally was just trying to check whether their setup in doing so
(by checking whether a parser.opt file was created), but was having a bit of a
time doing that. Is checking for ocamlopt what I should be doing? Just because
there is an ocamlopt program available doesn't necessarily mean that their setup
was able to detect everything properly and build using it.

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