[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-06-09 06:40 EST -------
> 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.

The purpose of BuildRequires is a complete list of build requirements so
that an identical binary package can be built on any system.  The current
spec file would build different binary RPMs depending on whatever happened
to be installed on the build system.  (And in fact it fails if that tex.../misc
directory is missing).  Don't worry about "reduc[ing] the list of BuildRequires".
In fact you should be doing just the opposite.

The issue of what a user needs at install time is completely different.
Provide a coq-emacs subpackage which contains the emacs components.
Users can optionally install this depending on their editor choice.

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

I think you're misunderstanding the difference between the build (which
happens once, on Fedora's Koji build system) and what users install (those
binary packages built by Koji).

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

No don't rebuild any tarballs.  Add a line to your %prep section to fix these,
eg:

  %prep
  mv text-file text-file.old
  iconv -f ISO-8859-1 -t UTF-8 < text-file.old > text-file
  rm bad-binary.gif

If the changes are more significant, use a patch instead.

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

Does coq ship libraries?  If so you should follow the OCaml package policy
for libraries, which would mandate a separate -devel subpackage.  The
generic 'foolib' spec file above is a good starting point for packaging
libraries.

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

It's not "build with the best possible binary".  Fedora packages should ship the
best possible binary of each program.  So you'll need something like this:

  %install
  %if %opt
  install parser.opt %{_bindir}/parser
  %else
  install parser %{_bindir}/parser
  %endif

BTW having a binary called /usr/bin/parser is probably a bad idea.  How do
Debian package this file?  They usually rename such generic names ('coqparser'
or the like).  If Debian rename it, then we should do so too.



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