7 files changed, 112 insertions, 0 deletions
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 <ribosome@gentoo.org> +metadata.xml,
+  +otter-3.2.ebuild, +otter-3.3.ebuild:
+  Moved from app-sci/otter to sci-mathematics/otter.
+
+  01 Dec 2004; <burgundy@gentoo.org> otter-3.3.ebuild:
+  Keyworded ~ppc-macos.
+
+  01 Jul 2004; Jeremy Huddleston <eradicator@gentoo.org> otter-3.2.ebuild,
+  otter-3.3.ebuild:
+  virtual/glibc -> virtual/libc
+
+*otter-3.3 (31 Dec 2003)
+
+  31 Dec 2003; George Shapovalov <george@gentoo.org> 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 <george@gentoo.org> 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 <s0199782@sms.ed.ac.uk>
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 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+<herd>sci</herd>
+</pkgmetadata>
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
+}
+