From 5c4f473a03aa9f72ca820af61ac957d7cd575be2 Mon Sep 17 00:00:00 2001 From: Olivier Fisette Date: Tue, 28 Dec 2004 14:56:31 +0000 Subject: [PATCH] Moved from app-sci/otter to sci-mathematics/otter. --- sci-mathematics/otter/ChangeLog | 37 ++++++++++++++++++++ sci-mathematics/otter/Manifest | 6 ++++ sci-mathematics/otter/files/digest-otter-3.2 | 1 + sci-mathematics/otter/files/digest-otter-3.3 | 1 + sci-mathematics/otter/metadata.xml | 5 +++ sci-mathematics/otter/otter-3.2.ebuild | 31 ++++++++++++++++ sci-mathematics/otter/otter-3.3.ebuild | 31 ++++++++++++++++ 7 files changed, 112 insertions(+) create mode 100644 sci-mathematics/otter/ChangeLog create mode 100644 sci-mathematics/otter/Manifest create mode 100644 sci-mathematics/otter/files/digest-otter-3.2 create mode 100644 sci-mathematics/otter/files/digest-otter-3.3 create mode 100644 sci-mathematics/otter/metadata.xml create mode 100644 sci-mathematics/otter/otter-3.2.ebuild create mode 100644 sci-mathematics/otter/otter-3.3.ebuild diff --git a/sci-mathematics/otter/ChangeLog b/sci-mathematics/otter/ChangeLog new file mode 100644 index 000000000000..7304eeafccdf --- /dev/null +++ b/sci-mathematics/otter/ChangeLog @@ -0,0 +1,37 @@ +# ChangeLog for app-sci/otter +# Copyright 2002-2004 Gentoo Foundation; Distributed under the GPL v2 +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/otter/ChangeLog,v 1.1 2004/12/28 14:56:31 ribosome Exp $ + +*otter-3.3 (28 Dec 2004) + + 28 Dec 2004; Olivier Fisette +metadata.xml, + +otter-3.2.ebuild, +otter-3.3.ebuild: + Moved from app-sci/otter to sci-mathematics/otter. + + 01 Dec 2004; otter-3.3.ebuild: + Keyworded ~ppc-macos. + + 01 Jul 2004; Jeremy Huddleston otter-3.2.ebuild, + otter-3.3.ebuild: + virtual/glibc -> virtual/libc + +*otter-3.3 (31 Dec 2003) + + 31 Dec 2003; George Shapovalov otter-3.2.ebuild : + new version. Build procedure has slightly changed, adjusted ebuild to follow + +*otter-3.2 (16 May 2003) + + 16 May 2003; George Shapovalov Manifest, otter-3.2.ebuild, files/{digest-otter-3.2} : + initial release (#19036) + + Otter is designed to prove theorems + stated in first-order logic with equality. Otter's inference rules are based on + resolution and paramodulation, and it includes facilities for term rewriting, + term orderings, Knuth-Bendix completion, weighting, and strategies for directing + and restricting searches for proofs. Otter can also be used as a symbolic + calculator and has an embedded equational programming system. Otter is a + fourth-generation Argonne National Laboratory deduction system whose ancestors + (dating from the early 1960s) include the TP series, NIUTP, AURA, and ITP. + + ebuild submitted by Meghan Claire Pike diff --git a/sci-mathematics/otter/Manifest b/sci-mathematics/otter/Manifest new file mode 100644 index 000000000000..5d227759501b --- /dev/null +++ b/sci-mathematics/otter/Manifest @@ -0,0 +1,6 @@ +MD5 3e97c23a3d5eaa47b946daf59770aebd ChangeLog 1409 +MD5 8c623e53daafa025137077c6b65815bd metadata.xml 156 +MD5 9987d1075d2f3f7f21b11830147fa29d otter-3.2.ebuild 686 +MD5 27c539dc5343b04d38b85d6e2fa6b664 otter-3.3.ebuild 709 +MD5 b299411e0aa76723d9617046d8d7ea5e files/digest-otter-3.2 62 +MD5 aa559b24f0a62ba3189129735c89b785 files/digest-otter-3.3 62 diff --git a/sci-mathematics/otter/files/digest-otter-3.2 b/sci-mathematics/otter/files/digest-otter-3.2 new file mode 100644 index 000000000000..7bbfae3b5482 --- /dev/null +++ b/sci-mathematics/otter/files/digest-otter-3.2 @@ -0,0 +1 @@ +MD5 8e318fa7b4f7115bc3b2b1d29df2ef32 otter-3.2.tar.gz 1540512 diff --git a/sci-mathematics/otter/files/digest-otter-3.3 b/sci-mathematics/otter/files/digest-otter-3.3 new file mode 100644 index 000000000000..6d9defe1aa7b --- /dev/null +++ b/sci-mathematics/otter/files/digest-otter-3.3 @@ -0,0 +1 @@ +MD5 516b659ffe23ff64ea8af45724b83196 otter-3.3.tar.gz 2809092 diff --git a/sci-mathematics/otter/metadata.xml b/sci-mathematics/otter/metadata.xml new file mode 100644 index 000000000000..b229aec85b8f --- /dev/null +++ b/sci-mathematics/otter/metadata.xml @@ -0,0 +1,5 @@ + + + +sci + diff --git a/sci-mathematics/otter/otter-3.2.ebuild b/sci-mathematics/otter/otter-3.2.ebuild new file mode 100644 index 000000000000..8df49ba2953f --- /dev/null +++ b/sci-mathematics/otter/otter-3.2.ebuild @@ -0,0 +1,31 @@ +# Copyright 1999-2004 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/otter/otter-3.2.ebuild,v 1.1 2004/12/28 14:56:31 ribosome Exp $ + +DESCRIPTION="An Automated Deduction System." +SRC_URI="http://www-unix.mcs.anl.gov/AR/${PN}/${P}.tar.gz" +HOMEPAGE="http://www-unix.mcs.anl.gov/AR/otter/" + +KEYWORDS="x86" +LICENSE="otter" +SLOT="0" +IUSE="" +DEPEND="virtual/libc" +S=${WORKDIR}/${P}/source +WORK=${WORKDIR}/${P} + + +src_compile() { + cd ${S} + emake || die + cd ${S}/mace + emake || die +} + +src_install() { + cd ${S} + dobin otter mace/mace formed/formed + cd ${WORK} + dodoc README Legal Copying Changelog documents/* +} + diff --git a/sci-mathematics/otter/otter-3.3.ebuild b/sci-mathematics/otter/otter-3.3.ebuild new file mode 100644 index 000000000000..6693bdbab38c --- /dev/null +++ b/sci-mathematics/otter/otter-3.3.ebuild @@ -0,0 +1,31 @@ +# Copyright 1999-2004 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/otter/otter-3.3.ebuild,v 1.1 2004/12/28 14:56:31 ribosome Exp $ + +DESCRIPTION="An Automated Deduction System." +SRC_URI="http://www-unix.mcs.anl.gov/AR/${PN}/${P}.tar.gz" +HOMEPAGE="http://www-unix.mcs.anl.gov/AR/otter/" + +KEYWORDS="~x86 ~ppc-macos" +LICENSE="otter" +SLOT="0" +IUSE="" +DEPEND="virtual/libc" + + + +src_compile() { + cd source + make || die + cd ${S}/mace2 + make || die +} + +src_install() { + dobin bin/* source/formed/formed + dodoc README* Legal Changelog Contents documents/*.{tex,ps} + insinto /usr/share/doc/${PF} + doins documents/*.pdf + dohtml index.html +} + -- 2.26.2