/[gentoo-x86]/sci-mathematics/isabelle/isabelle-2012.ebuild
Gentoo

Contents of /sci-mathematics/isabelle/isabelle-2012.ebuild

Parent Directory Parent Directory | Revision Log Revision Log


Revision 1.5 - (show annotations) (download)
Sun Dec 9 09:24:29 2012 UTC (2 years, 8 months ago) by gienah
Branch: MAIN
Changes since 1.4: +5 -2 lines
Add dependency on sci-mathematics/sha1-polyml, which fixes warnings for some functionality, like using Simpl/Vcg.

(Portage version: 2.1.11.33/cvs/Linux x86_64, signed Manifest commit with key 618E971F)

1 # Copyright 1999-2012 Gentoo Foundation
2 # Distributed under the terms of the GNU General Public License v2
3 # $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/isabelle-2012.ebuild,v 1.4 2012/12/05 10:09:32 gienah Exp $
4
5 EAPI="5"
6
7 inherit eutils java-pkg-2 multilib versionator
8
9 MY_PN="Isabelle"
10 MY_PV=$(replace_all_version_separators '-')
11 MY_P="${MY_PN}${MY_PV}"
12
13 JEDIT_PV="20120414"
14 JEDIT_PN="jedit_build"
15 JEDIT_P="${JEDIT_PN}-${JEDIT_PV}"
16
17 DESCRIPTION="Isabelle is a generic proof assistant"
18 HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html"
19 SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz
20 doc? ( http://dev.gentoo.org/~gienah/snapshots/${MY_P}-doc-src.tar.gz )
21 pide? ( http://www4.in.tum.de/~wenzelm/test/${JEDIT_P}.tar.gz )"
22
23 LICENSE="BSD"
24 SLOT="0/${PV}"
25 KEYWORDS="~amd64 ~x86"
26 ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents"
27 IUSE="${ALL_LOGICS} doc graphbrowsing ledit readline pide +proofgeneral test"
28
29 #upstream says
30 #bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
31 #for document preparation: complete LaTeX
32 DEPEND=">=app-shells/bash-3.0
33 >=dev-lang/polyml-5.4.1:=[-portable]
34 >=dev-lang/perl-5.8.8-r2"
35
36 RDEPEND="dev-perl/libwww-perl
37 sci-mathematics/sha1-polyml
38 doc? (
39 virtual/latex-base
40 dev-tex/rail
41 )
42 proofgeneral? (
43 app-emacs/proofgeneral
44 )
45 pide? (
46 >=dev-lang/scala-2.8.2
47 )
48 ledit? (
49 app-misc/ledit
50 )
51 readline? (
52 app-misc/rlwrap
53 )
54 ${DEPEND}"
55
56 S="${WORKDIR}"/Isabelle${MY_PV}
57 JEDIT_S="${WORKDIR}/${JEDIT_P}"
58 TARGETDIR="/usr/share/Isabelle"${MY_PV}
59 LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
60
61 pkg_setup() {
62 java-pkg-2_pkg_setup
63 if ! use proofgeneral
64 then
65 ewarn "You have deselected the Proof General interface."
66 ewarn "Only a text terminal will be installed."
67 ewarn "Emerge Isabelle with the proofgeneral USE flag enabled"
68 ewarn "to get the common interface, that most people want."
69 fi
70 }
71
72 src_prepare() {
73 java-pkg-2_src_prepare
74 epatch "${FILESDIR}/${PN}-2012-gentoo-settings.patch"
75 # http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/2732
76 epatch "${FILESDIR}/${PN}-2012-signal-handling.patch"
77 # http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/2780
78 epatch "${FILESDIR}/${PN}-2012-redundant-equations-in-function-definitions-error.patch"
79 polymlver=$(poly -v | cut -d' ' -f2)
80 polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
81 sed -e "s@5.4.0@${polymlver}@g" \
82 -i "${S}/etc/settings" \
83 || die "Could not configure polyml version in etc/settings"
84 sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \
85 -i "${S}/etc/settings" \
86 || die "Could not configure polyml ML_HOME in etc/settings"
87 sed -e "s@x86_64@${polymlarch}@g" \
88 -i "${S}/etc/settings" \
89 || die "Could not configure polyml arch in etc/settings"
90 sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \
91 -i "${S}/etc/settings" \
92 || die "Could not configure PROOFGENERAL_HOME in etc/settings"
93 sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \
94 -i "${S}/etc/settings" \
95 || die "Could not configure Isabelle lib directory in etc/settings"
96 epatch "${FILESDIR}/${PN}-2012-graphbrowser.patch"
97 epatch "${FILESDIR}/${PN}-2012-libsha1.patch"
98 cat <<- EOF >> "${S}/etc/settings"
99
100 ISABELLE_GHC="${ROOT}usr/bin/ghc"
101 ISABELLE_OCAML="${ROOT}usr/bin/ocaml"
102 ISABELLE_SWIPL="${ROOT}usr/bin/swipl"
103 ISABELLE_JDK_HOME="\$(java-config --jdk-home)"
104 SCALA_HOME="${ROOT}usr/share/scala"
105 SHA1_HOME="/usr/$(get_libdir)/sha1-polyml"
106 EOF
107 if use pide; then
108 cat <<- EOF >> "${S}/etc/settings"
109 ISABELLE_JEDIT_BUILD_HOME="\$ISABELLE_HOME/${JEDIT_P}"
110 init_component ${JEDIT_S}
111 EOF
112 fi
113 if use ledit && !use readline; then
114 epatch "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch"
115 fi
116 }
117
118 src_compile() {
119 LOGICS=""
120 for l in "${ALL_LOGICS}"; do
121 if has "${l/+/}"; then
122 LOGICS="${LOGICS} ${l/+/}"
123 fi
124 done
125 einfo "Building Isabelle logics ${LOGICS}. This may take some time."
126 ./build -b -i "${LOGICS}" || die "building logics failed"
127 ./bin/isabelle makeall || die "isabelle makeall failed"
128 if use graphbrowsing
129 then
130 rm -f "${S}/lib/browser/GraphBrowser.jar" \
131 || die "failed cleaning graph browser directory"
132 pushd "${S}/lib/browser" \
133 || die "Could not change directory to lib/browser"
134 ./build || die "failed building the graph browser"
135 popd
136 fi
137 if use pide; then
138 pushd "${S}/src/Tools/jEdit" \
139 || die "Could not change directory to src/Tools/jEdit"
140 "${S}"/bin/isabelle jedit -b -f \
141 || die "pide build failed"
142 popd
143 # The jedit_build stuff is only required to build
144 # Isabelle/jEdit Prover IDE (PIDE). These 2 lines need to be deleted
145 # from etc/settings as the jedit_build source code is not installed
146 sed -e '/ISABELLE_JEDIT_BUILD_HOME/d' \
147 -e '/init_component/d' \
148 -i "${S}/etc/settings" \
149 || die "Could not delete jedit_build lines from etc/settings"
150 fi
151 }
152
153 src_test() {
154 einfo "Running tests. A test run can take up to several hours!"
155 ./build -b -t || die "tests failed"
156 }
157
158 src_install() {
159 exeinto ${TARGETDIR}/bin
160 doexe bin/isabelle-process bin/isabelle
161
162 insinto ${TARGETDIR}
163 doins -r src
164 doins -r lib
165
166 docompress -x /usr/share/doc/${PF}
167 dodoc -r doc
168 if use doc; then
169 dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc"
170 # The build of sci-mathematics/haskabelle with use doc requires
171 # sci-mathematics/isabelle[doc?]. The haskabelle doc build requires
172 # the doc-src directory stuff in the isabelle package. Which is not
173 # provided in the Isabelle 2012 src tarball. So extract it from a
174 # snapshot of the isabelle repo taken soon after the Isabelle 2012
175 # release.
176 doins -r doc-src
177 for i in "./doc-src/IsarRef/showsymbols" \
178 "./doc-src/TutorialI/Overview/LNCS/makeDemo" \
179 "./doc-src/TutorialI/isa-index" \
180 "./doc-src/sedindex"
181 do
182 exeinto $(dirname "${TARGETDIR}/${i}")
183 doexe ${i}
184 done
185 fi
186
187 for i in "./build" \
188 "./src/Pure/mk" \
189 "./src/Pure/build-jars" \
190 "./src/Tools/JVM/build" \
191 "./src/Tools/JVM/java_ext_dirs" \
192 "./src/Tools/jEdit/lib/Tools/jedit" \
193 "./src/Tools/Metis/fix_metis_license" \
194 "./src/Tools/Metis/make_metis" \
195 "./src/Tools/Metis/scripts/mlpp" \
196 "./src/Tools/WWW_Find/lib/Tools/wwwfind" \
197 "./src/Tools/Code/lib/Tools/codegen" \
198 "./src/HOL/Mirabelle/lib/Tools/mirabelle" \
199 "./src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \
200 "./src/HOL/Tools/SMT/lib/scripts/remote_smt" \
201 "./src/HOL/Tools/ATP/scripts/remote_atp" \
202 "./src/HOL/Tools/ATP/scripts/spass" \
203 "./src/HOL/Mutabelle/lib/Tools/mutabelle" \
204 "./src/HOL/TPTP/TPTP_Parser/make_mlyacclib" \
205 "./src/HOL/TPTP/TPTP_Parser/make_tptp_parser" \
206 "./src/HOL/TPTP/lib/Tools/tptp_isabelle_demo" \
207 "./src/HOL/TPTP/lib/Tools/tptp_graph" \
208 "./src/HOL/TPTP/lib/Tools/tptp_isabelle_comp" \
209 "./src/HOL/TPTP/lib/Tools/tptp_refute" \
210 "./src/HOL/TPTP/lib/Tools/tptp_translate" \
211 "./src/HOL/TPTP/lib/Tools/tptp_sledgehammer" \
212 "./src/HOL/TPTP/lib/Tools/tptp_nitpick" \
213 "./src/HOL/Library/Sum_of_Squares/neos_csdp_client" \
214 "./src/HOL/IMP/export.sh" \
215 "./lib/browser/build" \
216 "./lib/Tools/tty" \
217 "./lib/Tools/mkproject" \
218 "./lib/Tools/keywords" \
219 "./lib/Tools/browser" \
220 "./lib/Tools/install" \
221 "./lib/Tools/mkdir" \
222 "./lib/Tools/unsymbolize" \
223 "./lib/Tools/getenv" \
224 "./lib/Tools/java" \
225 "./lib/Tools/make" \
226 "./lib/Tools/emacs" \
227 "./lib/Tools/scala" \
228 "./lib/Tools/print" \
229 "./lib/Tools/latex" \
230 "./lib/Tools/findlogics" \
231 "./lib/Tools/doc" \
232 "./lib/Tools/logo" \
233 "./lib/Tools/usedir" \
234 "./lib/Tools/yxml" \
235 "./lib/Tools/version" \
236 "./lib/Tools/makeall" \
237 "./lib/Tools/scalac" \
238 "./lib/Tools/document" \
239 "./lib/Tools/env" \
240 "./lib/Tools/display" \
241 "./lib/Tools/dimacs2hol" \
242 "./lib/scripts/keywords" \
243 "./lib/scripts/unsymbolize" \
244 "./lib/scripts/run-polyml" \
245 "./lib/scripts/run-smlnj" \
246 "./lib/scripts/feeder" \
247 "./lib/scripts/yxml" \
248 "./lib/scripts/polyml-version" \
249 "./lib/scripts/process"
250 do
251 exeinto $(dirname "${TARGETDIR}/${i}")
252 doexe ${i}
253 done
254
255 dodir /etc/isabelle
256 insinto /etc/isabelle
257 doins -r etc/*
258
259 dosym /etc/isabelle "${TARGETDIR}/etc"
260 dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
261
262 insinto ${LIBDIR}
263 doins -r heaps
264
265 bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \
266 || die "isabelle install failed"
267 newicon lib/icons/isabelle.xpm "${PN}.xpm"
268 dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README
269
270 java-pkg_regjar \
271 "${ED}${TARGETDIR}/src/Tools/JVM/java_ext_dirs.jar" \
272 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/QuickNotepad.jar" \
273 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Console.jar" \
274 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/ErrorList.jar" \
275 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Hyperlinks.jar" \
276 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/SideKick.jar" \
277 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/cobra.jar" \
278 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/js.jar" \
279 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/scala-compiler.jar" \
280 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" \
281 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jedit.jar" \
282 "${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \
283 "${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \
284 "${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \
285 "${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar"
286 }
287
288 pkg_postinst() {
289 # If any of the directories in /etc/isabelle/components do not exist, then
290 # even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to
291 # to delete any non-existing directories. If an old Isabelle version was
292 # installed with component ebuilds like sci-mathematics/e, then the
293 # Isabelle version is upgraded, then the contrib directories will not
294 # exist initially, it is necessary to delete them from /etc/isabelle/components.
295 # Then these components are rebuilt (creating these directories) using the
296 # EAPI=5 subslot depends.
297 for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components")
298 do
299 if [ ! -d /usr/share/Isabelle2012/${i} ]; then
300 sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components"
301 fi
302 done
303 if use ledit && use readline; then
304 elog "Both readline and ledit use flags specified. The default setting"
305 elog "if both are installed is to use readline (rlwrap), this can be"
306 elog "modfied by editing the ISABELLE_LINE_EDITOR setting in"
307 elog "${ROOT}/etc/isabelle/settings"
308 fi
309 elog "Please ensure you have a pdf viewer installed, for example:"
310 elog "As root: emerge app-text/zathura-pdf-poppler"
311 elog "Please configure your preferred pdf viewer, something like:"
312 elog "As normal user: xdg-mime default zathura.desktop application/pdf"
313 elog "Or alternatively by editing the PDF_VIEWER variable in the system"
314 elog "settings file ${ROOT}etc/isabelle/settings and/or the user"
315 elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings"
316 elog "To improve sledgehammer performance, consider installing:"
317 elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass"
318 elog "For nitpick it is necessary to install:"
319 elog "emerge sci-mathematics/kodkodi"
320 }

  ViewVC Help
Powered by ViewVC 1.1.20