| 1 |
gienah 12/05/30 00:55:23 |
| 2 |
|
| 3 |
Added: metadata.xml e-1.5.ebuild ChangeLog |
| 4 |
Log: |
| 5 |
Add E theorem prover, with optional Isabelle/HOL sledgehammer integration. |
| 6 |
|
| 7 |
(Portage version: 2.1.10.63/cvs/Linux x86_64) |
| 8 |
|
| 9 |
Revision Changes Path |
| 10 |
1.1 sci-mathematics/e/metadata.xml |
| 11 |
|
| 12 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/e/metadata.xml?rev=1.1&view=markup |
| 13 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/e/metadata.xml?rev=1.1&content-type=text/plain |
| 14 |
|
| 15 |
Index: metadata.xml |
| 16 |
=================================================================== |
| 17 |
<?xml version="1.0" encoding="UTF-8"?> |
| 18 |
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> |
| 19 |
<pkgmetadata> |
| 20 |
<maintainer> |
| 21 |
<email>gienah@g.o></email> |
| 22 |
</maintainer> |
| 23 |
<herd>sci-mathematics</herd> |
| 24 |
<longdescription lang='en'> |
| 25 |
E is a theorem prover for full first-order logic with equality. It |
| 26 |
accepts a problem specification, typically consisting of a number of |
| 27 |
first-order clauses or formulas, and a conjecture, again either in |
| 28 |
clausal or full first-order form. The system will then try to find a |
| 29 |
formal proof for the conjecture, assuming the axioms. |
| 30 |
|
| 31 |
If a proof is found, the system can provide a detailed list of proof |
| 32 |
steps that can be individually verified. If the conjecture is |
| 33 |
existential (i.e. it’s of the form “there exists an X with property |
| 34 |
P”), the latest versions can also provide possible answers (values for |
| 35 |
X). |
| 36 |
|
| 37 |
Development of E started as part of the E-SETHEO project at TUM. The |
| 38 |
first public release was in in 1998, and the system has been |
| 39 |
continuously improved ever since. I believe that E now is one of the |
| 40 |
most powerful and friendly reasoning systems for first-order |
| 41 |
logic. The prover has successfully participated in many competitions. |
| 42 |
</longdescription> |
| 43 |
<use> |
| 44 |
<flag name='isabelle'>Add integration support for the Isabelle/HOL |
| 45 |
theorem prover.</flag> |
| 46 |
</use> |
| 47 |
</pkgmetadata> |
| 48 |
|
| 49 |
|
| 50 |
|
| 51 |
1.1 sci-mathematics/e/e-1.5.ebuild |
| 52 |
|
| 53 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/e/e-1.5.ebuild?rev=1.1&view=markup |
| 54 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/e/e-1.5.ebuild?rev=1.1&content-type=text/plain |
| 55 |
|
| 56 |
Index: e-1.5.ebuild |
| 57 |
=================================================================== |
| 58 |
# Copyright 1999-2012 Gentoo Foundation |
| 59 |
# Distributed under the terms of the GNU General Public License v2 |
| 60 |
# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/e/e-1.5.ebuild,v 1.1 2012/05/30 00:55:22 gienah Exp $ |
| 61 |
|
| 62 |
EAPI="4" |
| 63 |
|
| 64 |
MY_PN="E" |
| 65 |
MY_P="${MY_PN}-${PV}" |
| 66 |
|
| 67 |
DESCRIPTION="E is a theorem prover for full first-order logic with equality" |
| 68 |
HOMEPAGE="http://www4.informatik.tu-muenchen.de/~schulz/E/E.html" |
| 69 |
SRC_URI="http://www4.in.tum.de/~schulz/WORK/E_DOWNLOAD/V_${PV}/${MY_PN}.tgz -> ${MY_P}.tgz" |
| 70 |
|
| 71 |
LICENSE="GPL-2" |
| 72 |
SLOT="0" |
| 73 |
KEYWORDS="~x86 ~amd64" |
| 74 |
IUSE="doc examples isabelle" |
| 75 |
|
| 76 |
RDEPEND="" |
| 77 |
DEPEND="${RDEPEND} |
| 78 |
isabelle? ( |
| 79 |
>=sci-mathematics/isabelle-2011.1-r1 |
| 80 |
)" |
| 81 |
|
| 82 |
S="${WORKDIR}"/${MY_PN} |
| 83 |
|
| 84 |
src_configure() { |
| 85 |
./configure --prefix="${ROOT}usr" \ |
| 86 |
--man-prefix="${ROOT}share/man" \ |
| 87 |
|| die "E configure failed" |
| 88 |
|
| 89 |
sed -e "s@CFLAGS = @CFLAGS = ${CFLAGS} @" \ |
| 90 |
-e "s@LD = \$(CC) @LD = \$(CC) ${LDFLAGS} @" \ |
| 91 |
-i "${S}/Makefile.vars" \ |
| 92 |
|| die "Could not add our flags to Makefile.vars" |
| 93 |
} |
| 94 |
|
| 95 |
src_install() { |
| 96 |
for i in "${S}/PROVER/eprover" \ |
| 97 |
"${S}/PROVER/epclextract" \ |
| 98 |
"${S}/PROVER/eproof" \ |
| 99 |
"${S}/PROVER/eproof_ram" \ |
| 100 |
"${S}/PROVER/eground" \ |
| 101 |
"${S}/PROVER/e_ltb_runner" \ |
| 102 |
"${S}/PROVER/e_axfilter" \ |
| 103 |
"${S}/PROVER/checkproof" \ |
| 104 |
"${S}/PROVER/ekb_create" \ |
| 105 |
"${S}/PROVER/ekb_delete" \ |
| 106 |
"${S}/PROVER/ekb_ginsert" \ |
| 107 |
"${S}/PROVER/ekb_insert" |
| 108 |
do |
| 109 |
dobin "${i}" |
| 110 |
done |
| 111 |
|
| 112 |
for i in "${S}/DOC/man/eprover.1" \ |
| 113 |
"${S}/DOC/man/epclextract.1" \ |
| 114 |
"${S}/DOC/man/eproof.1" \ |
| 115 |
"${S}/DOC/man/eproof_ram.1" \ |
| 116 |
"${S}/DOC/man/eground.1" \ |
| 117 |
"${S}/DOC/man/e_ltb_runner.1" \ |
| 118 |
"${S}/DOC/man/e_axfilter.1" \ |
| 119 |
"${S}/DOC/man/checkproof.1" \ |
| 120 |
"${S}/DOC/man/ekb_create.1" \ |
| 121 |
"${S}/DOC/man/ekb_delete.1" \ |
| 122 |
"${S}/DOC/man/ekb_ginsert.1" \ |
| 123 |
"${S}/DOC/man/ekb_insert.1" |
| 124 |
do |
| 125 |
doman "${i}" |
| 126 |
done |
| 127 |
|
| 128 |
if use doc; then |
| 129 |
pushd "${S}"/DOC || die "Could not cd to DOC" |
| 130 |
dodoc ANNOUNCE CREDITS DONE E-REMARKS E-REMARKS.english E-USERS \ |
| 131 |
HISTORY NEWS PORTING ReadMe THINKME TODO TPTP_SUBMISSION \ |
| 132 |
WISHLIST eprover.pdf |
| 133 |
dohtml *.html |
| 134 |
insinto /usr/share/doc/${PF}/html |
| 135 |
doins estyle.sty |
| 136 |
popd |
| 137 |
fi |
| 138 |
|
| 139 |
if use examples; then |
| 140 |
dodir /usr/share/${MY_PN}/examples |
| 141 |
insinto /usr/share/${MY_PN}/examples |
| 142 |
doins -r EXAMPLE_PROBLEMS |
| 143 |
doins -r SIMPLE_APPS |
| 144 |
fi |
| 145 |
|
| 146 |
if use isabelle; then |
| 147 |
ISABELLE_HOME="$(isabelle getenv ISABELLE_HOME | cut -d'=' -f 2)" \ |
| 148 |
|| die "isabelle getenv ISABELLE_HOME failed" |
| 149 |
if [[ -z "${ISABELLE_HOME}" ]]; then |
| 150 |
die "ISABELLE_HOME empty" |
| 151 |
fi |
| 152 |
dodir "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc" |
| 153 |
cat <<- EOF >> "${S}/settings" |
| 154 |
E_HOME="${ROOT}usr/bin" |
| 155 |
E_VERSION="${PV}" |
| 156 |
EOF |
| 157 |
insinto "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc" |
| 158 |
doins "${S}/settings" |
| 159 |
fi |
| 160 |
} |
| 161 |
|
| 162 |
pkg_postinst() { |
| 163 |
if use isabelle; then |
| 164 |
if [ -f "${ROOT}etc/isabelle/components" ]; then |
| 165 |
if egrep "contrib/${PN}-[0-9.]*" "${ROOT}etc/isabelle/components"; then |
| 166 |
sed -e "/contrib\/${PN}-[0-9.]*/d" \ |
| 167 |
-i "${ROOT}etc/isabelle/components" |
| 168 |
fi |
| 169 |
cat <<- EOF >> "${ROOT}etc/isabelle/components" |
| 170 |
contrib/${PN}-${PV} |
| 171 |
EOF |
| 172 |
fi |
| 173 |
fi |
| 174 |
} |
| 175 |
|
| 176 |
pkg_postrm() { |
| 177 |
if use isabelle; then |
| 178 |
if [ ! -f "${ROOT}usr/bin/eproof" ]; then |
| 179 |
if [ -f "${ROOT}etc/isabelle/components" ]; then |
| 180 |
# Note: this sed should only match the version of this ebuild |
| 181 |
# Which is what we want as we do not want to remove the line |
| 182 |
# of a new E being installed during an upgrade. |
| 183 |
sed -e "/contrib\/${PN}-${PV}/d" \ |
| 184 |
-i "${ROOT}etc/isabelle/components" |
| 185 |
fi |
| 186 |
fi |
| 187 |
fi |
| 188 |
} |
| 189 |
|
| 190 |
|
| 191 |
|
| 192 |
1.1 sci-mathematics/e/ChangeLog |
| 193 |
|
| 194 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/e/ChangeLog?rev=1.1&view=markup |
| 195 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/e/ChangeLog?rev=1.1&content-type=text/plain |
| 196 |
|
| 197 |
Index: ChangeLog |
| 198 |
=================================================================== |
| 199 |
# ChangeLog for sci-mathematics/e |
| 200 |
# Copyright 1999-2012 Gentoo Foundation; Distributed under the GPL v2 |
| 201 |
# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/e/ChangeLog,v 1.1 2012/05/30 00:55:22 gienah Exp $ |
| 202 |
|
| 203 |
*e-1.5 (30 May 2012) |
| 204 |
|
| 205 |
30 May 2012; Mark Wright <gienah@g.o> +e-1.5.ebuild, +metadata.xml: |
| 206 |
Add E theorem prover, with optional Isabelle/HOL sledgehammer integration. |
Archives