Spec URL: http://jjames.fedorapeople.org/blast/blast.spec SRPM URL: http://jjames.fedorapeople.org/blast/blast-2.5-1.fc12.src.rpm Description: BLAST is a software model checker for C programs. The goal of BLAST is to be able to check that software satisfies behavioral properties of the interfaces it uses. BLAST uses counterexample-driven automatic abstraction refinement to construct an abstract model which is model checked for safety properties. The abstraction is constructed on-the-fly, and only to the required precision.
One thing that jumps out at me is the "ocaml-caddie" package it creates (CAml cuDD InterfacE). It isn't named as a subpackage but is a completely separate package. This "ocaml-caddie" package certainly looks useful, but is this really the right source for it? Or is there a better upstream we should be trying to use instead? (I presume this is different from MLCUDDIDL, which is also an OCaml binding to cuDD.) This draft package includes "vampyre", which is NOT open source software. This needs to be removed. Its license says: "Permission to use, copy, modify and distribute this software for research purposes only is hereby granted..." Note that it's ONLY permitted for use for "research purposes"... you are NOT allowed to use it for anything useful. Thus, it's not okay for Fedora to include it. Vampyre needs to be stripped out of this package. I hope it can still be used without it; if vampyre is 100% required, then this package is done for. Instead of: sed -i -e "s|@libdir@|%{_libdir}|" blast/psrc/Makefile sed -i -e "s|@libdir@|%{_libdir}|" blast/psrc2/Makefile sed -i -e "s|@libdir@|%{_libdir}|" blast/spec/Makefile Why not (so we can see it's all the same change): sed -i -e "s|@libdir@|%{_libdir}|" blast/psrc/Makefile \ blast/psrc2/Makefile blast/spec/Makefile Should the smp_mflags limitation be a "FIXME"? It's more just a fact of life. Looking over the installed files, I see all sorts of issues: %{_bindir}/htmlize %{_bindir}/mfilter %{_bindir}/pblast %{_bindir}/smt_solver %{_bindir}/smtlibServer %{_bindir}/spec %{_bindir}/vampyre %{_includedir}/blast As I noted above, it installs "vampyre", which isn't allowed. Also, a number of these other names are probably too generic to be acceptable. I bet there are a dozen "htmlize" programs. Other bad names include mfilter, smt_solver, smtlibServer, spec. Also, one weird thing... the package is named "blast", but the program isn't named "blast"? That's okay, but odd. It did build on a 32-bit x86. I can't easily use koji, since this depends on a package (csisat) not in the Fedora repository. I ran rpmlint using rpmlint blast.spec ../RPMS/i586/blast-2.5-1.fc11.i586.rpm ../RPMS/i586/ocaml-caddie-* ../SRPMS/blast-2.5-1.fc11.src.rpm and got 2 warning messages: blast.i586: W: devel-file-in-non-devel-package /usr/include/blast/assert.h ocaml-caddie-devel.i586: W: no-documentation 4 packages and 1 specfiles checked; 0 errors, 2 warnings. The first one is probably okay, and we can ignore the warning. The second one doesn't look good. ocaml-caddie should have SOME docs, yes? Thoughts?
I went through the "caddie" subdirectory, and in particular looked at caddieBdd.ml and caddie.c (the key source files). This software library is *not* under the ASL, but under the modified (3-clause) BSD license. That's not a *problem*... BSD is a well-known FLOSS license, and these licenses are legal to combine. But it means that the license statements aren't right. The ocaml-caddie package should have a "License" of "BSD" per http://fedoraproject.org/wiki/Licensing#Good_Licenses and not ASL 2.0.
Why doesn't the package build the gui (blastgui), at least as a subpackage? This would "BuildRequire: ocaml-lablgtk", then "make gui". (You'd need to set up a desktop, and find a way to set BLASTGUI, but sounds useful.) I compiled it and tried to run it as it is. It *did* work. I put this in file "foo.c": ================================= #include <assert.h> int foo(int x, int y) { if (x > y) { x = x - y; L: assert(x > 0); } } ================================= Then did: gcc -E -I /usr/include/blast/ foo.c > foo.tmp mfilter foo.tmp > foo.i pblast -main foo -smt foo.i Which eventually produced: No error found. The system is safe :-) You have to give it the "-smt", or it tries to use the Simplify prover, and since Simplify isn't there it fails.
Note to others: BLAST depends on two other applications, which have been packaged and approved for inclusion in the Fedora repository. See: https://bugzilla.redhat.com/show_bug.cgi?id=555160 https://bugzilla.redhat.com/show_bug.cgi?id=555161
Sorry to take so long with this, but you raised some thorny issues. I'm afraid that vampyre is, indeed, required. At least, I can't find a way to untangle it from the main code (grep for "vampyre" in blast/psrc). So I guess we're done: this package cannot be included in Fedora for licensing reasons. We should perhaps look at http://code.google.com/p/cpachecker/ instead. Its author, one of the BLAST maintainers, calls it a "better BLAST". On the other hand, they haven't reached a 1.0 release yet.
Ugh. Can you send an email to its developers? Maybe vampyre can be untangled by them. Packaging http://code.google.com/p/cpachecker/ is not a bad idea. Other alternatives are: Saturn http://saturn.stanford.edu/pages/overviewindex.html MOPS
I looked briefly at CPAchecker. There's a paper about it here: http://www.sosy-lab.org/~dbeyer/Publications/2009-SFU-TR002.CPAchecker_A_Tool_for_Configurable_Software_Verification.pdf The paper suggests that CPAchecker may depend on Simplify and MathSAT. I know that Simplify is not FLOSS (it's not even clear it's legal to distribute at all), and I don't think that MathSAT is FLOSS either. So CPAchecker may be unpackageable.
Good news! On Thu, 25 Feb 2010 14:45:56 -0800, Rupak Majumdar ( rupak /at/ CS, dot, UCLA , dot, EDU send to me this email: ============= David, I am the original developer of Blast (the only other tool I know that used Vampyre and is available) and we have gotten rid of vampyre dependencies. The latest version of Blast (not depending on vampyre) is at http://www.cs.ucla.edu/~rupak/b2/ I will also relicense vampyre, but will only get to it next week. ============= This "latest version of BLAST" is really a follow-on project, with a new project name "B2". It's released under the Apache 2.0 license, which is uncontroversially FLOSS. If you package B2, I suggest opening a different review request... it's a different name, different developer, etc. Once vampyre is released as FLOSS, you can continue with the BLAST packaging. I still think it's great to get vampyre released as FLOSS, even if you decide to not package BLAST itself and just package B2 or something else instead. As we package other stuff, I suspect we'll find other vampyre users :-).
Correction: It appears that B2 depends on Simplify. Simplify isn't FLOSS, and I doubt it ever will be. So if B2 really *requires* Simplify, then B2 cannot be packaged in the Fedora repository (or many others' either). But if vampyre is released as FLOSS, then to the best of my understanding we can re-open this review request, since it would then be possible to package BLAST in the Fedora repository.
I got more information from Rupak about B2 (his replacement for BLAST); B2 can work without Simplify. Thus, it *appears* that we could package B2, but we'll need to package dpt (and hope that there aren't any MORE license problems). Here is his Rupak's response: > There is a compile time option to get rid of simplify. At the moment, > there are backends to Simplify, > Yices (also not FLOSS) and DPT (FLOSS, dpt.sourceforge.net). > There is a component called Foci also not FLOSS, but an alternate > CSISAT which is FLOSS. Again, there is a compile time way to take out Foci.