Bug 719150 - Review Request: flocq - Formalization of floating point numbers for Coq
Summary: Review Request: flocq - Formalization of floating point numbers for Coq
Keywords:
Status: CLOSED ERRATA
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: Thomas Spura
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks: 719152
TreeView+ depends on / blocked
 
Reported: 2011-07-05 21:47 UTC by Jerry James
Modified: 2011-11-10 17:45 UTC (History)
3 users (show)

Fixed In Version: flocq-1.4.0-3.fc16
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2011-11-10 17:45:35 UTC
Type: ---
tomspur: fedora-review+
jkeating: fedora-cvs+


Attachments (Terms of Use)

Description Jerry James 2011-07-05 21:47:24 UTC
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.

Comment 1 Thomas Spura 2011-10-26 19:39:43 UTC
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?

Comment 2 Jerry James 2011-10-26 20:36:46 UTC
(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

Comment 3 Thomas Spura 2011-10-26 21:10:30 UTC
(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

Comment 4 Jerry James 2011-10-26 21:39:49 UTC
(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.

Comment 5 Jerry James 2011-10-26 21:41:17 UTC
New Package SCM Request
=======================
Package Name: flocq
Short Description: Formalization of floating point numbers for Coq
Owners: jjames
Branches: f16
InitialCC:

Comment 6 Thomas Spura 2011-10-26 22:01:05 UTC
(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 :(

Comment 7 Jerry James 2011-10-26 22:21:31 UTC
:-)  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.

Comment 8 Jesse Keating 2011-10-26 23:23:49 UTC
Git done (by process-git-requests).

Comment 9 Fedora Update System 2011-10-28 20:43:14 UTC
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

Comment 10 Fedora Update System 2011-11-01 01:27:00 UTC
flocq-1.4.0-3.fc16 has been pushed to the Fedora 16 testing repository.

Comment 11 Fedora Update System 2011-11-10 17:45:35 UTC
flocq-1.4.0-3.fc16 has been pushed to the Fedora 16 stable repository.


Note You need to log in before you can comment on or make changes to this bug.