[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq

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


https://bugzilla.redhat.com/show_bug.cgi?id=719150

Thomas Spura <tomspur at fedoraproject.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|NEW                         |ASSIGNED
         AssignedTo|nobody at fedoraproject.org    |tomspur at fedoraproject.org
               Flag|                            |fedora-review+

--- Comment #3 from Thomas Spura <tomspur at fedoraproject.org> 2011-10-26 17:10:30 EDT ---
(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

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