[E] New upstream release. Now dual-licensed: GPLv2+ or LGPLv2+. Drop unnecessary spec file elements (Bui
Jerry James
jjames at fedoraproject.org
Wed Jun 22 04:12:26 UTC 2011
commit e22ce8ea2474356668eab2858d1b86bd2a30a91d
Author: Jerry James <loganjerry at gmail.com>
Date: Tue Jun 21 22:11:12 2011 -0600
New upstream release.
Now dual-licensed: GPLv2+ or LGPLv2+.
Drop unnecessary spec file elements (BuildRoot, etc.).
Use virtual provides for the BRs instead of files.
Install the man pages.
E.spec | 115 ++++++++++++++++++++++++++++++++-------------------------------
sources | 2 +-
2 files changed, 59 insertions(+), 58 deletions(-)
---
diff --git a/E.spec b/E.spec
index 5f51056..377e1ff 100644
--- a/E.spec
+++ b/E.spec
@@ -1,71 +1,66 @@
Name: E
-Version: 1.0.002
-Release: 6%{?dist}
+Version: 1.2.001
+Release: 1%{?dist}
Summary: Equational Theorem Prover
Group: Applications/Engineering
-License: GPLv2
+License: GPLv2+ or LGPLv2+
URL: http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
-Source0: http://www4.informatik.tu-muenchen.de/~schulz/WORK/E_DOWNLOAD/V_1.0-002/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
+Source0: http://www4.informatik.tu-muenchen.de/~schulz/WORK/E_DOWNLOAD/V_1.2-001/E.tgz
+
# Building actually checks for specific versions of python; building may
# need to be updated for new versions of python 2:
BuildRequires: python
+BuildRequires: tex(latex)
# 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.
+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.
+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.
+E was the best-performing open source software prover in the 2008 CADE
+ATP System Competition (CASC) in the FOF, CNF, and UEQ divisions. In
+the 2011 competition, it won second place in the FOF division, and
+placed highly in CNF and UEQ.
%prep
%setup -q -n E
+# Set up Fedora CFLAGS and paths
+sed -e "s|^EXECPATH = .*|EXECPATH = %{_bindir}|" \
+ -e "s|^MANPATH = .*|MANPATH = %{_mandir}|" \
+ -e "s|^CFLAGS.*|CFLAGS = $RPM_OPT_FLAGS -std=gnu99 \\\\|" \
+ -i Makefile.vars
+sed -i "s|^EXECPATH=.*|EXECPATH=%{_bindir}|" PROVER/eproof
-%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, so we will not use it
-make tools
-make rebuild
-make documentation
+# Fix the character encoding of one file
+iconv -f ISO8859-1 -t UTF-8 DOC/E-REMARKS > DOC/E-REMARKS.utf8
+touch -r DOC/E-REMARKS DOC/E-REMARKS.utf8
+mv -f DOC/E-REMARKS.utf8 DOC/E-REMARKS
-# 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 ..
+%build
+# smp_mflags causes unwelcome races, so we will not use it
+make remake
%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
+# Install the binaries
+mkdir -p $RPM_BUILD_ROOT%{_bindir}
+for file in eproof eprover epclextract eground e_ltb_runner; do
+ install -m 0755 -p PROVER/$file $RPM_BUILD_ROOT%{_bindir}
+done
+
+# Install the man pages
+mkdir -p $RPM_BUILD_ROOT%{_mandir}/man1
+for file in eproof eprover epclextract eground e_ltb_runner; do
+ install -m 0644 -p DOC/man/$file.1 $RPM_BUILD_ROOT%{_mandir}/man1
done
%check
@@ -74,27 +69,33 @@ 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/bug_reporting
+%doc DOC/clib.ps
+%doc DOC/CREDITS
+%doc DOC/E-1.2pre.html
+%doc DOC/eprover.pdf
+%doc DOC/E-REMARKS
+%doc DOC/E-REMARKS.english
%doc DOC/grammar.txt
-%doc DOC/TPTP_SUBMISSION
-%doc DOC/E-0.999.html
+%doc DOC/NEWS
%doc DOC/sample_proofs.html
%doc DOC/sample_proofs_tstp.html
%doc DOC/TSTP_Syntax.txt
-%doc DOC/clib.ps
-%doc DOC/eprover.pdf
-
+%doc DOC/WISHLIST
+%{_bindir}/*
+%{_mandir}/man1/*
%changelog
+* Tue Jun 21 2011 Jerry James <loganjerry at gmail.com> - 1.2.001-1
+- New upstream release
+- Now dual-licensed: GPLv2+ or LGPLv2+
+- Drop unnecessary spec file elements (BuildRoot, etc.)
+- Use virtual provides for the BRs instead of files
+- Install the man pages
+
* Mon Feb 07 2011 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 1.0.002-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
diff --git a/sources b/sources
index c76f4fd..23a7b80 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-886c765854120d30dcd748404a7ebf9c E.tgz
+acee33e200af096b65c94df16b992c87 E.tgz
More information about the scm-commits
mailing list