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

Contents of /sci-mathematics/isabelle/isabelle-2011.1-r1.ebuild

Parent Directory Parent Directory | Revision Log Revision Log


Revision 1.4 - (show annotations) (download)
Sun Dec 9 09:24:29 2012 UTC (21 months, 1 week ago) by gienah
Branch: MAIN
Changes since 1.3: +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-2011.1-r1.ebuild,v 1.3 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 DESCRIPTION="Isabelle is a generic proof assistant"
14 HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html"
15 SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz"
16
17 LICENSE="BSD"
18 SLOT="0/${PV}"
19 KEYWORDS="~amd64 ~x86"
20 ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents"
21 IUSE="${ALL_LOGICS} doc graphbrowsing ledit readline +proofgeneral test"
22
23 #upstream says
24 #bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
25 #for document preparation: complete LaTeX
26 DEPEND=">=app-shells/bash-3.0
27 >=dev-lang/polyml-5.4.1:=[-portable]
28 >=dev-lang/perl-5.8.8-r2"
29
30 RDEPEND="dev-perl/libwww-perl
31 sci-mathematics/sha1-polyml
32 doc? (
33 virtual/latex-base
34 dev-tex/rail
35 )
36 proofgeneral? (
37 app-emacs/proofgeneral
38 )
39 ledit? (
40 app-misc/ledit
41 )
42 readline? (
43 app-misc/rlwrap
44 )
45 ${DEPEND}"
46
47 S="${WORKDIR}"/Isabelle${MY_PV}
48 TARGETDIR="/usr/share/Isabelle"${MY_PV}
49 LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
50
51 pkg_setup() {
52 java-pkg-2_pkg_setup
53 if ! use proofgeneral
54 then
55 ewarn "You have deselected the Proof General interface."
56 ewarn "Only a text terminal will be installed."
57 ewarn "Emerge Isabelle with the proofgeneral USE flag enabled"
58 ewarn "to get the common interface, that most people want."
59 fi
60 }
61
62 src_prepare() {
63 java-pkg-2_src_prepare
64 epatch "${FILESDIR}/${PN}-2011.1-gentoo-settings.patch"
65 polymlver=$(poly -v | cut -d' ' -f2)
66 polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
67 sed -e "s@5.4.0@${polymlver}@g" \
68 -i "${S}/etc/settings" \
69 || die "Could not configure polyml version in etc/settings"
70 sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \
71 -i "${S}/etc/settings" \
72 || die "Could not configure polyml ML_HOME in etc/settings"
73 sed -e "s@x86_64@${polymlarch}@g" \
74 -i "${S}/etc/settings" \
75 || die "Could not configure polyml arch in etc/settings"
76 sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \
77 -i "${S}/etc/settings" \
78 || die "Could not configure PROOFGENERAL_HOME in etc/settings"
79 sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \
80 -i "${S}/etc/settings" \
81 || die "Could not configure Isabelle lib directory in etc/settings"
82 epatch "${FILESDIR}/${PN}-2011.1-graphbrowser.patch"
83 epatch "${FILESDIR}/${PN}-2011.1-libsha1.patch"
84 cat <<- EOF >> "${S}/etc/settings"
85
86 ISABELLE_GHC="${ROOT}usr/bin/ghc"
87 ISABELLE_OCAML="${ROOT}usr/bin/ocaml"
88 ISABELLE_SWIPL="${ROOT}usr/bin/swipl"
89 ISABELLE_JDK_HOME="\$(java-config --jdk-home)"
90 SCALA_HOME="${ROOT}usr/share/scala"
91 SHA1_HOME="/usr/$(get_libdir)/sha1-polyml"
92 EOF
93 if use ledit && !use readline; then
94 epatch "${FILESDIR}/${PN}-2011.1-reverse-line-editor-order.patch"
95 fi
96 }
97
98 src_compile() {
99 LOGICS=""
100 for l in "${ALL_LOGICS}"; do
101 if has "${l/+/}"; then
102 LOGICS="${LOGICS} ${l/+/}"
103 fi
104 done
105 einfo "Building Isabelle logics ${LOGICS}. This may take some time."
106 ./build -b -i "${LOGICS}" || die "building logics failed"
107 ./bin/isabelle makeall || die "isabelle makeall failed"
108 if use graphbrowsing
109 then
110 rm -f "${S}/lib/browser/GraphBrowser.jar" \
111 || die "failed cleaning graph browser directory"
112 pushd "${S}/lib/browser" \
113 || die "Could not change directory to lib/browser"
114 ./build || die "failed building the graph browser"
115 popd
116 fi
117 }
118
119 src_test() {
120 einfo "Running tests. A test run can take up to several hours!"
121 ./build -b -t || die "tests failed"
122 }
123
124 src_install() {
125 exeinto ${TARGETDIR}/bin
126 doexe bin/isabelle-process bin/isabelle
127
128 insinto ${TARGETDIR}
129 doins -r src
130 doins -r lib
131
132 for i in "./build" \
133 "src/Pure/mk" \
134 "src/Pure/build-jars" \
135 "src/Tools/jEdit/dist/build-support/ci/copy_properties.groovy" \
136 "src/Tools/jEdit/dist/build-support/ci/ci_release.groovy" \
137 "src/Tools/jEdit/lib/Tools/jedit" \
138 "src/Tools/Metis/fix_metis_license" \
139 "src/Tools/Metis/make_metis" \
140 "src/Tools/Metis/scripts/mlpp" \
141 "src/Tools/WWW_Find/lib/Tools/wwwfind" \
142 "src/Tools/Code/lib/Tools/codegen" \
143 "src/HOL/Mirabelle/lib/Tools/mirabelle" \
144 "src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \
145 "src/HOL/Tools/SMT/lib/scripts/remote_smt" \
146 "src/HOL/Tools/ATP/scripts/remote_atp" \
147 "src/HOL/Tools/ATP/scripts/spass" \
148 "src/HOL/Tools/Nitpick/lib/Tools/nitrox" \
149 "src/HOL/Mutabelle/lib/Tools/mutabelle" \
150 "src/HOL/Library/Sum_of_Squares/neos_csdp_client" \
151 "lib/browser/build" \
152 "lib/Tools/tty" \
153 "lib/Tools/mkproject" \
154 "lib/Tools/keywords" \
155 "lib/Tools/browser" \
156 "lib/Tools/install" \
157 "lib/Tools/mkdir" \
158 "lib/Tools/unsymbolize" \
159 "lib/Tools/getenv" \
160 "lib/Tools/java" \
161 "lib/Tools/make" \
162 "lib/Tools/emacs" \
163 "lib/Tools/scala" \
164 "lib/Tools/print" \
165 "lib/Tools/latex" \
166 "lib/Tools/findlogics" \
167 "lib/Tools/doc" \
168 "lib/Tools/logo" \
169 "lib/Tools/usedir" \
170 "lib/Tools/yxml" \
171 "lib/Tools/version" \
172 "lib/Tools/makeall" \
173 "lib/Tools/scalac" \
174 "lib/Tools/document" \
175 "lib/Tools/env" \
176 "lib/Tools/display" \
177 "lib/Tools/dimacs2hol" \
178 "lib/scripts/keywords" \
179 "lib/scripts/unsymbolize" \
180 "lib/scripts/run-polyml" \
181 "lib/scripts/run-smlnj" \
182 "lib/scripts/feeder" \
183 "lib/scripts/java_ext_dirs" \
184 "lib/scripts/yxml" \
185 "lib/scripts/raw_dump" \
186 "lib/scripts/polyml-version" \
187 "lib/scripts/process"
188 do
189 exeinto $(dirname "${TARGETDIR}/${i}")
190 doexe ${i}
191 done
192
193 docompress -x /usr/share/doc/${PF}
194 dodoc -r doc
195 if use doc; then
196 dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc"
197 fi
198
199 dodir /etc/isabelle
200 insinto /etc/isabelle
201 doins -r etc/*
202
203 dosym /etc/isabelle "${TARGETDIR}/etc"
204 dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
205
206 insinto ${LIBDIR}
207 doins -r heaps
208
209 bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \
210 || die "isabelle install failed"
211 newicon lib/icons/isabelle.xpm "${PN}.xpm"
212 dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README
213
214 java-pkg_regjar \
215 "${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \
216 "${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \
217 "${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \
218 "${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \
219 "${ED}${TARGETDIR}/lib/classes/java_ext_dirs.jar"
220 }
221
222 pkg_postinst() {
223 # If any of the directories in /etc/isabelle/components do not exist, then
224 # even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to
225 # to delete any non-existing directories. If an old Isabelle version was
226 # installed with component ebuilds like sci-mathematics/e, then the
227 # Isabelle version is upgraded, then the contrib directories will not
228 # exist initially, it is necessary to delete them from /etc/isabelle/components.
229 # Then these components are rebuilt (creating these directories) using the
230 # EAPI=5 subslot depends.
231 for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components")
232 do
233 if [ ! -d /usr/share/Isabelle2012/${i} ]; then
234 sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components"
235 fi
236 done
237 if use ledit && use readline; then
238 elog "Both readline and ledit use flags specified. The default setting"
239 elog "if both are installed is to use readline (rlwrap), this can be"
240 elog "modfied by editing the ISABELLE_LINE_EDITOR setting in"
241 elog "${ROOT}/etc/isabelle/settings"
242 fi
243 elog "Please ensure you have a pdf viewer installed, for example:"
244 elog "As root: emerge app-text/zathura-pdf-poppler"
245 elog "Please configure your preferred pdf viewer, something like:"
246 elog "As normal user: xdg-mime default zathura.desktop application/pdf"
247 elog "Or alternatively by editing the PDF_VIEWER variable in the system"
248 elog "settings file ${ROOT}etc/isabelle/settings and/or the user"
249 elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings"
250 elog "To improve sledgehammer performance, consider installing:"
251 elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass"
252 elog "For nitpick it is necessary to install:"
253 elog "emerge sci-mathematics/kodkodi"
254 }

  ViewVC Help
Powered by ViewVC 1.1.20