Spec URL: http://jjames.fedorapeople.org/flocq/flocq.spec SRPM URL: http://jjames.fedorapeople.org/flocq/flocq-1.4.0-1.fc15.src.rpm Description: Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq. This package is needed to enable optional functionality in the why-coq and gappa packages.
PREREVIEW: Good: - group ok - License ok - rpmling ignorable/expected warnings $ rpmlint /home/tom/rpmbuild/RPMS/x86_64/flocq-1.4.0-1.fc15.x86_64.rpm /home/tom/rpmbuild/SRPMS/flocq-1.4.0-1.fc15.src.rpm flocq.x86_64: W: spelling-error %description -l en_US multi -> mulch, mufti flocq.x86_64: W: spelling-error %description -l en_US radix -> radii, radio, rad ix flocq.x86_64: E: no-binary flocq.x86_64: W: only-non-binary-in-usr-lib flocq.src: W: spelling-error %description -l en_US multi -> mulch, mufti flocq.src: W: spelling-error %description -l en_US radix -> radii, radio, rad ix flocq.src:30: W: configure-without-libdir-spec 2 packages and 0 specfiles checked; 1 errors, 6 warnings. - arch ok (needs to be in /usr/lib64 although noarch) - %files ok %{_libdir}/coq/user-contrib/ is owned by coq (a R) NEEDSWORK: - Please use INSTALL="install -p" for preserving timestamps Just a few questions, before I'll approve this: * Don't the source belongs to a devel package like other packages? (Don't know how that usually works in ocalm.) Or are the sources needed at runtime? * When the source are needed at runtime, this looks like a bug in the Makefile, so it should be installed automaticalls isn't it?
(In reply to comment #1) > NEEDSWORK: > - Please use INSTALL="install -p" for preserving timestamps I use "cp -p" for the source files, so their timestamps are preserved. All of the other files are generated, the *.vo files by coq and the documentation files by coqdoc, so their timestamps don't matter. > Just a few questions, before I'll approve this: > * Don't the source belongs to a devel package like other packages? > (Don't know how that usually works in ocalm.) > Or are the sources needed at runtime? Heh. This is the first-ever Coq add-on in Fedora, so we're blazing new territory. These aren't actually ocaml files. The Coq tool is written in ocaml, but it has its own input language, which is what these files are written in. Coq is a formal proof assistant, so the *.v files are written in a formal logic, which coq checks for correctness. Other programs which need flocq only need the compiled (*.vo) files. I just thought that humans developing new proofs that require coq would also want to see the source files. So .... yes, I guess those should go into a -devel package. Spec URL: http://jjames.fedorapeople.org/flocq/flocq.spec SRPM URL: http://jjames.fedorapeople.org/flocq/flocq-1.4.0-2.fc15.src.rpm
(In reply to comment #2) > (In reply to comment #1) > > NEEDSWORK: > > - Please use INSTALL="install -p" for preserving timestamps > > I use "cp -p" for the source files, so their timestamps are preserved. All of > the other files are generated, the *.vo files by coq and the documentation > files by coqdoc, so their timestamps don't matter. OK > > Just a few questions, before I'll approve this: > > * Don't the source belongs to a devel package like other packages? > > (Don't know how that usually works in ocalm.) > > Or are the sources needed at runtime? > > Heh. This is the first-ever Coq add-on in Fedora, so we're blazing new > territory. These aren't actually ocaml files. The Coq tool is written in > ocaml, but it has its own input language, which is what these files are written > in. Coq is a formal proof assistant, so the *.v files are written in a formal > logic, which coq checks for correctness. Sounds like you should do a packaging draft and send it to fpc. Maybe further extending this one for Coq add-ons: https://fedoraproject.org/wiki/Packaging/OCaml > Other programs which need flocq only need the compiled (*.vo) files. I just > thought that humans developing new proofs that require coq would also want to > see the source files. So .... yes, I guess those should go into a -devel > package. > > Spec URL: http://jjames.fedorapeople.org/flocq/flocq.spec > SRPM URL: http://jjames.fedorapeople.org/flocq/flocq-1.4.0-2.fc15.src.rpm New no-go: %files %dir %{flocqdir} That's already owned by coq, so this shoudn't own it. The rest looks sane to me. ######################################################## Please unown %{flocqdir} on importing and this is: ######################################################### APPROVED
(In reply to comment #3) > Sounds like you should do a packaging draft and send it to fpc. > Maybe further extending this one for Coq add-ons: > https://fedoraproject.org/wiki/Packaging/OCaml That's a good idea. It would be good to have other people's eyes on the way I'm packaging this stuff, to see if they spot any problems. > New no-go: > %files > %dir %{flocqdir} > > That's already owned by coq, so this shoudn't own it. No, coq owns the parent directory, %{_libdir}/coq/user-contrib. The flocqdir macro expands to %{_libdir}/coq/user-contrib/Flocq. > APPROVED Thank you very much for the review. I appreciate it.
New Package SCM Request ======================= Package Name: flocq Short Description: Formalization of floating point numbers for Coq Owners: jjames Branches: f16 InitialCC:
(In reply to comment #4) > > That's already owned by coq, so this shoudn't own it. > > No, coq owns the parent directory, %{_libdir}/coq/user-contrib. The flocqdir > macro expands to %{_libdir}/coq/user-contrib/Flocq. I shouldn't do a review this late... Will comment to your trickier review request at another time :(
:-) Actually, I think the espresso review was comparable to this one in difficulty. I don't think you owe me any more reviews, unless you have more you want me to do for you.
Git done (by process-git-requests).
flocq-1.4.0-3.fc16 has been submitted as an update for Fedora 16. https://admin.fedoraproject.org/updates/flocq-1.4.0-3.fc16
flocq-1.4.0-3.fc16 has been pushed to the Fedora 16 testing repository.
flocq-1.4.0-3.fc16 has been pushed to the Fedora 16 stable repository.