[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
bugzilla at redhat.com
bugzilla at redhat.com
Wed Oct 26 21:10:31 UTC 2011
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.
More information about the package-review
mailing list