| 1 |
Name: E
|
| 2 |
Version: 1.0.002
|
| 3 |
Release: 5%{?dist}
|
| 4 |
Summary: Equational Theorem Prover
|
| 5 |
Group: Applications/Engineering
|
| 6 |
License: GPLv2
|
| 7 |
URL: http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
|
| 8 |
Source0: http://www4.informatik.tu-muenchen.de/~schulz/WORK/E_DOWNLOAD/V_1.0-002/E.tgz
|
| 9 |
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
|
| 10 |
|
| 11 |
# BuildRequires refers to files, not packages, because the package name differs
|
| 12 |
# between releases. This is okay by Fedora's Packaging/Guidelines, which only
|
| 13 |
# say "Whenever possible you should avoid file dependencies outside of
|
| 14 |
# /etc, /bin, /sbin, /usr/bin, or /usr/sbin" - and these are in /usr/bin.
|
| 15 |
BuildRequires: /usr/bin/latex
|
| 16 |
BuildRequires: /usr/bin/dvips
|
| 17 |
BuildRequires: /usr/bin/pdflatex
|
| 18 |
BuildRequires: /usr/bin/bibtex
|
| 19 |
# Building actually checks for specific versions of python; building may
|
| 20 |
# need to be updated for new versions of python 2:
|
| 21 |
BuildRequires: python
|
| 22 |
# You can verify the CASC results here: http://www.cs.miami.edu/~tptp/CASC/J4/
|
| 23 |
|
| 24 |
%description
|
| 25 |
E is a purely equational theorem prover for full first-order logic.
|
| 26 |
That means it is a program that you can stuff a mathematical specification
|
| 27 |
(in first-order format) and a hypothesis into, and which will then run
|
| 28 |
forever, using up all of your machines' resources.
|
| 29 |
Very occasionally it will find a proof for the hypothesis and tell you so.
|
| 30 |
|
| 31 |
E's inference core is based on a modified version of the superposition
|
| 32 |
calculus for equational clausal logic. Both clausification and reasoning on
|
| 33 |
the clausal form can be documented in checkable proof objects.
|
| 34 |
|
| 35 |
E was the best-performing open source software prover in the 2008
|
| 36 |
CADE ATP System Competition (CASC) in the FOF, CNF, and UEQ divisions.
|
| 37 |
|
| 38 |
%prep
|
| 39 |
%setup -q -n E
|
| 40 |
|
| 41 |
|
| 42 |
%build
|
| 43 |
sed -i -e 's/^EXECPATH = .*/EXECPATH = \/usr\/bin/' Makefile.vars
|
| 44 |
sed -i -e 's/^CFLAGS.*=.*-O6/CFLAGS = %{optflags} /' Makefile.vars
|
| 45 |
# smp_mflags causes unwelcome races, so we will not use it
|
| 46 |
make tools
|
| 47 |
make rebuild
|
| 48 |
make documentation
|
| 49 |
|
| 50 |
# Redo part of install-exec
|
| 51 |
cd PROVER
|
| 52 |
echo "#!"`which bash`" -f" > tmpfile
|
| 53 |
echo "" >> tmpfile
|
| 54 |
echo "EXECPATH=/usr/bin" >> tmpfile
|
| 55 |
tail --lines=+4 eproof >> tmpfile
|
| 56 |
mv tmpfile eproof
|
| 57 |
chmod ugo+x eproof
|
| 58 |
cd ..
|
| 59 |
|
| 60 |
|
| 61 |
%install
|
| 62 |
rm -rf $RPM_BUILD_ROOT
|
| 63 |
mkdir -p $RPM_BUILD_ROOT/usr/bin
|
| 64 |
cd PROVER
|
| 65 |
for file in eproof eprover epclextract eground
|
| 66 |
do
|
| 67 |
chmod 0755 "$file"
|
| 68 |
cp -p "$file" $RPM_BUILD_ROOT/usr/bin
|
| 69 |
done
|
| 70 |
|
| 71 |
%check
|
| 72 |
./PROVER/eprover -s --tptp-in EXAMPLE_PROBLEMS/TPTP/SYN310-1+rm_eq_rstfp.tptp | tail -1 > test-results
|
| 73 |
echo "# SZS status Unsatisfiable" > test-expected-results
|
| 74 |
diff test-results test-expected-results
|
| 75 |
|
| 76 |
|
| 77 |
%clean
|
| 78 |
rm -rf $RPM_BUILD_ROOT
|
| 79 |
|
| 80 |
|
| 81 |
%files
|
| 82 |
%defattr(-,root,root,-)
|
| 83 |
/usr/bin/*
|
| 84 |
%doc README
|
| 85 |
%doc COPYING
|
| 86 |
%doc DOC/NEWS
|
| 87 |
%doc DOC/grammar.txt
|
| 88 |
%doc DOC/TPTP_SUBMISSION
|
| 89 |
%doc DOC/E-0.999.html
|
| 90 |
%doc DOC/sample_proofs.html
|
| 91 |
%doc DOC/sample_proofs_tstp.html
|
| 92 |
%doc DOC/TSTP_Syntax.txt
|
| 93 |
%doc DOC/clib.ps
|
| 94 |
%doc DOC/eprover.pdf
|
| 95 |
|
| 96 |
|
| 97 |
%changelog
|
| 98 |
* Fri Jul 24 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.0.002-5
|
| 99 |
- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
|
| 100 |
|
| 101 |
* Mon Feb 23 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.0.002-4
|
| 102 |
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
|
| 103 |
|
| 104 |
* Mon Dec 22 2008 David A. Wheeler <dwheeler at, dwheeler.com> 1.0.002-3
|
| 105 |
- Work around local tags
|
| 106 |
|
| 107 |
* Mon Dec 22 2008 David A. Wheeler <dwheeler at, dwheeler.com> 1.0.002-2
|
| 108 |
- Repaired for python2 variations (different releases have different versions
|
| 109 |
of python2)
|
| 110 |
|
| 111 |
* Mon Dec 22 2008 David A. Wheeler <dwheeler at, dwheeler.com> 1.0.002-1
|
| 112 |
- Added python2.5 as BuildRequires
|
| 113 |
- Update to E version 1.0 ("Temi"). This includes...
|
| 114 |
- Improved eproof script signal handling.
|
| 115 |
- Fixed a number of warnings with the latest gcc version.
|
| 116 |
- Updated proof objects to latest SZS ontology.
|
| 117 |
|
| 118 |
* Tue Aug 16 2008 David A. Wheeler <dwheeler at, dwheeler.com> 0.999.006-2
|
| 119 |
- Change executable permissions from 0775 to 0755
|
| 120 |
- Use compilation switches (e.g., -O2 instead of pointless -O6, and use -g)
|
| 121 |
|
| 122 |
* Tue Aug 16 2008 David A. Wheeler <dwheeler at, dwheeler.com> 0.999.006-1
|
| 123 |
- Initial package
|
| 124 |
|
Parent Directory
| 
Revision Log