diff options
| author |   George Shapovalov <george@gentoo.org> | 2003-05-16 09:54:33 +0000 |
|---|---|---|
| committer | George Shapovalov <george@gentoo.org> | 2003-05-16 09:54:33 +0000 |
| commit | 1b837e2e0332ab410b8aca520a9452f7fc78c51e (patch) | |
| tree | 39a7b0002232f9a0b57d626ab42bc8d85c5a3a9b /app-sci | |
| parent | new package: Automated Deduction System (diff) | |
| download | gentoo-2-1b837e2e0332ab410b8aca520a9452f7fc78c51e.tar.gz gentoo-2-1b837e2e0332ab410b8aca520a9452f7fc78c51e.tar.bz2 gentoo-2-1b837e2e0332ab410b8aca520a9452f7fc78c51e.zip | |
new package: Automated Deduction System
Diffstat (limited to 'app-sci')
| -rw-r--r-- | app-sci/otter/ChangeLog | 19 | ||||
| -rw-r--r-- | app-sci/otter/Manifest | 4 | ||||
| -rw-r--r-- | app-sci/otter/files/digest-otter-3.2 | 1 | ||||
| -rw-r--r-- | app-sci/otter/otter-3.2.ebuild | 31 |
4 files changed, 53 insertions, 2 deletions
diff --git a/app-sci/otter/ChangeLog b/app-sci/otter/ChangeLog new file mode 100644 index 000000000000..0f44d26a92e9 --- /dev/null +++ b/app-sci/otter/ChangeLog @@ -0,0 +1,19 @@ +# ChangeLog for app-sci/otter +# Copyright 2002 Gentoo Technologies, Inc.; Distributed under the GPL +# $Header: /var/cvsroot/gentoo-x86/app-sci/otter/ChangeLog,v 1.1 2003/05/16 09:54:21 george Exp $ + +*otter-3.2.ebuild (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/app-sci/otter/Manifest b/app-sci/otter/Manifest index 7d634177b00e..5905d16269e3 100644 --- a/app-sci/otter/Manifest +++ b/app-sci/otter/Manifest @@ -1,3 +1,3 @@ -MD5 5a879445965069a26d6f863ac86440d4 Legal 1133 -MD5 c2cb154d9190088f7095127a13c25f35 otter-3.2.ebuild 600 +MD5 c17f2faaafec0a69cc6b4a5394cb1c87 otter-3.2.ebuild 693 +MD5 756057cd6d74bff8b4d6d5d30e880f0e ChangeLog 1031 MD5 b299411e0aa76723d9617046d8d7ea5e files/digest-otter-3.2 62 diff --git a/app-sci/otter/files/digest-otter-3.2 b/app-sci/otter/files/digest-otter-3.2 new file mode 100644 index 000000000000..7bbfae3b5482 --- /dev/null +++ b/app-sci/otter/files/digest-otter-3.2 @@ -0,0 +1 @@ +MD5 8e318fa7b4f7115bc3b2b1d29df2ef32 otter-3.2.tar.gz 1540512 diff --git a/app-sci/otter/otter-3.2.ebuild b/app-sci/otter/otter-3.2.ebuild new file mode 100644 index 000000000000..f7ef39ef891d --- /dev/null +++ b/app-sci/otter/otter-3.2.ebuild @@ -0,0 +1,31 @@ +# Copyright 1999-2003 Gentoo Technologies, Inc. +# Distributed under the terms of the GNU General Public License v2 +# $Header: /var/cvsroot/gentoo-x86/app-sci/otter/otter-3.2.ebuild,v 1.1 2003/05/16 09:54:21 george 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/glibc" +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/* +} + |