From 7f7edfc97b586a4db204030d6d36fbc1e484dead Mon Sep 17 00:00:00 2001
From: David A. Wheeler <dwheeler@fedoraproject.org>
Date: Aug 27 2008 00:05:50 +0000
Subject: - Initial release.


---

diff --git a/.cvsignore b/.cvsignore
index e69de29..a4ae0f7 100644
--- a/.cvsignore
+++ b/.cvsignore
@@ -0,0 +1 @@
+E.tgz
diff --git a/E.spec b/E.spec
new file mode 100644
index 0000000..3d0d768
--- /dev/null
+++ b/E.spec
@@ -0,0 +1,99 @@
+Name:		E
+Version:	0.999.006
+Release:	2%{?dist}
+Summary:	Equational Theorem Prover
+Group:		Applications/Engineering
+License:	GPLv2
+URL:		http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
+Source0:	http://www4.informatik.tu-muenchen.de/~schulz/WORK/E_DOWNLOAD/V_0.999-006/E.tgz
+BuildRoot:	%{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
+# BuildRequires refers to files, not packages, because the package name differs
+# between releases. This is okay by Fedora's Packaging/Guidelines, which only
+# say "Whenever possible you should avoid file dependencies outside of
+# /etc, /bin, /sbin, /usr/bin, or /usr/sbin" - and these are in /usr/bin.
+BuildRequires:	/usr/bin/latex
+BuildRequires:	/usr/bin/dvips
+BuildRequires:	/usr/bin/pdflatex
+BuildRequires:	/usr/bin/bibtex
+# You can verify the CASC results here: http://www.cs.miami.edu/~tptp/CASC/J4/
+%description
+E is 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.  Both clausification and reasoning on
+the clausal form can be documented in checkable proof objects. 
+
+E was the best-performing open source software prover in the 2008
+CADE ATP System Competition (CASC) in the FOF, CNF, and UEQ divisions.
+
+%prep
+%setup -q -n E
+
+
+%build
+sed -i -e 's/^EXECPATH = .*/EXECPATH = \/usr\/bin/' Makefile.vars
+sed -i -e 's/^CFLAGS.*=.*-O6/CFLAGS = %{optflags} /' Makefile.vars
+# smp_mflags causes unwelcome races
+make tools
+make rebuild
+make documentation
+
+# Redo part of install-exec
+cd PROVER
+ echo "#!"`which bash`" -f" > tmpfile
+ echo "" >> tmpfile
+ echo "EXECPATH=/usr/bin" >> tmpfile
+ tail --lines=+4 eproof >> tmpfile
+ mv tmpfile eproof
+ chmod ugo+x eproof
+cd ..
+
+
+%install
+rm -rf $RPM_BUILD_ROOT
+mkdir -p $RPM_BUILD_ROOT/usr/bin
+cd PROVER
+for file in eproof eprover epclextract eground
+do
+ chmod 0755 "$file"
+ cp -p "$file" $RPM_BUILD_ROOT/usr/bin
+done
+
+%check
+./PROVER/eprover -s --tptp-in EXAMPLE_PROBLEMS/TPTP/SYN310-1+rm_eq_rstfp.tptp | tail -1 > test-results
+echo "# SZS status Unsatisfiable" > test-expected-results
+diff test-results test-expected-results
+
+
+%clean
+rm -rf $RPM_BUILD_ROOT
+
+
+%files
+%defattr(-,root,root,-)
+/usr/bin/*
+%doc README
+%doc COPYING
+%doc DOC/NEWS
+%doc DOC/grammar.txt
+%doc DOC/TPTP_SUBMISSION
+%doc DOC/E-0.999.html
+%doc DOC/sample_proofs.html
+%doc DOC/sample_proofs_tstp.html
+%doc DOC/TSTP_Syntax.txt
+%doc DOC/clib.ps
+%doc DOC/eprover.pdf
+
+
+%changelog
+* Tue Aug 16 2008 David A. Wheeler <dwheeler at, dwheeler.com> 0.999.006-2
+- Change executable permissions from 0775 to 0755 
+- Use compilation switches (e.g., -O2 instead of pointless -O6, and use -g)
+
+* Tue Aug 16 2008 David A. Wheeler <dwheeler at, dwheeler.com> 0.999.006-1
+- Initial package
+
diff --git a/import.log b/import.log
new file mode 100644
index 0000000..43436bc
--- /dev/null
+++ b/import.log
@@ -0,0 +1 @@
+E-0_999_006-2_fc9:HEAD:E-0.999.006-2.fc9.src.rpm:1219795475
diff --git a/sources b/sources
index e69de29..ed59db7 100644
--- a/sources
+++ b/sources
@@ -0,0 +1 @@
+5a2168d44e8b3f23f84ccc5ef66aadee  E.tgz