Spec URL: http://ninth-circle.dnsalias.com/~adunn/coq/coq.spec SRPM URL: http://ninth-circle.dnsalias.com/~adunn/coq/coq-8.1pl3-1.fc9.src.rpm Description: Review Request: coq - Coq proof management system I packaged up the formal proof management system Coq and would appreciate a review. This is my first package contribution, and I am in need of a sponsor. Coq is a formal proof management system. It allows for the development of theorems through first order logic that are mechanically checked by the machine. Sets of definitions and theorems can be saved as compiled modules and loaded into the system. Coq is based off of OCaml.
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.