This is excellent - I'm glad to see this package!!!

I have a nit about this description, I think it needs to be clearer.
I realize it's similar to the Debian text, but I think the Debian
text isn't clear at all. Also,
Coq is an _interactive_ prover, not an automatic prover, and I
think it's important to note that.

How about this description instead (starting with the text on their
website, but changing "done with" to "interactively developed using",
and adding in the stuff from the submitted description):

***

Coq is a formal proof management system: a proof interactively developed using
Coq is mechanically checked by the machine. In particular, Coq allows
users to define functions or predicates,
to state mathematical theorems and software specifications,
to develop interactively formal proofs of these theorems, and
to check these proofs by a relatively small certification "kernel".
Sets of definitions and theorems can be saved as compiled modules and loaded
into the system.
Coq has been used to formally prove claims about real programs
(see the Coq website for more).
Coq uses first order logic, and is implemented with OCaml.

***

Thanks!!

Oh, one additional thing to add to the description (say, to the end of it):

Coq is pronounced "coke".



It's hard to talk about a package without knowing how to pronounce it.
Coq is the French word for "rooster", e.g., "Coq au vin".
Here are some justifications for this pronunciation:
http://tastingspoons.blogspot.com/2008/02/quick-modern-coq-au-vin.html
http://www.bigoven.com/72191-Coq-Au-Vin-recipe.html

Subpackage "coq-coqide" should be renamed to "coqide", i.e., change:
 %package coqide
to:
 %package -n coqide
Normally I'd suggest naming this "coq-ide", but since the Ubuntu/Debian package
is named "coqide", I'd use the same name they do (as I think you intended to do).

The "coqide" package doesn't seem to create a GUI icon (desktop entry).
You need to create a small "desktop entry" file as part of the build
and install it, as discussed here:
http://fedoraproject.org/wiki/Packaging/Guidelines#Desktop_files
Here's the desktop entry spec:
http://standards.freedesktop.org/desktop-entry-spec/latest/
If glade2 is installed, you can look here at another example:
/usr/share/applications/gnome-glade-2.desktop

(In reply to comment #3)
> Subpackage "coq-coqide" should be renamed to "coqide", i.e., change:
>  %package coqide
> to:
>  %package -n coqide

I was just trying to emphasize that it is indeed a subpackage of coq; if that's
not proper it can certainly be changed.

> Normally I'd suggest naming this "coq-ide", but since the Ubuntu/Debian package
> is named "coqide", I'd use the same name they do (as I think you intended to do).

Also, coq-coqide matches both coqide and ide text-wise, but coq-ide does not
match coqide text-wise. I was afraid searches for the text coqide could
potentially mess up.

> The "coqide" package doesn't seem to create a GUI icon (desktop entry).
> You need to create a small "desktop entry" file as part of the build
> and install it, as discussed here:
> http://fedoraproject.org/wiki/Packaging/Guidelines#Desktop_files
> Here's the desktop entry spec:
> http://standards.freedesktop.org/desktop-entry-spec/latest/
> If glade2 is installed, you can look here at another example:
> /usr/share/applications/gnome-glade-2.desktop

This part I admittedly missed, and will fix.

> I was just trying to emphasize that it is indeed a subpackage of coq;
> if that's not proper it can certainly be changed.

Oh! I see!  That's a good idea.  In that case, I suggest documenting that
in the spec file as a comment, e.g.:

# The IDE's package name will become "coq-coqide".  That way, searching for
# either "coqide" (the Ubuntu/Debian package name) or "coq" will find this.

I fixed the desktop entry issue and also packaged the documentation for Coq in
subpackage coq-doc. The new files are in place of the original files, and the
original files can still be reached by appending ".v1" to each of the original URLs.

Another alternative is to call it coq-ide and make it Provides: coqide =
%{version}-%{release} ?

I was hoping to see coq packaged for Fedora -- great to see this coming along
(alas, I can't sponsor). Have you sent a mail to fedora-devel? It's easy for a
package to get lost in the submission queue.

Server appears to be down. To make reviewing easier, could I suggest that you
attach the spec file as an attachment?

Created attachment 308652 [details]
The main coq spec file

Given that access to the server seems to be flakier/slower than I anticipated, I
put up an alternate site:

The URLs

http://www.duke.edu/~amd34/coq/coq-8.1pl3-1.fc9.src.rpm
http://www.duke.edu/~amd34/coq/coq.spec

will also work, and may actually give better performance. (The corresponding
".v1" URLs will also be active, but are currently uploading.)

From the changelog section in the spec file..

%changelog
* Wed Jun 14 2008 Alan Dunn <amdunn> 8.1pl3-1
- Initial version.

Initial version?  Maybe "Initial Fedora rpm/package" or something along those
lines maybe since it's at version 8 already?

It's too bad rpm doesn't have a "Suggests:" tag.  Perhaps the description could add:
"coqtop users may want to install and use rlwrap, e.g., 'rlwrap coqtop', or use
an IDE."

Basically, coqtop doesn't include readline (for history and line editing), which
makes it annoying to use directly.  Installing and using rlwrap fixes that, but
it's not _required_ so rlwrap shouldn't be a dependency.

In reply to comment 12: I think you should just Require: rlwrap
It's not a big package, just 49K, and rlwrap really improves usability
of coq (and OCaml).

I'm taking this package for review now.

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

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.

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.

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

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

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

BTW, I had a look at the Debian package and they're applying no fewer than 7 patches.
You might want to check if any of those are relevant to Fedora.

Also they ship parser as /usr/bin/parser, so I guess we can leave that for now.

Link to Debian package:
http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/trunk/debian/?rev=0&sc=0

Thanks for all the comments. I thought I'd let all interested know that I'm
currently working on addressing these points, and will try and have a new
version ready as soon as possible.

(In reply to comment #18)
> Link to Debian package:
>
http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/trunk/debian/?rev=0&sc=0
> 

I suggest doing the following, which implements history and line editing
in coqtop (as well as justifying a dependency on rlwrap):

Inside the directory "/etc/profile.d", install 2 trivial files
"coq.sh" and "coq.csh", with the trivial contents shown below.
Then, when you log into a shell you'll get aliases that enable
history and line editing.  Make sure that the files are
readable (and executable) by all.  {bash invokes this via /etc/bashrc.}


::::::::::::::
coq.sh
::::::::::::::
# coq initialization

alias coqtop='rlwrap coqtop' 2>/dev/null


::::::::::::::
coq.csh
::::::::::::::
#! /bin/csh -f
alias coqtop 'rlwrap coqtop'

I created a new version of this package, available at

http://www.duke.edu/~amd34/coq/coq.spec
http://www.duke.edu/~amd34/coq/coq-8.1pl3-1.fc9.src.rpm

Among the things changed:
- Fixed tex, emacs directory issues (by changing BuildRequires)
- Fixed bugs I noticed with stripping exactly when appropriate, documentation 
directory permissions

In order to fix the stripping issue, I had to disable the creation of debug 
info and change the post install script (as indicated at the top of the spec 
file) - I didn't see any other way.

- Made desktop icon, menu entry
- Looked at Debian patches, applied when appropriate (documented in the spec 
file)

This new version builds on Koji for i386:
http://koji.fedoraproject.org/koji/taskinfo?taskID=666435
but appears to fail for ppc64 (as part of:)
http://koji.fedoraproject.org/koji/taskinfo?taskID=666507
I'm working on this - the exact reason isn't clear to me.

I've run rpmlint on all the packages - the main output is about non-stripped 
binaries that are bytecode compilations -> shouldn't really be stripped.

Sorry things took so long!

Build failure is limited to ppc64 architecture, potential fix for now would be
an architecture exclusion, like with:

http://koji.fedoraproject.org/koji/taskinfo?taskID=670200

(That version was made with an altered SPEC file that just includes the line
ExcludeArch ppc64.)

Perhaps the problem is with OCaml support on ppc64? I remember reading that
there were some difficulties about this in the recent past.

One can do slightly better on ppc64 - the bytecode version compiles, but it
seems as though any compile fails for ppc64 on f10, I think some change was
recently made that breaks compiles there - everything works fine on f9, and a
build with a spec file that incorporates the modification to use bytecode on
ppc64 is here:

http://koji.fedoraproject.org/koji/taskinfo?taskID=671994

In any case, I believe all of the relevant issues people have raised have been
addressed and that this package is ready for review for inclusion into the
repository.

Hi - congrats to Alan Dunn, I think this looks like a good package!

Just a note - my comment 20 described how to wrap up coqtop using rlwrap when
you invoke coqtop interactively.  Unfortunately, Alan Dunn found that doing that
has some problems.  For example, pasting sometimes doesn't work as expected.  So
he's convinced me that this automatic wrapping should NOT be done, and that his
packaging as it stands is the better approach.

I made one last change to the SPEC file and source RPM: I was unclear as to the 
nature of the message from rpmlint that "only binaries should go in /usr/lib", 
as I had only compiled Coq .vo files in /usr/lib. As it turns out that only 
architecture dependent binary files should go in /usr/lib, I moved all these to 
%{_datadir} (which is usually /usr/share) and the message from rpmlint was then 
fixed. The new SPEC file and source RPM remain at the same location at the 
duke.edu address (and the old ones were moved to ".v1" and so forth as before).

Taking this bug for review now.

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.

The preceding two issues have been addressed:

- A new version of the spec file, which works with dist-f10, can be found 
through

http://koji.fedoraproject.org/koji/taskinfo?taskID=700547

which includes the change to remove "make clean" from the %clean section as 
desired. I assume also that the version desired for commit to the repositories 
is the one that works with dist-f10, and thus must have ppc64 as an excluded 
architecture.

- I am under the impression that the bug is supposed to be filed after the 
package is committed, as otherwise there's no way (that I can see) to indicate 
the package that has a bug - there's no coq package bugzilla page. However, I 
will file the bug with blocker FE-ExcludeArch-ppc64 when an appropriate page 
exists and this will have the following description:

Exception raised during Koji ppc64 build of coq package. Problem is not fixed 
by restricting to byte-code compilation instead of native-code compilation.
(Failed) Build logs with dist-f10 available at

http://koji.fedoraproject.org/koji/taskinfo?taskID=700733

Build succeeds (with native-code compilation) for dist-f9, available at 

http://koji.fedoraproject.org/koji/taskinfo?taskID=699677

so error must be Fedora 10 specific.

(Is it ok to reference the koji builds like that? Will they disappear after a 
while -> should duplicate/put the results somewhere else?)

Are those acceptable resolutions?

Looks good.

APPROVED.

Hey Alan, I would be happy to sponsor you. 

Please continue the process at: 
http://fedoraproject.org/wiki/PackageMaintainers/Join#Add_Package_to_CVS_and_Set_Owner

If you have any questions at all with processes and procedures, feel free to
email me directly, or find me on irc.freenode.com (nickname: nirik). 

New Package CVS Request
=======================
Package Name: coq
Short Description: Coq proof management system
Owners: amdunn
Branches: F-8 F-9
Cvsextras Commits: yes

Hey Alan. 

Is the spec link in comment #21 the current one? 
I can't seem to get it from the koji links. 
(Side note: it's best to bump the spec version and add a changelog entry for
changes in review, then everyone can be sure they have the latest version and
there is a history of changes). 

I would like to take a quick look before you import and see if I can suggest any
solutions to anything. In particular it sounds like you are disabling debuginfo,
but there may be some ways to get around that. Also, perhaps we can track down
the ppc64 issue real quick. 

I realize this in retrospect (re: versions during review), though I originally
thought that was only after the original version was committed.

The links in 21 are current, though it seems to me that there is still a link in
the Koji build (here:
http://koji.fedoraproject.org/koji/getfile?taskID=699678&name=coq-8.1pl3-1.fc9.src.rpm
however, oddly enough, it seems that the system only stores a link to the source
rpm in one of the build branches each time, I believe the one that is listed first.)

It is true that I'm disabling debuginfo, as otherwise bytecode OCaml executables
are stripped and rendered inoperable. If there's a better way to do that, like
finding a way to selectively disable stripping from the debuginfo scripts, then
I can certainly change things to get that to work. The ppc64 build error was
pretty odd - the build logs were not much help at all in figuring out the
problem - I think one would really need access to a ppc64 system (which I don't
have) to make progress on that front.

(In reply to comment #32)
> Hey Alan. 
> 
> Is the spec link in comment #21 the current one? 
> I can't seem to get it from the koji links. 
> (Side note: it's best to bump the spec version and add a changelog entry for
> changes in review, then everyone can be sure they have the latest version and
> there is a history of changes). 
> 
> I would like to take a quick look before you import and see if I can suggest any
> solutions to anything. In particular it sounds like you are disabling debuginfo,
> but there may be some ways to get around that. Also, perhaps we can track down
> the ppc64 issue real quick. 
> 
> 

We disable debuginfo in all ocaml packages because it's not useful.  OCaml
has its own debugger and doesn't provide the necessary dwarf data to use
gdb in anything other than a 'basic' (function names only) mode.

This is the base specfile I use for libraries:
https://fedoraproject.org/w/uploads/5/5c/Packaging_OCaml_ocaml-foolib.spec

Ah yes. I recall that now... 

I did a scratch build of the src.rpm from comment 21, and it built ok on ppc64
(with the unopt line in there): 

http://koji.fedoraproject.org/koji/taskinfo?taskID=717510

So, I would say there isn't any need to exclude ppc64 right now, but you should
try and figure out why the opt compiler doesn't work there. 

cvs done.

coq-8.1pl3-1.fc9 has been submitted as an update for Fedora 9

coq-8.1pl3-1.fc9 has been pushed to the Fedora 9 stable repository.  If problems still persist, please make note of it in this bug report.