From bc69c12f9d029d94a8720ba51d60cc145c637a8e Mon Sep 17 00:00:00 2001 From: Michał Górny Date: Sat, 14 Sep 2019 17:43:34 +0200 Subject: sci-mathematics/e: Remove last-rited pkg MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Michał Górny --- sci-mathematics/e/Manifest | 2 - sci-mathematics/e/e-1.8-r1.ebuild | 118 ----------------------- sci-mathematics/e/e-2.3.ebuild | 75 -------------- sci-mathematics/e/files/e-2.3-build-system.patch | 8 -- sci-mathematics/e/metadata.xml | 35 ------- 5 files changed, 238 deletions(-) delete mode 100644 sci-mathematics/e/Manifest delete mode 100644 sci-mathematics/e/e-1.8-r1.ebuild delete mode 100644 sci-mathematics/e/e-2.3.ebuild delete mode 100644 sci-mathematics/e/files/e-2.3-build-system.patch delete mode 100644 sci-mathematics/e/metadata.xml (limited to 'sci-mathematics') diff --git a/sci-mathematics/e/Manifest b/sci-mathematics/e/Manifest deleted file mode 100644 index 13f262a533cf..000000000000 --- a/sci-mathematics/e/Manifest +++ /dev/null @@ -1,2 +0,0 @@ -DIST E-1.8.tgz 1832975 BLAKE2B ebac17f157f591874107009d1ad45d03449c8d440f3ad6dabda308193775cd69d01f6ffb159ef8acbc73fbd41e5b38f2eb61a1c734d638d4a045e068cc63fc90 SHA512 1b4358c636e8ea564ca942e1221e78234a9f0f793991f637bd7ec4d92eb9aa4a408a14c707405271fc017a9d63884d70bdfb0ed1b878383a1a44cfa57a7bdd51 -DIST E-2.3.tgz 2176351 BLAKE2B cb234d5d6ed9d098b9f1b3def44de570c2014dd017e2e39de58bfe8ea47f539008e30213eab78c61e042d04529cfdbc647706ae71707e306cf51f5189c5dad30 SHA512 9e0f22a174f9f0fae401d8556d0b825c17d06e48e40d027003a89ff8cc637e3a14e14af70e6a65ecf2a11a52d59388c6c36b129a123511b958c152f58fd06a16 diff --git a/sci-mathematics/e/e-1.8-r1.ebuild b/sci-mathematics/e/e-1.8-r1.ebuild deleted file mode 100644 index d21fa37fa82b..000000000000 --- a/sci-mathematics/e/e-1.8-r1.ebuild +++ /dev/null @@ -1,118 +0,0 @@ -# Copyright 1999-2017 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 - -EAPI="6" - -MY_PN="E" -MY_P="${MY_PN}-${PV}" - -DESCRIPTION="E is a theorem prover for full first-order logic with equality" -HOMEPAGE="http://www4.informatik.tu-muenchen.de/~schulz/E/E.html" -SRC_URI="http://www4.in.tum.de/~schulz/WORK/E_DOWNLOAD/V_${PV}/${MY_PN}.tgz -> ${MY_P}.tgz" - -LICENSE="GPL-2" -SLOT="0/${PV}" -KEYWORDS="~amd64 ~x86" -IUSE="doc examples isabelle" - -RDEPEND="isabelle? ( - >=sci-mathematics/isabelle-2011.1-r1:= - )" -DEPEND="${RDEPEND}" - -S="${WORKDIR}"/${MY_PN} - -src_configure() { - ./configure --prefix="${ROOT}usr" \ - --man-prefix="${ROOT}share/man" \ - || die "E configure failed" - - sed -e "s@CFLAGS = @CFLAGS = ${CFLAGS} @" \ - -e "s@LD = \$(CC) @LD = \$(CC) ${LDFLAGS} @" \ - -i "${S}/Makefile.vars" \ - || die "Could not add our flags to Makefile.vars" -} - -src_install() { - dobin "${S}/PROVER/eprover" \ - "${S}/PROVER/epclextract" \ - "${S}/PROVER/eproof" \ - "${S}/PROVER/eproof_ram" \ - "${S}/PROVER/eground" \ - "${S}/PROVER/e_ltb_runner" \ - "${S}/PROVER/e_axfilter" \ - "${S}/PROVER/checkproof" \ - "${S}/PROVER/ekb_create" \ - "${S}/PROVER/ekb_delete" \ - "${S}/PROVER/ekb_ginsert" \ - "${S}/PROVER/ekb_insert" - - doman "${S}/DOC/man/eprover.1" \ - "${S}/DOC/man/epclextract.1" \ - "${S}/DOC/man/eproof.1" \ - "${S}/DOC/man/eproof_ram.1" \ - "${S}/DOC/man/eground.1" \ - "${S}/DOC/man/e_ltb_runner.1" \ - "${S}/DOC/man/e_axfilter.1" \ - "${S}/DOC/man/checkproof.1" \ - "${S}/DOC/man/ekb_create.1" \ - "${S}/DOC/man/ekb_delete.1" \ - "${S}/DOC/man/ekb_ginsert.1" \ - "${S}/DOC/man/ekb_insert.1" - - if use doc; then - pushd "${S}"/DOC || die "Could not cd to DOC" - dodoc ANNOUNCE CREDITS DONE E-REMARKS E-REMARKS.english E-USERS \ - HISTORY NEWS PORTING ReadMe THINKME TODO TPTP_SUBMISSION \ - WISHLIST eprover.pdf - dohtml *.html - dohtml estyle.sty - popd - fi - - if use examples; then - insinto /usr/share/${MY_PN}/examples - doins -r EXAMPLE_PROBLEMS - doins -r SIMPLE_APPS - fi - - if use isabelle; then - ISABELLE_HOME="$(isabelle getenv ISABELLE_HOME | cut -d'=' -f 2)" \ - || die "isabelle getenv ISABELLE_HOME failed" - [[ -n "${ISABELLE_HOME}" ]] || die "ISABELLE_HOME empty" - cat <<- EOF >> "${S}/settings" - E_HOME="${ROOT}usr/bin" - E_VERSION="${PV}" - EOF - insinto "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc" - doins "${S}/settings" - fi -} - -pkg_postinst() { - if use isabelle; then - if [ -f "${ROOT}etc/isabelle/components" ]; then - if egrep "contrib/${PN}-[0-9.]*" "${ROOT}etc/isabelle/components"; then - sed -e "/contrib\/${PN}-[0-9.]*/d" \ - -i "${ROOT}etc/isabelle/components" - fi - cat <<- EOF >> "${ROOT}etc/isabelle/components" - contrib/${PN}-${PV} - EOF - fi - fi -} - -pkg_postrm() { - if use isabelle; then - if [ ! -f "${ROOT}usr/bin/eproof" ]; then - if [ -f "${ROOT}etc/isabelle/components" ]; then - # Note: this sed should only match the version of this ebuild - # Which is what we want as we do not want to remove the line - # of a new E being installed during an upgrade. - sed -e "/contrib\/${PN}-${PV}/d" \ - -i "${ROOT}etc/isabelle/components" - fi - fi - fi -} diff --git a/sci-mathematics/e/e-2.3.ebuild b/sci-mathematics/e/e-2.3.ebuild deleted file mode 100644 index 2b9f7875941d..000000000000 --- a/sci-mathematics/e/e-2.3.ebuild +++ /dev/null @@ -1,75 +0,0 @@ -# Copyright 1999-2019 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI="7" - -MY_PN="E" -MY_P="${MY_PN}-${PV}" - -DESCRIPTION="E is a theorem prover for full first-order logic with equality" -HOMEPAGE="https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html" -SRC_URI="http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_${PV}/${MY_PN}.tgz -> ${MY_P}.tgz" -LICENSE="GPL-2" -SLOT="0/${PV}" -KEYWORDS="~amd64 ~x86" -IUSE="doc examples" - -RDEPEND="" -DEPEND="${RDEPEND} - doc? ( dev-texlive/texlive-latex )" - -S="${WORKDIR}"/${MY_PN} - -PATCHES=( "${FILESDIR}"/${PN}-2.3-build-system.patch ) - -src_prepare() { - default - rm -f DOC/eprover.pdf -} - -src_configure() { - ./configure --prefix="${ED}/usr" \ - --man-prefix="${ED}/usr/share/man" \ - || die "E configure failed" - - sed -e "s@CFLAGS = @CFLAGS = ${CFLAGS} @" \ - -e "s@LD = \$(CC) @LD = \$(CC) ${LDFLAGS} @" \ - -i "${S}/Makefile.vars" \ - || die "Could not add our flags to Makefile.vars" -} - -src_compile() { - default - use doc && emake documentation -} - -src_install() { - default - - local DOCS=( - "README.md" - "DOC/ANNOUNCE" - "DOC/CONTRIBUTORS" - "DOC/DONE" - "DOC/E-REMARKS" - "DOC/E-REMARKS.english" - "DOC/E-USERS" - "DOC/HISTORY" - "DOC/NEWS" - "DOC/PORTING" - "DOC/ReadMe" - "DOC/THINKME" - "DOC/TODO" - "DOC/TPTP_SUBMISSION" - "DOC/WISHLIST" - "DOC/eprover.pdf" - ) - local HTML_DOCS=( "DOC" ) - einstalldocs - - if use examples; then - insinto /usr/share/${MY_PN}/examples - doins -r EXAMPLE_PROBLEMS - doins -r SIMPLE_APPS - fi -} diff --git a/sci-mathematics/e/files/e-2.3-build-system.patch b/sci-mathematics/e/files/e-2.3-build-system.patch deleted file mode 100644 index 8031c20e026e..000000000000 --- a/sci-mathematics/e/files/e-2.3-build-system.patch +++ /dev/null @@ -1,8 +0,0 @@ ---- E-orig/development_tools/e_install 2019-03-13 04:55:13.000000000 +1100 -+++ E/development_tools/e_install 2019-09-11 21:11:37.628045114 +1000 -@@ -13,4 +13,4 @@ - fi - } - --testinstall $1 $2 -+install $1 $2 diff --git a/sci-mathematics/e/metadata.xml b/sci-mathematics/e/metadata.xml deleted file mode 100644 index 38c1496fe98f..000000000000 --- a/sci-mathematics/e/metadata.xml +++ /dev/null @@ -1,35 +0,0 @@ - - - - - gienah@gentoo.org - Mark Wright - - - sci-mathematics@gentoo.org - Gentoo Mathematics Project - - -E is a theorem prover for full first-order logic with equality. It -accepts a problem specification, typically consisting of a number of -first-order clauses or formulas, and a conjecture, again either in -clausal or full first-order form. The system will then try to find a -formal proof for the conjecture, assuming the axioms. - -If a proof is found, the system can provide a detailed list of proof -steps that can be individually verified. If the conjecture is -existential (i.e. it’s of the form “there exists an X with property -P”), the latest versions can also provide possible answers (values for -X). - -Development of E started as part of the E-SETHEO project at TUM. The -first public release was in in 1998, and the system has been -continuously improved ever since. I believe that E now is one of the -most powerful and friendly reasoning systems for first-order -logic. The prover has successfully participated in many competitions. - - - Add integration support for the Isabelle/HOL - theorem prover. - - -- cgit v1.2.3-65-gdbad