[Bug 529404] Review Request: cvc3 - Validity checker of many-sorted first-order formulas with theories

[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=529404





--- Comment #1 from David A. Wheeler <dwheeler at dwheeler.com>  2009-10-16 15:13:29 EDT ---
I'm looking through it right now.  Here are a few quick comments, a more formal
review to come.

It looks like the license problems are completely gone!!  I double-checked the
main license in LICENSE.in; the nasty non-BSD clause originally there (aka the
"pay up if I get sued" clause) is gone.  Hooray!!  The LICENSE.in file gives a
short list of files with different licenses; I looked at every one of those
files, and they're clearly BSD-style as well.  CVC3 version 1.2 had zchaff,
which could be removed; this version of CVC3 doesn't even INCLUDE zchaff as far
as I can tell, so there aren't any zchaff licensing issues either.  So happily,
it looks like the licensing problems are completely gone.  Excellent!

This package doesn't enable the Java interface (--enable-java).  At first, I
thought that was unfortunate, but then I noticed that the documentation says
that the interface is "experimental" and "may change".  So, you might want to
consider enabling the interface, but given that description, perhaps it's just
as well.  Java apps can always use the command-line interface anyway.

I know of no rule forbidding the use of "%makeinstall".  The rule, as I
understand it, is that you should NOT use %makeinstall if "make DESTDIR=..."
works.  But DESTDIR isn't supported by CVC3's makefile, so that rule doesn't
apply.  So I think the %%makefile comment is misleading, but directly invoking
make (as you've done) is okay.  For more info, see:
http://fedoraproject.org/wiki/Packaging/Guidelines#Why_the_.25makeinstall_macro_should_not_be_used

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