[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 Fedora Update System upda...@fedoraproject.org changed: What|Removed |Added Status|ON_QA |CLOSED Fixed In Version||flocq-1.4.0-3.fc16 Resolution||ERRATA Last Closed||2011-11-10 12:45:35 --- Comment #11 from Fedora Update System upda...@fedoraproject.org 2011-11-10 12:45:35 EST --- flocq-1.4.0-3.fc16 has been pushed to the Fedora 16 stable repository. -- 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. ___ package-review mailing list package-review@lists.fedoraproject.org https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 Fedora Update System upda...@fedoraproject.org changed: What|Removed |Added Status|MODIFIED|ON_QA --- Comment #10 from Fedora Update System upda...@fedoraproject.org 2011-10-31 21:27:00 EDT --- flocq-1.4.0-3.fc16 has been pushed to the Fedora 16 testing repository. -- 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. ___ package-review mailing list package-review@lists.fedoraproject.org https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 --- Comment #9 from Fedora Update System upda...@fedoraproject.org 2011-10-28 16:43:14 EDT --- 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 -- 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. ___ package-review mailing list package-review@lists.fedoraproject.org https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 Fedora Update System upda...@fedoraproject.org changed: What|Removed |Added Status|ASSIGNED|MODIFIED -- 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. ___ package-review mailing list package-review@lists.fedoraproject.org https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 toms...@fedoraproject.org changed:
What|Removed |Added
CC||toms...@fedoraproject.org
--- Comment #1 from Thomas Spura toms...@fedoraproject.org 2011-10-26
15:39:43 EDT ---
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?
--
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.
___
package-review mailing list
package-review@lists.fedoraproject.org
https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 --- Comment #2 from Jerry James loganje...@gmail.com 2011-10-26 16:36:46 EDT --- (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 -- 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. ___ package-review mailing list package-review@lists.fedoraproject.org https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 toms...@fedoraproject.org changed:
What|Removed |Added
Status|NEW |ASSIGNED
AssignedTo|nob...@fedoraproject.org|toms...@fedoraproject.org
Flag||fedora-review+
--- Comment #3 from Thomas Spura toms...@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.
___
package-review mailing list
package-review@lists.fedoraproject.org
https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 Jerry James loganje...@gmail.com changed: What|Removed |Added Flag||fedora-cvs? --- Comment #5 from Jerry James loganje...@gmail.com 2011-10-26 17:41:17 EDT --- New Package SCM Request === Package Name: flocq Short Description: Formalization of floating point numbers for Coq Owners: jjames Branches: f16 InitialCC: -- 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. ___ package-review mailing list package-review@lists.fedoraproject.org https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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
--- Comment #4 from Jerry James loganje...@gmail.com 2011-10-26 17:39:49 EDT
---
(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.
--
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.
___
package-review mailing list
package-review@lists.fedoraproject.org
https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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
--- Comment #6 from Thomas Spura toms...@fedoraproject.org 2011-10-26
18:01:05 EDT ---
(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 :(
--
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.
___
package-review mailing list
package-review@lists.fedoraproject.org
https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 --- Comment #7 from Jerry James loganje...@gmail.com 2011-10-26 18:21:31 EDT --- :-) 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. -- 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. ___ package-review mailing list package-review@lists.fedoraproject.org https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 --- Comment #8 from Jesse Keating jkeat...@redhat.com 2011-10-26 19:23:49 EDT --- Git done (by process-git-requests). -- 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. ___ package-review mailing list package-review@lists.fedoraproject.org https://admin.fedoraproject.org/mailman/listinfo/package-review
[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq
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 Jerry James loganje...@gmail.com changed: What|Removed |Added Blocks||719152 -- 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. ___ package-review mailing list package-review@lists.fedoraproject.org https://admin.fedoraproject.org/mailman/listinfo/package-review
