summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRobin H. Johnson <robbat2@gentoo.org>2015-08-08 13:49:04 -0700
committerRobin H. Johnson <robbat2@gentoo.org>2015-08-08 17:38:18 -0700
commit56bd759df1d0c750a065b8c845e93d5dfa6b549d (patch)
tree3f91093cdb475e565ae857f1c5a7fd339e2d781e /sci-mathematics/nusmv
downloadgentoo-56bd759df1d0c750a065b8c845e93d5dfa6b549d.tar.gz
gentoo-56bd759df1d0c750a065b8c845e93d5dfa6b549d.tar.bz2
gentoo-56bd759df1d0c750a065b8c845e93d5dfa6b549d.zip
proj/gentoo: Initial commit
This commit represents a new era for Gentoo: Storing the gentoo-x86 tree in Git, as converted from CVS. This commit is the start of the NEW history. Any historical data is intended to be grafted onto this point. Creation process: 1. Take final CVS checkout snapshot 2. Remove ALL ChangeLog* files 3. Transform all Manifests to thin 4. Remove empty Manifests 5. Convert all stale $Header$/$Id$ CVS keywords to non-expanded Git $Id$ 5.1. Do not touch files with -kb/-ko keyword flags. Signed-off-by: Robin H. Johnson <robbat2@gentoo.org> X-Thanks: Alec Warner <antarus@gentoo.org> - did the GSoC 2006 migration tests X-Thanks: Robin H. Johnson <robbat2@gentoo.org> - infra guy, herding this project X-Thanks: Nguyen Thai Ngoc Duy <pclouds@gentoo.org> - Former Gentoo developer, wrote Git features for the migration X-Thanks: Brian Harring <ferringb@gentoo.org> - wrote much python to improve cvs2svn X-Thanks: Rich Freeman <rich0@gentoo.org> - validation scripts X-Thanks: Patrick Lauer <patrick@gentoo.org> - Gentoo dev, running new 2014 work in migration X-Thanks: Michał Górny <mgorny@gentoo.org> - scripts, QA, nagging X-Thanks: All of other Gentoo developers - many ideas and lots of paint on the bikeshed
Diffstat (limited to 'sci-mathematics/nusmv')
-rw-r--r--sci-mathematics/nusmv/Manifest6
-rw-r--r--sci-mathematics/nusmv/files/MiniSat_v1.14-optimizedlib.patch44
-rw-r--r--sci-mathematics/nusmv/files/MiniSat_v1.14_gcc41.patch92
-rw-r--r--sci-mathematics/nusmv/files/cudd-no-pentium4.patch11
-rw-r--r--sci-mathematics/nusmv/metadata.xml11
-rw-r--r--sci-mathematics/nusmv/nusmv-2.3.1.ebuild121
-rw-r--r--sci-mathematics/nusmv/nusmv-2.5.0.ebuild133
-rw-r--r--sci-mathematics/nusmv/nusmv-2.5.2.ebuild132
-rw-r--r--sci-mathematics/nusmv/nusmv-2.5.3.ebuild132
-rw-r--r--sci-mathematics/nusmv/nusmv-2.5.4.ebuild135
10 files changed, 817 insertions, 0 deletions
diff --git a/sci-mathematics/nusmv/Manifest b/sci-mathematics/nusmv/Manifest
new file mode 100644
index 00000000000..eeeef6335c5
--- /dev/null
+++ b/sci-mathematics/nusmv/Manifest
@@ -0,0 +1,6 @@
+DIST MiniSat_v1.14_src.zip 29428 SHA256 8e5e0ee84a770dcb3abd6fc65ed4aef938f9ffabca5ddc8a739029f7fb58a8f5 SHA512 451839f3b0508ccfc78a65bbdf3d6820d335aea43b32aa2e39168ff515f3eb6f74ab1297186f1a89dc69e4d8663a1479043fd10135faf2dbaf33269ff7b831e1 WHIRLPOOL dea39fd30ad7c4195c5fe07356890c6525744d59644aff89ce865269daa4ffbebbbba94fe929d0bf6df441e169e2fd974b5373a443d5c3fb410ec8d7dffd9cb2
+DIST NuSMV-2.3.1.tar.gz 2590944 SHA256 b8ba0f29afafdfdef8c30f722eead3ef6cbb17e4bfe5563240a01d8a99dbbf68 SHA512 24d258197ecfd314378f132c28722c6f91ee0ee10f5d67e51e924a682c03646b8700e28899eb8ab3ee67b231c26c2094c075b000d391adddfb82bb93a8dfc12b WHIRLPOOL c015aeeabff6fe0770a1d216ab783db0ea4d1915e09e2fa9ac2f470ffbcc6a89881f0e917c544598f7f6484a50b1216ca0e631084887c56bfc2efe29b8f82dbd
+DIST NuSMV-2.5.0.tar.gz 3792968 SHA256 59310f5f23f72cb1ad16419e40f245db7c5aa41c0f59ba5c75732bb6c4b56ff1
+DIST NuSMV-2.5.2.tar.gz 3631420 SHA256 bc41c53c266d41d7bcb92851fbdb07d894c246d1189bfe420301c7b4fca46de0
+DIST NuSMV-2.5.3.tar.gz 3951637 SHA256 d5d6b2873dfa6f82ff9bef1a7eefa36dc5070557aa2b0e0d53cc8c54b2fe437d SHA512 8233a621d3cfad17d0b8f77a33460089b5c0a9fa694e6d91cbd6eb334213cd8d9e37fce8755e9ebc066279f25e86dfa7ded0197f679e42b8f2e7c048cc93356a WHIRLPOOL ea8075f405324179a822b9abd78f2c5d2a0c62ac31d2682f2145db7b033e2cf30f3a466689d75814cc3bfc551471425097d17515b19742f298899a432daec249
+DIST NuSMV-2.5.4.tar.gz 3968258 SHA256 3c250624cba801b1f62f50733f9507b0f3b3ca557ce1cd65956178eb273f1bdf SHA512 fc3cc641bbdbfc9464947c9991c8d363adeed9ed34af215c092a14b32d5ce536cb2dbc4eee1645d5aa85caa85e6e95b695620fa247f3a22652cdc4cd252c4c79 WHIRLPOOL 5822d1e7d853cf78cbdee07b0dafa1216fd226ecad803533310351573c7e9a864e6bba699a16c1b357da458311bf65b7362b6207b63e0c8008123e63950121e1
diff --git a/sci-mathematics/nusmv/files/MiniSat_v1.14-optimizedlib.patch b/sci-mathematics/nusmv/files/MiniSat_v1.14-optimizedlib.patch
new file mode 100644
index 00000000000..a291339491b
--- /dev/null
+++ b/sci-mathematics/nusmv/files/MiniSat_v1.14-optimizedlib.patch
@@ -0,0 +1,44 @@
+diff -Nuar MiniSat_v1.14/Makefile MiniSat_v1.14.new/Makefile
+--- MiniSat_v1.14/Makefile 2006-04-02 01:33:46.000000000 -0800
++++ MiniSat_v1.14.new/Makefile 2006-04-02 01:31:39.000000000 -0800
+@@ -26,10 +26,11 @@
+ RANLIB = ranlib
+ AR = ar
+
+-.PHONY : ls s p d r build clean depend
++.PHONY : lr ls s p d r build clean depend
+
+ s: WAY=standard
+ ls: WAY=standard
++lr: WAY=release
+ p: WAY=profile
+ d: WAY=debug
+ r: WAY=release
+@@ -38,8 +39,7 @@
+ s: CFLAGS+=$(COPTIMIZE) -ggdb -D DEBUG
+ p: CFLAGS+=$(COPTIMIZE) -pg -ggdb -D DEBUG
+ d: CFLAGS+=-O0 -ggdb -D DEBUG
+-r: CFLAGS+=$(COPTIMIZE) -D NDEBUG
+-rs: CFLAGS+=$(COPTIMIZE) -D NDEBUG
++r rs ls lr: CFLAGS+=$(COPTIMIZE) -D NDEBUG
+
+ s: build $(EXEC)
+ p: build $(EXEC)_profile
+@@ -48,7 +48,7 @@
+ rs: build $(EXEC)_static
+
+ s: CFLAGS+=$(COPTIMIZE) -ggdb -D DEBUG
+-ls: lbuild $(LIB)_s
++ls lr: lbuild $(LIB)_s
+
+ build:
+ @echo Building $(EXEC) "("$(WAY)")"
+@@ -63,7 +63,7 @@
+ ## Build rule
+ %.o %.op %.od %.or: %.C
+ @echo Compiling: $<
+- @$(CXX) $(CFLAGS) -c -o $@ $<
++ $(CXX) $(CFLAGS) -c -o $@ $<
+
+ ## Linking rules (standard/profile/debug/release)
+ $(EXEC): $(COBJS)
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 00000000000..dd5856ae57e
--- /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/files/cudd-no-pentium4.patch b/sci-mathematics/nusmv/files/cudd-no-pentium4.patch
new file mode 100644
index 00000000000..844f7c00d63
--- /dev/null
+++ b/sci-mathematics/nusmv/files/cudd-no-pentium4.patch
@@ -0,0 +1,11 @@
+--- Makefile.orig 2010-07-12 02:54:26.000000000 +0200
++++ Makefile 2010-07-12 02:54:49.000000000 +0200
+@@ -69,7 +69,7 @@
+ # Gcc 2.8.1 or higher on i686.
+ #XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
+ # Gcc 3.2.2 or higher on i686.
+-XCFLAGS = -mcpu=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4
++XCFLAGS = -malign-double -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4
+ # Icc on i686.
+ #XCFLAGS = -ansi -align -ip -DHAVE_IEEE_754 -DBSD
+ # Gcc on ia64.
diff --git a/sci-mathematics/nusmv/metadata.xml b/sci-mathematics/nusmv/metadata.xml
new file mode 100644
index 00000000000..da589122a2f
--- /dev/null
+++ b/sci-mathematics/nusmv/metadata.xml
@@ -0,0 +1,11 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+ <herd>sci-mathematics</herd>
+ <maintainer>
+ <email>robbat2@gentoo.org</email>
+ </maintainer>
+ <use>
+ <flag name="minisat">Enable support for MiniSat</flag>
+ </use>
+</pkgmetadata>
diff --git a/sci-mathematics/nusmv/nusmv-2.3.1.ebuild b/sci-mathematics/nusmv/nusmv-2.3.1.ebuild
new file mode 100644
index 00000000000..49764e29819
--- /dev/null
+++ b/sci-mathematics/nusmv/nusmv-2.3.1.ebuild
@@ -0,0 +1,121 @@
+# Copyright 1999-2012 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+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.3.0.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/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
+ 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."
+
+ cd ${NUSMV_S}
+ econf `use_enable minisat` \
+ --enable-sa \
+ --enable-sa-cpp \
+ --enable-psl
+ 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"
+}
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 00000000000..58220e1e95b
--- /dev/null
+++ b/sci-mathematics/nusmv/nusmv-2.5.0.ebuild
@@ -0,0 +1,133 @@
+# Copyright 1999-2012 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+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/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
+
+ cd "${CUDD_S}"
+ epatch "${FILESDIR}"/${CUDD_PN}-no-pentium4.patch
+ if [[ "$(tc-arch)" = amd64 ]] ; then
+ mv Makefile_64bit Makefile || die
+ 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}
+ 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"
+}
diff --git a/sci-mathematics/nusmv/nusmv-2.5.2.ebuild b/sci-mathematics/nusmv/nusmv-2.5.2.ebuild
new file mode 100644
index 00000000000..38ce8b01c80
--- /dev/null
+++ b/sci-mathematics/nusmv/nusmv-2.5.2.ebuild
@@ -0,0 +1,132 @@
+# Copyright 1999-2012 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+inherit eutils flag-o-matic 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/"
+SRC_URI="http://nusmv.fbk.eu/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/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
+
+ cd "${CUDD_S}"
+ if [[ "$(tc-arch)" = amd64 ]] ; then
+ mv Makefile_64bit Makefile || die
+ fi
+ sed -i Makefile -e 's/-mcpu=[^\s]*//' || die
+
+ 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() {
+ if [[ "$(tc-arch)" = x86 ]] ; then
+ append-flags -DNUSMV_SIZEOF_VOID_P=4 -DNUSMV_SIZEOF_LONG=4 -DNUSMV_SIZEOF_INT=4
+ fi
+
+ 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}
+ 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"
+}
diff --git a/sci-mathematics/nusmv/nusmv-2.5.3.ebuild b/sci-mathematics/nusmv/nusmv-2.5.3.ebuild
new file mode 100644
index 00000000000..9fa6a28a892
--- /dev/null
+++ b/sci-mathematics/nusmv/nusmv-2.5.3.ebuild
@@ -0,0 +1,132 @@
+# Copyright 1999-2013 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+inherit eutils flag-o-matic 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/"
+SRC_URI="http://nusmv.fbk.eu/distrib/${NUSMV_A}
+ minisat? ( mirror://gentoo/${MINISAT_A} )"
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="minisat examples"
+RDEPEND="dev-libs/expat"
+DEPEND="${RDEPEND}
+ virtual/latex-base
+ dev-texlive/texlive-latexextra
+ 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
+
+ cd "${CUDD_S}"
+ if [[ "$(tc-arch)" = amd64 ]] ; then
+ mv Makefile_64bit Makefile || die
+ fi
+ sed -i Makefile -e 's/-mcpu=[^\s]*//' || die
+
+ 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() {
+ if [[ "$(tc-arch)" = x86 ]] ; then
+ append-flags -DNUSMV_SIZEOF_VOID_P=4 -DNUSMV_SIZEOF_LONG=4 -DNUSMV_SIZEOF_INT=4
+ fi
+
+ 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}
+ 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"
+}
diff --git a/sci-mathematics/nusmv/nusmv-2.5.4.ebuild b/sci-mathematics/nusmv/nusmv-2.5.4.ebuild
new file mode 100644
index 00000000000..1f08cca70b7
--- /dev/null
+++ b/sci-mathematics/nusmv/nusmv-2.5.4.ebuild
@@ -0,0 +1,135 @@
+# Copyright 1999-2013 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+inherit eutils flag-o-matic 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/"
+SRC_URI="http://nusmv.fbk.eu/distrib/${NUSMV_A}
+ minisat? ( mirror://gentoo/${MINISAT_A} )"
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="minisat examples"
+RDEPEND="dev-libs/expat"
+DEPEND="${RDEPEND}
+ virtual/latex-base
+ dev-texlive/texlive-latexextra
+ 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
+
+ cd "${CUDD_S}"
+ if [[ "$(tc-arch)" = amd64 ]] ; then
+ mv Makefile_64bit Makefile || die
+ fi
+ sed -i Makefile -e 's/-mcpu=[^\s]*//' || die
+
+ 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() {
+ if [[ "$(tc-arch)" = x86 ]] ; then
+ append-flags -DNUSMV_SIZEOF_VOID_P=4 -DNUSMV_SIZEOF_LONG=4 -DNUSMV_SIZEOF_INT=4
+ fi
+ # With LTO, it tried to link for 6 hours on an i7 system before failing.
+ filter-flags -flto -Wl,-flto
+
+ 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}
+ einfo "Don't be alarmed if compileWriteUdg.o takes a very long time to compile, ~90 minutes on an i7"
+ 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"
+}