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=548607 --- Comment #4 from Jerry James <loganjerry@xxxxxxxxx> 2009-12-21 15:10:11 EDT --- Thanks for all the comments, David. Sorry to be slow responding. Darn viruses .... Comment 1: you're right about the version number. I'll fix that. There was a discussion on fedora-devel recently about not including the name of the package in its Summary field, and rpmlint complains if you do that. However, you have a good point about the expansion of PVS being purely historical. I've changed the Summary to "Interactive theorem prover from SRI". Patch0 is required for Fedora. No bundled libraries are allowed without an exception. As far as I know, other distributions have similar rules, so I don't see the point in making Patch0 optional. Furthermore, the PVS copy of mona has not kept up with upstream. There are multiple bug fixes in the current mona release that have never been copied over to the PVS version. (This is exactly the reason for the "no bundled libraries" rule, in fact.) I have, in fact, made Sam Owre aware that I'm doing this and why. I asked Sam for the missing documentation files at the beginning of November. He has never replied. I am not in contact with anyone else at SRI, but I suppose I could try locating John Rushby's contact information. Comment 2: I am also worried about that other "pvs". I'll make this one "pvs-sbcl". I think the current Provides is okay. /sbin/pvs is owned by the lvm2 package, which only provides these: config(lvm2) = 2.02.53-2.fc12 lvm2 = 2.02.53-2.fc12 lvm2(x86-64) = 2.02.53-2.fc12 so there is no conflict. I did the "pvs" Provides so that libraries of PVS theories can "Requires: pvs" and have that be satisfied by a PVS built by any supported Common Lisp. Thanks for the desktop entry. I have added that, with some modifications inspired by the coq desktop file. Comment 3: Do you have PVSEMACS=xemacs in your environment? If so, see http://calypso.tux.org/pipermail/xemacs-beta/2009-December/018035.html Those BDD-related messages are harmless. They are due to the way the Makefiles are set up, which assumes that you will be doing multiple builds in the same directory. You get those messages about failing to clean up the previous build on the first build ... which, of course, is the ONLY build when constructing an RPM. The total build time for me is usually 7-8 minutes, by the way. New files: http://jjames.fedorapeople.org/pvs/pvs-sbcl.spec http://jjames.fedorapeople.org/pvs/pvs-sbcl-4.2-1.20091008svn.fc12.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. _______________________________________________ Fedora-package-review mailing list Fedora-package-review@xxxxxxxxxx http://www.redhat.com/mailman/listinfo/fedora-package-review