diff options
| -rw-r--r-- | sci-mathematics/cvc3/ChangeLog | 10 | ||||
| -rw-r--r-- | sci-mathematics/cvc3/Manifest | 15 | ||||
| -rw-r--r-- | sci-mathematics/cvc3/cvc3-2.4.1.ebuild | 146 | ||||
| -rw-r--r-- | sci-mathematics/cvc3/files/50cvc3-gentoo.el | 5 | ||||
| -rw-r--r-- | sci-mathematics/cvc3/metadata.xml | 40 | ||||
| -rw-r--r-- | sci-mathematics/e/Manifest | 14 | ||||
| -rw-r--r-- | sci-mathematics/spass/Manifest | 14 |
7 files changed, 244 insertions, 0 deletions
diff --git a/sci-mathematics/cvc3/ChangeLog b/sci-mathematics/cvc3/ChangeLog new file mode 100644 index 000000000000..236286228415 --- /dev/null +++ b/sci-mathematics/cvc3/ChangeLog @@ -0,0 +1,10 @@ +# ChangeLog for sci-mathematics/cvc3 +# Copyright 1999-2012 Gentoo Foundation; Distributed under the GPL v2 +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/cvc3/ChangeLog,v 1.1 2012/05/30 00:51:22 gienah Exp $ + +*cvc3-2.4.1 (30 May 2012) + + 30 May 2012; Mark Wright <gienah@gentoo.org> +cvc3-2.4.1.ebuild, + +files/50cvc3-gentoo.el, +metadata.xml: + Add CVC3 automatic theorem prover, with optional Isabelle/HOL integration. + diff --git a/sci-mathematics/cvc3/Manifest b/sci-mathematics/cvc3/Manifest new file mode 100644 index 000000000000..8c26dbcf4a2f --- /dev/null +++ b/sci-mathematics/cvc3/Manifest @@ -0,0 +1,15 @@ +-----BEGIN PGP SIGNED MESSAGE----- +Hash: SHA256 + +AUX 50cvc3-gentoo.el 200 RMD160 6fe87a208c68caa0f5f7105d08883eac7f3469ef SHA1 3c73dbee5fb1d8e88932b6c96c5c8f3bffeb3829 SHA256 3c58ff066505561c73dacb492eca4fcedd37f63ffff3b2c12cba0a4cc4e4f939 +DIST cvc3-2.4.1.tar.gz 1196616 RMD160 c96274a961d147571811a390ee7009285eaedc00 SHA1 b694d65234fe1119d86f3c6f53318b09f0ad68fe SHA256 d55b1d6006cfbac3f6d4c086964558902c3ed0efa66ac499cfb2193f3ee4acf7 +EBUILD cvc3-2.4.1.ebuild 3500 RMD160 e995c816d18dd079334fac8e63e162840ca46e23 SHA1 791ddbfe26e080892c885a13f90545674832f3b9 SHA256 f463d9dd1ea595c16757e1070f93fbc3f4fde0c0833981752d8a408dd4cb5d2a +MISC ChangeLog 427 RMD160 499d7382591142fb40e8b3075d5b6372b4113abc SHA1 318fd8c4e4bae7de9ac6e251351e7f85ce00187e SHA256 ff847b99f49ea1fc2caa40ce8ca473b1ddec59090804416d1ee139e47f958abd +MISC metadata.xml 1658 RMD160 76458153871c406d965fd691d832722c93c764b8 SHA1 d45240d6d986aa63b7729dd18cdadb0e1ce59000 SHA256 acdd9f0c8953b28e39975a89b821ab7c386aefa06c93e3a991c104231d136751 +-----BEGIN PGP SIGNATURE----- +Version: GnuPG v2.0.17 (GNU/Linux) + +iF4EAREIAAYFAk/FbxUACgkQoBEVQmGOlx/92QD9EkgI5Csz7Q8cqDClaTBpcKqL +WfESief1ZyrDepH7k8sBAKJhcxxq2JVkuFW1EwdB60qVX9fenDutvB4cMIbbmwOD +=JyLA +-----END PGP SIGNATURE----- diff --git a/sci-mathematics/cvc3/cvc3-2.4.1.ebuild b/sci-mathematics/cvc3/cvc3-2.4.1.ebuild new file mode 100644 index 000000000000..8a53f5932de7 --- /dev/null +++ b/sci-mathematics/cvc3/cvc3-2.4.1.ebuild @@ -0,0 +1,146 @@ +# Copyright 1999-2012 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/cvc3/cvc3-2.4.1.ebuild,v 1.1 2012/05/30 00:51:22 gienah Exp $ + +EAPI="4" + +inherit elisp-common + +DESCRIPTION="CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems" +HOMEPAGE="http://www.cs.nyu.edu/acsys/cvc3/index.html" +SRC_URI="http://www.cs.nyu.edu/acsys/cvc3/releases/2.4.1/${P}.tar.gz" + +LICENSE="CVC3" +SLOT="0" +KEYWORDS="~x86 ~amd64" +IUSE="doc emacs isabelle static-libs zchaff" + +RDEPEND="" +DEPEND="${RDEPEND} + >=dev-libs/gmp-5[static-libs?] + doc? ( + app-doc/doxygen + media-gfx/graphviz + ) + emacs? ( + virtual/emacs + ) + isabelle? ( + >=sci-mathematics/isabelle-2011.1-r1 + )" + +SITEFILE=50${PN}-gentoo.el + +src_prepare() { + sed -e 's/prefix=@prefix@/prefix=${DESTDIR}@prefix/' \ + -e 's/libdir=@libdir@/libdir=${DESTDIR}@libdir/' \ + -e 's/mandir=@mandir@/mandir=${DESTDIR}@mandir@/' \ + -i "${S}/Makefile.local.in" \ + || die "Could not set DESTDIR in Makefile.local.in" +} + +src_configure() { + econf \ + $(use_enable static-libs static) \ + $(use_enable zchaff) + + if use test; then + sed -e 's@LD_LIBS = @LD_LIBS = -L'"${S}"'/lib -Wl,-R'"${S}"'/lib @' \ + -i "${S}/test/Makefile" \ + || die "Could not set library paths in test/Makefile" + fi +} + +src_compile() { + emake + + if use doc; then + pushd doc || die "Could not cd to doc" + emake + popd + fi + + if use emacs ; then + pushd "${S}/emacs" || die "Could change directory to emacs" + elisp-compile *.el || die "emacs elisp compile failed" + popd + fi + + if use test; then + pushd test || die "Could not cd to test" + emake + popd + fi +} + +src_test() { + pushd test || die "Could not cd to test" + ./bin/test || die "tests failed" + popd +} + +src_install() { + emake DESTDIR="${D}" install + + if use doc; then + pushd "${S}"/doc/html || die "Could not cd to doc/html" + dohtml *.html + insinto /usr/share/doc/${PF}/html + doins *.css *.gif *.png + popd + fi + + if use emacs ; then + elisp-install ${PN} emacs/*.{el,elc} + cp "${FILESDIR}"/${SITEFILE} "${S}" + elisp-site-file-install ${SITEFILE} + fi + + if use isabelle; then + ISABELLE_HOME="$(isabelle getenv ISABELLE_HOME | cut -d'=' -f 2)" \ + || die "isabelle getenv ISABELLE_HOME failed" + if [[ -z "${ISABELLE_HOME}" ]]; then + die "ISABELLE_HOME empty" + fi + dodir "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc" + cat <<- EOF >> "${S}/settings" + CVC3_COMPONENT="\$COMPONENT" + CVC3_HOME="${ROOT}usr/bin" + CVC3_SOLVER="\$CVC3_HOME/cvc3" + CVC3_REMOTE_SOLVER="cvc3" + CVC3_INSTALLED="yes" + EOF + insinto "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc" + doins "${S}/settings" + fi +} + +pkg_postinst() { + use emacs && elisp-site-regen + if use isabelle; then + if [ -f "${ROOT}etc/isabelle/components" ]; then + if egrep "contrib/${PN}-[0-9.]*" "${ROOT}etc/isabelle/components"; then + sed -e "/contrib\/${PN}-[0-9.]*/d" \ + -i "${ROOT}etc/isabelle/components" + fi + cat <<- EOF >> "${ROOT}etc/isabelle/components" + contrib/${PN}-${PV} + EOF + fi + fi +} + +pkg_postrm() { + use emacs && elisp-site-regen + if use isabelle; then + if [ ! -f "${ROOT}usr/bin/cvc3" ]; then + if [ -f "${ROOT}etc/isabelle/components" ]; then + # Note: this sed should only match the version of this ebuild + # Which is what we want as we do not want to remove the line + # of a new E being installed during an upgrade. + sed -e "/contrib\/${PN}-${PV}/d" \ + -i "${ROOT}etc/isabelle/components" + fi + fi + fi +} diff --git a/sci-mathematics/cvc3/files/50cvc3-gentoo.el b/sci-mathematics/cvc3/files/50cvc3-gentoo.el new file mode 100644 index 000000000000..2c8b4011acbd --- /dev/null +++ b/sci-mathematics/cvc3/files/50cvc3-gentoo.el @@ -0,0 +1,5 @@ +;;; teyjus site-lisp configuration + +(add-to-list 'load-path "@SITELISP@") +(add-to-list 'auto-mode-alist '("\\.cvc\\'" . cvc-mode)) +(autoload 'cvc-mode "cvc-mode" "CVC specifications editing mode." t) diff --git a/sci-mathematics/cvc3/metadata.xml b/sci-mathematics/cvc3/metadata.xml new file mode 100644 index 000000000000..db25562598fb --- /dev/null +++ b/sci-mathematics/cvc3/metadata.xml @@ -0,0 +1,40 @@ +<?xml version="1.0" encoding="UTF-8"?> +<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> +<pkgmetadata> +<maintainer> + <email>gienah@gentoo.org></email> +</maintainer> +<herd>sci-mathematics</herd> +<longdescription lang='en'> +CVC3 is an automatic theorem prover for Satisfiability Modulo Theories +(SMT) problems. It can be used to prove the validity (or, dually, the +satisfiability) of first-order formulas in a large number of built-in +logical theories and their combination. + +CVC3 is the last offspring of a series of popular SMT provers, which +originated at Stanford University with the SVC system. In particular, +it builds on the code base of CVC Lite, its most recent +predecessor. Its high level design follows that of the Sammy prover. + +CVC3 works with a version of first-order logic with polymorphic types +and has a wide variety of features including: + + several built-in base theories: rational and integer linear + arithmetic, arrays, tuples, records, inductive data types, bit + vectors, and equality over uninterpreted function symbols; + support for quantifiers; + an interactive text-based interface; + a rich C and C++ API for embedding in other systems; + proof and model generation abilities; + predicate subtyping; + essentially no limit on its use for research or commercial + purposes (see license). +</longdescription> +<use> + <flag name='isabelle'>Add integration support for the Isabelle/HOL + theorem prover.</flag> + <flag name='zchaff'>Use the SAT solver zchaff whose copyright is + owned by Princeton University and is more restrictive (see license). + </flag> +</use> +</pkgmetadata> diff --git a/sci-mathematics/e/Manifest b/sci-mathematics/e/Manifest new file mode 100644 index 000000000000..97414a4e1964 --- /dev/null +++ b/sci-mathematics/e/Manifest @@ -0,0 +1,14 @@ +-----BEGIN PGP SIGNED MESSAGE----- +Hash: SHA256 + +DIST E-1.5.tgz 1689077 RMD160 49742d441d205dc76a3278d9544100a3c6732a2f SHA1 d7fcf5aacfa309b3e2a93f1d7d8fdbf6ccbc3c06 SHA256 37239f169a9af3bb64edd205abe5022a043a1f4ea9ec694b39a9e61b37f5e46f +EBUILD e-1.5.ebuild 3465 RMD160 0aef9ecb7f8b4838d14eafdab1204bb98b35e606 SHA1 4a8468aa61e2cd9fe5785c4f987fdccd390399d3 SHA256 c735f5ca5b78a7a1b679984e39876a2f21a718051d4d25a899f59339e88bf95a +MISC ChangeLog 384 RMD160 39976a96eaa81068870fb309609cfe16191761f4 SHA1 ba5659b7acaf5c9bbdf9bd995ebb63bb48dcbdb9 SHA256 23eb422f89b53adb4899ac4ef1708de6eaa9d3ee8fcfdf7221cc342f785a99fb +MISC metadata.xml 1323 RMD160 366373798425f0daedafeadadbe7cf62844f0506 SHA1 f08122178cfdc4f190c3b9474861d64ae6fbbfdf SHA256 ee934514d44fa85025ca82639eae1ae007ca9585d86a82bf5b3b413b31de1af0 +-----BEGIN PGP SIGNATURE----- +Version: GnuPG v2.0.17 (GNU/Linux) + +iF4EAREIAAYFAk/FcAUACgkQoBEVQmGOlx/oLwD/QLTxSnzNhC79bVmHZ0Gdmv43 +Km2P/GCXaBLEtpllXVEBAN+KLrUcmVpiTV6rr19a6APfX7eWifIYBjfvE2Mk/6e8 +=Eekz +-----END PGP SIGNATURE----- diff --git a/sci-mathematics/spass/Manifest b/sci-mathematics/spass/Manifest new file mode 100644 index 000000000000..668a182be26c --- /dev/null +++ b/sci-mathematics/spass/Manifest @@ -0,0 +1,14 @@ +-----BEGIN PGP SIGNED MESSAGE----- +Hash: SHA256 + +DIST spass37.tgz 1340925 RMD160 fb501cbe99331b4482b99c7f2df2f91566aa6a6a SHA1 68b1e570381b1bedafb5c682f4dee7ed3a6c6874 SHA256 13c67e5e09b814ba50f38a391fe653661ba714e7541ffd4951efef91274aaacc +EBUILD spass-3.7.ebuild 2065 RMD160 0c75ed6ffa056c79bdf2eebe44831d8e2c35ef2e SHA1 140ba5f042e0afcff3b15c05e51e93c94a3059e3 SHA256 71d76b4c3aa90bea327cec680dce05429ac0ea869019c7e7050552f4b79e7714 +MISC ChangeLog 416 RMD160 81da7194a5fc8623cc7652d6a974b2e3de96a5c8 SHA1 57dcf037ed47fdb50d68b6e04235e97d7cd2a713 SHA256 b6f27163fc07f9bb818793912487fe994b435e1edb0b5ebfc817ff8b5f6508d1 +MISC metadata.xml 457 RMD160 be80e2ad1155c9ca3939811523a2f4d7865db52a SHA1 4bc39390402f4ea729af6147557f548a37180b24 SHA256 5be29865933aafc64edf4febf36101a59efbcf12da6772b90e564f3c794ad554 +-----BEGIN PGP SIGNATURE----- +Version: GnuPG v2.0.17 (GNU/Linux) + +iF4EAREIAAYFAk/Fb50ACgkQoBEVQmGOlx/WkgD+PZhaMxmR4ktXs2pquezN2pxO +8sNOLfPM1WA2eMo+aX8BAJlFqjL0yueoomhkDlXdyz0yPTyNpA0WcQEhN3e/T8Mh +=jBgU +-----END PGP SIGNATURE----- |