1 |
gienah 12/01/08 12:35:43 |
2 |
|
3 |
Added: metadata.xml ChangeLog isabelle-2011.1.ebuild |
4 |
Log: |
5 |
New ebuild, thanks Mr. Anderson for earlier version, fixes #397995 |
6 |
|
7 |
(Portage version: 2.1.10.44/cvs/Linux x86_64) |
8 |
|
9 |
Revision Changes Path |
10 |
1.1 sci-mathematics/isabelle/metadata.xml |
11 |
|
12 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/metadata.xml?rev=1.1&view=markup |
13 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/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 |
<herd>sci-mathematics</herd> |
21 |
<longdescription lang='en'> |
22 |
Isabelle is a generic proof assistant. It allows mathematical |
23 |
formulas to be expressed in a formal language and provides tools |
24 |
for proving those formulas in a logical calculus. The main |
25 |
application is the formalization of mathematical proofs and in |
26 |
particular formal verification, which includes proving the |
27 |
correctness of computer hardware or software and proving |
28 |
properties of computer languages and protocols. |
29 |
</longdescription> |
30 |
<use> |
31 |
<flag name='Pure'>Pure is the basis for all object-logics.</flag> |
32 |
<flag name='FOL'>FOL (Many-sorted First-Order Logic) provides basic |
33 |
classical and intuitionistic first-order logic. It is polymorphic.</flag> |
34 |
<flag name='HOL'>(Higher-Order Logic) is a version of classical higher-order |
35 |
logic resembling that of the HOL System.</flag> |
36 |
<flag name='ZF'>ZF (Set Theory) offers a formulation of Zermelo-Fraenkel |
37 |
set theory on top of FOL.</flag> |
38 |
<flag name='CCL'>CCL (Classical Computational Logic)</flag> |
39 |
<flag name='CTT'>CTT (Constructive Type Theory) is an extensional version |
40 |
of Martin-Löf's Type Theory.</flag> |
41 |
<flag name='Cube'>Cube (The Lambda Cube)</flag> |
42 |
<flag name='FOLP'>FOLP (FOL with Proof Terms)</flag> |
43 |
<flag name='LCF'>LCF (Logic of Computable Functions)</flag> |
44 |
<flag name='Sequents'>Sequents (first-order, modal and linear logics)</flag> |
45 |
<flag name='graphbrowsing'>Generate theory browsing information, |
46 |
including HTML documents that show a theory's definition, the |
47 |
theorems proved in its ML file and the relationship with its |
48 |
ancestors and descendants.</flag> |
49 |
<flag name='proofgeneral'>Add support for the |
50 |
<pkg>app-emacs/proofgeneral</pkg> proof assistant front end.</flag> |
51 |
</use> |
52 |
</pkgmetadata> |
53 |
|
54 |
|
55 |
|
56 |
1.1 sci-mathematics/isabelle/ChangeLog |
57 |
|
58 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/ChangeLog?rev=1.1&view=markup |
59 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/ChangeLog?rev=1.1&content-type=text/plain |
60 |
|
61 |
Index: ChangeLog |
62 |
=================================================================== |
63 |
# ChangeLog for sci-mathematics/isabelle |
64 |
# Copyright 1999-2012 Gentoo Foundation; Distributed under the GPL v2 |
65 |
# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/ChangeLog,v 1.1 2012/01/08 12:35:43 gienah Exp $ |
66 |
|
67 |
*isabelle-2011.1 (08 Jan 2012) |
68 |
|
69 |
08 Jan 2012; Mark Wright <gienah@g.o> +isabelle-2011.1.ebuild, |
70 |
+files/isabelle-2011.1-graphbrowser.patch, |
71 |
+files/isabelle-2011.1-proofgeneral-gentoo-path.patch, +metadata.xml: |
72 |
New ebuild, thanks Mr. Anderson for earlier version, fixes #397995 |
73 |
|
74 |
|
75 |
|
76 |
|
77 |
1.1 sci-mathematics/isabelle/isabelle-2011.1.ebuild |
78 |
|
79 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild?rev=1.1&view=markup |
80 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild?rev=1.1&content-type=text/plain |
81 |
|
82 |
Index: isabelle-2011.1.ebuild |
83 |
=================================================================== |
84 |
# Copyright 1999-2012 Gentoo Foundation |
85 |
# Distributed under the terms of the GNU General Public License v2 |
86 |
# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild,v 1.1 2012/01/08 12:35:43 gienah Exp $ |
87 |
|
88 |
EAPI="4" |
89 |
|
90 |
JAVA_PKG_OPT_USE="graphbrowsing" |
91 |
inherit eutils java-pkg-opt-2 multilib versionator |
92 |
|
93 |
MY_PN="Isabelle" |
94 |
typeset -u MY_PV |
95 |
MY_PV=$(replace_all_version_separators '-') |
96 |
MY_P="${MY_PN}${MY_PV}" |
97 |
|
98 |
DESCRIPTION="Isabelle is a generic proof assistant" |
99 |
HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html" |
100 |
SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz" |
101 |
|
102 |
LICENSE="BSD" |
103 |
SLOT="0" |
104 |
KEYWORDS="~x86 ~amd64" |
105 |
ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents" |
106 |
IUSE="${ALL_LOGICS} doc graphbrowsing +pdf +proofgeneral" |
107 |
|
108 |
#upstream says |
109 |
#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, |
110 |
#for document preparation: complete LaTeX |
111 |
DEPEND=">=app-shells/bash-3.0 |
112 |
>=dev-lang/polyml-5.4.1 |
113 |
>=dev-lang/perl-5.8.8-r2" |
114 |
|
115 |
RDEPEND="doc? ( |
116 |
virtual/latex-base |
117 |
dev-tex/rail |
118 |
) |
119 |
pdf? ( || ( app-text/xpdf |
120 |
app-text/gv |
121 |
app-text/gsview |
122 |
app-text/epdfview |
123 |
app-text/acroread |
124 |
app-text/zathura ) |
125 |
) |
126 |
proofgeneral? ( |
127 |
app-emacs/proofgeneral |
128 |
) |
129 |
${DEPEND}" |
130 |
|
131 |
S="${WORKDIR}"/Isabelle${MY_PV} |
132 |
TARGETDIR="/usr/share/Isabelle"${MY_PV} |
133 |
LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV} |
134 |
|
135 |
pkg_setup() { |
136 |
java-pkg-opt-2_pkg_setup |
137 |
if ! use proofgeneral |
138 |
then |
139 |
ewarn "You have deselected the Proof General interface." |
140 |
ewarn "Only a text terminal will be installed." |
141 |
ewarn "Emerge Isabelle with the proofgeneral USE flag enabled" |
142 |
ewarn "to get the common interface, that most people want." |
143 |
fi |
144 |
} |
145 |
|
146 |
src_prepare() { |
147 |
java-pkg-opt-2_src_prepare |
148 |
if use proofgeneral; then |
149 |
epatch "${FILESDIR}/${PN}-2011.1-proofgeneral-gentoo-path.patch" |
150 |
polymlver=$(poly -v | cut -d' ' -f2) |
151 |
polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1) |
152 |
sed -e "s@5.4.0@${polymlver}@g" \ |
153 |
-i "${S}/etc/settings" || die "Could not configure polyml version in etc/settings" |
154 |
sed -e "s@x86_64@${polymlarch}@g" \ |
155 |
-i "${S}/etc/settings" || die "Could not configure polyml arch in etc/settings" |
156 |
fi |
157 |
if use graphbrowsing; then |
158 |
epatch "${FILESDIR}/${PN}-2011.1-graphbrowser.patch" |
159 |
fi |
160 |
} |
161 |
|
162 |
src_compile() { |
163 |
LOGICS="" |
164 |
for l in "${ALL_LOGICS}"; do |
165 |
if has "${l/+/}"; then |
166 |
LOGICS="${LOGICS} ${l/+/}" |
167 |
fi |
168 |
done |
169 |
einfo "Building Isabelle logics ${LOGICS}. This may take some time." |
170 |
./build -b -i "${LOGICS}" || die "building logics failed" |
171 |
./bin/isabelle makeall || die "isabelle makeall failed" |
172 |
if use graphbrowsing |
173 |
then |
174 |
rm -f "${S}/lib/browser/GraphBrowser.jar" || die "failed cleaning graph browser directory" |
175 |
cd "${S}/lib/browser" |
176 |
./build || die "failed building the graph browser" |
177 |
cd "${S}" |
178 |
fi |
179 |
} |
180 |
|
181 |
src_test() { |
182 |
einfo "Running tests. A test run can take up to several hours!" |
183 |
./build -b -t |
184 |
} |
185 |
|
186 |
src_install() { |
187 |
exeinto ${TARGETDIR}/bin |
188 |
doexe bin/isabelle-process bin/isabelle |
189 |
|
190 |
exeinto ${TARGETDIR} |
191 |
doexe build |
192 |
|
193 |
insinto ${TARGETDIR} |
194 |
doins -r src |
195 |
dodoc -r doc |
196 |
|
197 |
dodir /etc/isabelle |
198 |
insinto /etc/isabelle |
199 |
doins -r etc |
200 |
|
201 |
dosym /etc/isabelle "${TARGETDIR}/etc" |
202 |
dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps" |
203 |
|
204 |
insinto ${LIBDIR} |
205 |
doins -r heaps |
206 |
|
207 |
# use cp to keep file attributes |
208 |
cp -R lib "${ED}${TARGETDIR}" || die "install lib failed" |
209 |
|
210 |
bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \ |
211 |
|| die "isabelle install failed" |
212 |
newicon lib/icons/isabelle.xpm "${PN}.xpm" |
213 |
dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README |
214 |
|
215 |
java-pkg_regjar \ |
216 |
"${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \ |
217 |
"${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \ |
218 |
"${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \ |
219 |
"${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \ |
220 |
"${ED}${TARGETDIR}/lib/classes/java_ext_dirs.jar" |
221 |
} |
222 |
|
223 |
pkg_postinst() { |
224 |
elog "You will need to re-emerge Isabelle after emerging polyml." |
225 |
if use pdf; then |
226 |
einfo "Please configure your preferred pdf viewer by editing" |
227 |
einfo "the PDF_VIEWER variable in the system settings file" |
228 |
einfo "/etc/conf/isabelle and/or the user settings file" |
229 |
einfo "\$HOME/.isabelle/${MY_P}" |
230 |
fi |
231 |
} |