Update of /cvsroot/fink/dists/10.4/unstable/main/finkinfo/sci
In directory sc8-pr-cvs17.sourceforge.net:/tmp/cvs-serv32126
Added Files:
eprover.info eprover.patch
Log Message:
New from tracker
http://sourceforge.net/tracker/index.php?func=detail&aid=1853743&group_id=17203&atid=414256
--- NEW FILE: eprover.patch ---
diff -Naur --exclude='*~' E/Makefile E.fink/Makefile
--- E/Makefile 2007-09-08 20:42:41.000000000 -0700
+++ E.fink/Makefile 2007-12-18 23:16:39.000000000 -0800
@@ -159,10 +159,10 @@
@awk '{count++; if(count >= 4){print}}' PROVER/eproof >> tmpfile
@mv tmpfile PROVER/eproof
@chmod ugo+x PROVER/eproof
- bash -c 'cp PROVER/eprover $(EXECPATH)'
- bash -c 'cp PROVER/epclextract $(EXECPATH)'
- bash -c 'cp PROVER/eproof $(EXECPATH)'
- bash -c 'cp PROVER/eground $(EXECPATH)'
+ cp PROVER/eprover $(DESTDIR)$(EXECPATH)
+ cp PROVER/epclextract $(DESTDIR)$(EXECPATH)
+ cp PROVER/eproof $(DESTDIR)$(EXECPATH)
+ cp PROVER/eground $(DESTDIR)$(EXECPATH)
# bash -c 'install -c $(EXECPATH) PROVER/eprover'
# bash -c 'install -c $(EXECPATH) PROVER/e2pcl'
# bash -c 'install -c $(EXECPATH) PROVER/eproof'
diff -Naur --exclude='*~' E/Makefile.vars E.fink/Makefile.vars
--- E/Makefile.vars 2007-12-12 16:01:18.000000000 -0800
+++ E.fink/Makefile.vars 2007-12-18 21:04:19.000000000 -0800
@@ -19,7 +19,7 @@
# EXECPATH is where make install-exec will move the more important
# executables. Edit it to point to wherever you want them to live.
-EXECPATH = ~/bin
+EXECPATH = @PREFIX@/bin
# Makefile special variables
#
--- NEW FILE: eprover.info ---
Package: eprover
Description: Powerful equational logic theorem prover
Homepage: http://www.eprover.org
Version: 0.999-004
Revision: 1
BuildDepends: tetex-base | system-tetex
Maintainer: Jesse Alama <[EMAIL PROTECTED]>
DescDetail: <<
E is a a purely equational theorem prover for full first-order
logic. That means it is a program that you can stuff a mathematical
specification (in first-order format) and a hypothesis into, and which
will then run forever, using up all of your machines resources. Very
occasionally it will find a proof for the hypothesis and tell you
so...
E's inference core is based on a modified version of the superposition
calculus for equational clausal logic as described in [BG94]. For the
case of pure unit equality (where both goals and axioms are simple
equations, not disjunctions of literals or conditional rules), the
calculus degenerates to unfailing completion [BDP89] extended to deal
with arbitrarily quantified goals as implemented in DISCOUNT
[DKS97]. Current versions offers a variety of literal selection
functions and can e.g. emulate the unit-paramodulation strategy
described in [Der91] for Horn clauses.
E can now also handle full first-order logic. It uses a standard
clausification algorithm to translate first order formula to clausal
logic. Both clausification and reasoning on the clausal form can be
documented in checkable proof objects.
The prover was intended to become part of a METOP-based version of
E-SETHEO [Mos96]. E-SETHEO now has evolved into a multi-paradigm
strategy parallel proof system, but E is still a cornerstone of the
system.
There is a short system description about E 0.999 on the CASC-21
website.
<<
Source: http://www4.informatik.tu-muenchen.de/~schulz/WORK/E_DOWNLOAD/V_%v/E.tgz
Source-MD5: 277eac855b73a529068271c25a50b386
PatchScript: sed 's|@PREFIX@|%p|g' < %a/%n.patch | patch -p1
DocFiles: COPYING README DOC/clib.ps DOC/eprover.ps
License: GPL
CompileScript: <<
make install
make documentation
cd DOC;
<<
InstallScript: <<
mkdir -p %i/bin
make install-exec DESTDIR=%d
<<
-------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/marketplace
_______________________________________________
Fink-commits mailing list
[email protected]
http://news.gmane.org/gmane.os.apple.fink.cvs
