Version bump, bug #311903.

Package-Manager: portage-2.1.8.3/cvs/Linux i686

4 files changed, 230 insertions, 12 deletions

diff --git a/sci-mathematics/nusmv/ChangeLog b/sci-mathematics/nusmv/ChangeLog
index fd5b881a55ff..90480a1f68e7 100644
--- a/sci-mathematics/nusmv/ChangeLog
+++ b/sci-mathematics/nusmv/ChangeLog
@@ -1,6 +1,12 @@
 # ChangeLog for sci-mathematics/nusmv
 # Copyright 1999-2010 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/nusmv/ChangeLog,v 1.8 2010/01/13 16:48:53 bicatali Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/nusmv/ChangeLog,v 1.9 2010/06/22 20:03:17 phajdan.jr Exp $
+
+*nusmv-2.5.0 (22 Jun 2010)
+
+  22 Jun 2010; Pawel Hajdan jr <phajdan.jr@gentoo.org>
+  +files/MiniSat_v1.14_gcc41.patch, +nusmv-2.5.0.ebuild:
+  Version bump, bug #311903.
 
   13 Jan 2010; Sébastien Fabbro <bicatali@gentoo.org> nusmv-2.3.1.ebuild:
   Added VARTEXFONTS, bug #223077
diff --git a/sci-mathematics/nusmv/Manifest b/sci-mathematics/nusmv/Manifest
index 4368fadaea23..f94ebabc1c2c 100644
--- a/sci-mathematics/nusmv/Manifest
+++ b/sci-mathematics/nusmv/Manifest
@@ -1,16 +1,9 @@
------BEGIN PGP SIGNED MESSAGE-----
-Hash: SHA1
-
 AUX MiniSat_v1.14-optimizedlib.patch 1112 RMD160 9ae63aef1b74fac1bad9ee62049460856b5c5982 SHA1 7a2ee88eef0591690a2a728c07b68fdd882addda SHA256 21016b1ce69553c058385afa93f13248dbdc398c7968609d86dd9b707e227bfb
+AUX MiniSat_v1.14_gcc41.patch 4568 RMD160 59cccf1bfd15a4913c6026875639212859ce1ffa SHA1 532288df7231053ec41bbc11a02a1ec12ec396a4 SHA256 05179a822cca176f76340b2a5a9ffab1128d7018a1dfee743fb937abdc8233d9
 DIST MiniSat_v1.14_src.zip 29428 RMD160 d5f0dc611a6116128d9a404f9045e02b185958b4 SHA1 266536cf5e5e77aa0478b98869bcd67ac1a523b6 SHA256 8e5e0ee84a770dcb3abd6fc65ed4aef938f9ffabca5ddc8a739029f7fb58a8f5
 DIST NuSMV-2.3.1.tar.gz 2590944 RMD160 74f00e1c29dabe98e04cf0d652b92d63a73b07dc SHA1 588d3b43f136273176f4a6056b474f9d872b977b SHA256 b8ba0f29afafdfdef8c30f722eead3ef6cbb17e4bfe5563240a01d8a99dbbf68
+DIST NuSMV-2.5.0.tar.gz 3792968 RMD160 aaa3b9dc1329ad3feca6c9511b144437caf83472 SHA1 4b2837b0511e9eaf0eee53395308e8eaba6be727 SHA256 59310f5f23f72cb1ad16419e40f245db7c5aa41c0f59ba5c75732bb6c4b56ff1
 EBUILD nusmv-2.3.1.ebuild 3331 RMD160 09aa89279858b6a6ac1be71adaf54545d4dffc54 SHA1 36c394fa4bbc8053059bd19be61ae8679983eb53 SHA256 43f713b4e5f21318516348f732f4129670235317724ce595d1e635aa0fbd91cd
-MISC ChangeLog 1356 RMD160 82fb9a1381f05b2c643dd2e11c6f907336800d37 SHA1 af2ee0e584af336b1864e598e2c613f36c7c8300 SHA256 f5b7a780e1e0f4f58eaf3e9025a31929ca37d215631409ddd4af49c6e43c5086
+EBUILD nusmv-2.5.0.ebuild 3504 RMD160 5c4594ec3c14bd77fefb7346e8736c52385fd145 SHA1 feb109b871e3f50028e7511151d3392b9ba546d3 SHA256 bd2396e81e30647d88334f9cb6f71b0b75414de49eadf7d2e8b1ffe20634518e
+MISC ChangeLog 1528 RMD160 e7b6b30f32950d1c18bb9095b6e9b9758a0bf556 SHA1 10d7264837b2a1fcb4af40cdd55daf2353d98aa2 SHA256 341299d9a7043a303f8d11b39dca07557a71e348dd1504b6871d1938496262d4
 MISC metadata.xml 301 RMD160 95f4a72bad52574229901ce16d7d503b68cb22f9 SHA1 a62c653d31a41d1e11cea40d2d9366676d67d333 SHA256 b7f1f13dae0ffaaf9894bf5f5a95b351d63c630e9ccaab304b1edb8fa8f1c18c
------BEGIN PGP SIGNATURE-----
-Version: GnuPG v2.0.14 (GNU/Linux)
-
-iEYEARECAAYFAktOAgoACgkQ1ycZbhPLE2ApZACfQzxCrKqtPob3XwjbHxLGiai5
-vzMAn2IaaIqDNuoqEsj+hUeoms2x2w5q
-=gXuV
------END PGP SIGNATURE-----
diff --git a/sci-mathematics/nusmv/files/MiniSat_v1.14_gcc41.patch b/sci-mathematics/nusmv/files/MiniSat_v1.14_gcc41.patch
new file mode 100644
index 000000000000..dd5856ae57e5
--- /dev/null
+++ b/sci-mathematics/nusmv/files/MiniSat_v1.14_gcc41.patch
@@ -0,0 +1,92 @@
+Index: MiniSat/MiniSat_v1.14/SolverTypes.h
+===================================================================
+--- MiniSat/MiniSat_v1.14/SolverTypes.h	(revision 1040)
++++ MiniSat/MiniSat_v1.14/SolverTypes.h	(working copy)
+@@ -42,19 +42,32 @@
+ public:
+     Lit() : x(2*var_Undef) {}   // (lit_Undef)
+     explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { }
+-    friend Lit operator ~ (Lit p) { Lit q; q.x = p.x ^ 1; return q; }
++    friend Lit operator ~ (Lit p);
+ 
+-    friend bool sign  (Lit p) { return p.x & 1; }
+-    friend int  var   (Lit p) { return p.x >> 1; }
+-    friend int  index (Lit p) { return p.x; }                // A "toInt" method that guarantees small, positive integers suitable for array indexing.
+-    friend Lit  toLit (int i) { Lit p; p.x = i; return p; }  // Inverse of 'index()'.
+-    friend Lit  unsign(Lit p) { Lit q; q.x = p.x & ~1; return q; }
+-    friend Lit  id    (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; }
++    friend bool sign  (Lit p);
++    friend int  var   (Lit p);
++    friend int  index (Lit p); // A "toInt" method that guarantees small, positive integers suitable for array indexing.
++    friend Lit  toLit (int i); // Inverse of 'index()'.
++    friend Lit  unsign(Lit p);
++    friend Lit  id    (Lit p, bool sgn);
+ 
+-    friend bool operator == (Lit p, Lit q) { return index(p) == index(q); }
+-    friend bool operator <  (Lit p, Lit q) { return index(p)  < index(q); }  // '<' guarantees that p, ~p are adjacent in the ordering.
++    friend bool operator == (Lit p, Lit q);
++    friend bool operator <  (Lit p, Lit q); // '<' guarantees that p, ~p are adjacent in the ordering.
+ };
+ 
++inline Lit operator ~ (Lit p) { Lit q; q.x = p.x ^ 1; return q; }
++
++inline bool sign  (Lit p) { return p.x & 1; }
++inline int  var   (Lit p) { return p.x >> 1; }
++inline int  index (Lit p) { return p.x; }                // A "toInt" method that guarantees small, positive integers suitable for array indexing.
++inline Lit  toLit (int i) { Lit p; p.x = i; return p; }  // Inverse of 'index()'.
++inline Lit  unsign(Lit p) { Lit q; q.x = p.x & ~1; return q; }
++inline Lit  id    (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; }
++
++inline bool operator == (Lit p, Lit q) { return index(p) == index(q); }
++inline bool operator <  (Lit p, Lit q) { return index(p)  < index(q); }  // '<' guarantees that p, ~p are adjacent in the ordering.
++
++
+ const Lit lit_Undef(var_Undef, false);  // }- Useful special constants.
+ const Lit lit_Error(var_Undef, true );  // }
+ 
+@@ -79,11 +92,7 @@
+         if (learnt) activity() = 0; }
+ 
+     // -- use this function instead:
+-    friend Clause* Clause_new(bool learnt, const vec<Lit>& ps) {
+-        assert(sizeof(Lit)      == sizeof(uint));
+-        assert(sizeof(float)    == sizeof(uint));
+-        void*   mem = xmalloc<char>(sizeof(Clause) + sizeof(uint)*(ps.size() + (int)learnt));
+-        return new (mem) Clause(learnt, ps); }
++    friend Clause* Clause_new(bool learnt, const vec<Lit>& ps);
+ 
+     int       size        ()      const { return size_learnt >> 1; }
+     bool      learnt      ()      const { return size_learnt & 1; }
+@@ -92,6 +101,12 @@
+     float&    activity    ()      const { return *((float*)&data[size()]); }
+ };
+ 
++inline Clause* Clause_new(bool learnt, const vec<Lit>& ps) {
++        assert(sizeof(Lit)      == sizeof(uint));
++        assert(sizeof(float)    == sizeof(uint));
++        void*   mem = xmalloc<char>(sizeof(Clause) + sizeof(uint)*(ps.size() + (int)learnt));
++        return new (mem) Clause(learnt, ps); 
++}
+ 
+ //=================================================================================================
+ // GClause -- Generalize clause:
+@@ -102,8 +117,8 @@
+     void*   data;
+     GClause(void* d) : data(d) {}
+ public:
+-    friend GClause GClause_new(Lit p)     { return GClause((void*)((index(p) << 1) + 1)); }
+-    friend GClause GClause_new(Clause* c) { assert(((uintp)c & 1) == 0); return GClause((void*)c); }
++    friend GClause GClause_new(Lit p);
++    friend GClause GClause_new(Clause* c); 
+ 
+     bool        isLit    () const { return ((uintp)data & 1) == 1; }
+     bool        isNull   () const { return data == NULL; }
+@@ -114,6 +129,8 @@
+ };
+ #define GClause_NULL GClause_new((Clause*)NULL)
+ 
++inline GClause GClause_new(Lit p) { return GClause((void*)((index(p) << 1) + 1)); }
++inline GClause GClause_new(Clause* c) { assert(((uintp)c & 1) == 0); return GClause((void*)c); }
+ 
+ //=================================================================================================
+ #endif
diff --git a/sci-mathematics/nusmv/nusmv-2.5.0.ebuild b/sci-mathematics/nusmv/nusmv-2.5.0.ebuild
new file mode 100644
index 000000000000..15461364a9de
--- /dev/null
+++ b/sci-mathematics/nusmv/nusmv-2.5.0.ebuild
@@ -0,0 +1,127 @@
+# Copyright 1999-2010 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/nusmv/nusmv-2.5.0.ebuild,v 1.1 2010/06/22 20:03:17 phajdan.jr Exp $
+
+inherit eutils toolchain-funcs
+
+NUSMV_PN="NuSMV"
+NUSMV_PV="${PV}"
+NUSMV_P="${NUSMV_PN}-${NUSMV_PV}"
+NUSMV_A="${NUSMV_P}.tar.gz"
+NUSMV_S="${WORKDIR}/${NUSMV_P}/nusmv"
+
+MINISAT_PN="MiniSat"
+MINISAT_PV="1.14"
+MINISAT_P="${MINISAT_PN}_v${MINISAT_PV}"
+MINISAT_A="${MINISAT_P}_src.zip"
+MINISAT_S="${WORKDIR}/${NUSMV_P}/MiniSat/${MINISAT_P}"
+
+CUDD_PN="cudd"
+CUDD_PV="2.4.1.1"
+CUDD_P="${CUDD_PN}-${CUDD_PV}"
+#CUDD_A is none
+CUDD_S="${WORKDIR}/${NUSMV_P}/${CUDD_P}"
+
+DESCRIPTION="NuSMV: new symbolic model checker"
+HOMEPAGE="http://nusmv.irst.itc.it/"
+# The Homepage is _very_ slow, 2Kb/sec or worse.
+# So we use our own mirror.
+# Additionally, MiniSat is distributed with a slightly different filename
+# So we mirror it ourselves
+SRC_URI="mirror://gentoo/${NUSMV_A}
+		http://nusmv.irst.itc.it/distrib/${NUSMV_A}
+		minisat? ( mirror://gentoo/${MINISAT_A} )"
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="~x86 ~amd64"
+IUSE="minisat examples"
+RDEPEND="dev-libs/expat"
+DEPEND="${RDEPEND}
+		virtual/latex-base
+		|| ( ( dev-texlive/texlive-latexextra )
+			app-text/ptex )
+		app-text/ghostscript-gpl
+		www-client/lynx
+		dev-lang/perl"
+# the above 4 are for docs, which aren't optional yet patches welcome to
+# avoid building the docs but I suspect anybody using this package will
+# actually need them
+S="${NUSMV_S}"
+
+src_unpack() {
+	unpack ${NUSMV_A}
+	if use minisat; then
+		cd "${WORKDIR}"/${NUSMV_P}/MiniSat
+		unpack ${MINISAT_A}
+		epatch ${MINISAT_P}_nusmv.patch
+		epatch "${FILESDIR}"/${MINISAT_P}-optimizedlib.patch
+		epatch "${FILESDIR}"/${MINISAT_P}_gcc41.patch
+	fi
+	for i in ${NUSMV_S}/doc/{user-man,tutorial}/Makefile.in ; do
+		sed -i.orig \
+			'/install_sh_DATA/s!$(datadir)!$(DESTDIR)$(datadir)!g' \
+			${i} || die "sed $i failed"
+	done
+}
+
+src_compile() {
+	rm -f ${NUSMV_S}/${MINISAT_P}
+	if use minisat; then
+		cd ${MINISAT_S}
+		# do NOT merge these targets
+		emake COPTIMIZE="${CFLAGS}" r || die "Failed to build minisat bin"
+		emake COPTIMIZE="${CFLAGS}" lr || die "Failed to build minisat lib"
+		ln -sf ${MINISAT_S} "${WORKDIR}"/${NUSMV_P}/${MINISAT_P}
+	fi
+
+	cd ${CUDD_S}
+	emake clean || die "Failed to clean cudd out."
+	emake \
+		CPP="$(tc-getCPP)" CC="$(tc-getCC)" \
+		RANLIB="$(tc-getRANLIB)" ICFLAGS="${CFLAGS}" \
+		|| die "Failed to build cudd."
+
+	local myconf="$(use_enable minisat) --enable-pslparser"
+	if use minisat; then
+		myconf="${myconf}
+			--with-minisat-incdir=../${MINISAT_P}
+			--with-minisat-libdir=../${MINISAT_P}"
+	fi
+
+	cd ${NUSMV_S}
+	econf ${myconf} || die "econf failed"
+	emake || die "emake failed"
+
+	VARTEXFONTS="${T}"/fonts emake docs
+}
+
+src_install() {
+	into /usr
+	if use minisat; then
+		newbin ${MINISAT_S}/minisat_release minisat
+	fi
+
+	dodir /usr/share/nusmv/doc
+	cd ${NUSMV_S}
+	emake DESTDIR="${D}" install || die "emake install failed"
+	# duplicate items
+	rm -f "${D}"/usr/share/nusmv/{LGPL-2.1,README*,NEWS}
+	# real docs
+	dodoc README* NEWS AUTHORS
+	dodoc doc/tutorial/tutorial.pdf
+	dodoc doc/user-man/nusmv.pdf
+
+	# move package-installed docs
+	mv "${D}"/usr/share/nusmv/doc/* "${D}"/usr/share/doc/${PF}/
+	rmdir "${D}"/usr/share/nusmv/doc
+
+	# clean out examples if not needed
+	if use !examples ; then
+		rm -rf "${D}"/usr/share/nusmv/examples || die "Failed to remove examples"
+	fi
+}
+
+src_test() {
+	cd ${NUSMV_S}
+	emake check || die "emake check failed"
+}