[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