1 |
commit: 7d2aafd09b8f128da73333201c48b793607077be |
2 |
Author: Michał Górny <mgorny <AT> gentoo <DOT> org> |
3 |
AuthorDate: Sat Sep 14 15:44:37 2019 +0000 |
4 |
Commit: Michał Górny <mgorny <AT> gentoo <DOT> org> |
5 |
CommitDate: Sat Sep 14 15:44:37 2019 +0000 |
6 |
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=7d2aafd0 |
7 |
|
8 |
sci-mathematics/isabelle: Remove last-rited pkg |
9 |
|
10 |
Signed-off-by: Michał Górny <mgorny <AT> gentoo.org> |
11 |
|
12 |
profiles/package.mask | 1 - |
13 |
sci-mathematics/isabelle/Manifest | 10 - |
14 |
.../files/isabelle-2012-graphbrowser.patch | 11 - |
15 |
.../isabelle-2012-reverse-line-editor-order.patch | 12 - |
16 |
.../isabelle/files/isabelle-2016-classpath.patch | 32 -- |
17 |
.../files/isabelle-2016-jfreechart-classpath.patch | 16 - |
18 |
...abelle-2016.1-bash_process-1.2.1-settings.patch | 7 - |
19 |
...-2016.1-disable-jedit-build-after-install.patch | 128 -------- |
20 |
.../isabelle-2016.1-jortho-1.0-2-classpath.patch | 8 - |
21 |
.../isabelle/files/isabelle-2016.1-libsha1.patch | 11 - |
22 |
...sabelle-2016.1-smt_read_only_certificates.patch | 33 --- |
23 |
.../files/isabelle-2016.1-smt_timeout.patch | 22 -- |
24 |
sci-mathematics/isabelle/isabelle-2016.1.ebuild | 328 --------------------- |
25 |
sci-mathematics/isabelle/metadata.xml | 29 -- |
26 |
14 files changed, 648 deletions(-) |
27 |
|
28 |
diff --git a/profiles/package.mask b/profiles/package.mask |
29 |
index feef25289e3..1eaa755ace9 100644 |
30 |
--- a/profiles/package.mask |
31 |
+++ b/profiles/package.mask |
32 |
@@ -1116,7 +1116,6 @@ dev-java/itext |
33 |
app-text/jpdftweak |
34 |
dev-util/deskzilla |
35 |
media-sound/tuxguitar |
36 |
-sci-mathematics/isabelle |
37 |
|
38 |
# Michał Górny <mgorny@g.o> (2019-08-14) |
39 |
# No longer builds. Homepage is gone, and its keep-alive fork is also |
40 |
|
41 |
diff --git a/sci-mathematics/isabelle/Manifest b/sci-mathematics/isabelle/Manifest |
42 |
deleted file mode 100644 |
43 |
index b5aab891dc5..00000000000 |
44 |
--- a/sci-mathematics/isabelle/Manifest |
45 |
+++ /dev/null |
46 |
@@ -1,10 +0,0 @@ |
47 |
-DIST Isabelle2016-1.tar.gz 39567637 BLAKE2B a664c89f2705e6b2709a8b3054d57ca443435967dd85f07e1651aa0bbfc41ee31dee88146243c8e0bddc2a1de86107158a89d13b2ff427f8dcf0308fe3dd2654 SHA512 c7da7900033a8c816f002b8899e398da7819dc457b3b1176dc9a19adffeb42d5524f2d14581a391487da1f36ffeabd0867bacab6462f3decfc0f7a9caf81a2d2 |
48 |
-DIST bash_process-isabelle-component-1.2.1.tar.gz 33182 BLAKE2B d139f5476b02b22a896fa742303a4e5c4de583972eb38a67e1a451fabe28d52c2c1310be865faf244104cad46758e1bf97f6222170999ff2e2da7c07e1398fe3 SHA512 d9817191af5660e38f1647401803115a93f0052291bfbbcb1cd9b41a4bab89b3ebdde22b40744a04ad3268aed8ca037ae59981c513f71b3ff6d89855d29e14c3 |
49 |
-DIST csdp-isabelle-component-6.x.tar.gz 493 BLAKE2B 364c8f390adfb4031958597e4435783e58ebbb3be49ee80d5ee6631770d9322190bd364530622ae66d490d91e499bb3bb626b01762fccf3f67c65b20b3f7756b SHA512 9be28ecbf61d0f6ad23e28d44bd7ceb8f06ab22f3a05a7c823a9c5bf52ddcf5e5c300c41e14451d6b8e6a4c32b1bbd17769c731cd890fab335a866cd5e735290 |
50 |
-DIST isabelle_fonts-isabelle-component-20160830.tar.gz 249427 BLAKE2B 8398e578e6b8f54ac163b33e29c8283fef29c5db2cd8562dca1d636e1947bebb54e79e55035398fca215f2fbdf868dfe318d91a7f76074ad97f2d4792b8b4432 SHA512 a185f79990478861832e9400ea37ffd02f582d3f916d26d901b8b0ec923027c412538bafe4a763a132adb9277a4b00a7a510762928ec49433ef550ae3fe59dbc |
51 |
-DIST jedit_build-isabelle-component-20161024.tar.gz 10819946 BLAKE2B 2764d854eecd6783a0893934742f21db9ac47b1304f969803e01ffc402d57d2f3d38c9f07cb6ea6d77f12a48337892baecc7175b1d759989d7c46d0104b34a9f SHA512 0563b696307dd33b244e4ecc62664056a2b003c3291a5e3d7dd4f1c936dac2c3257ff90273cb2c8dc3bf9dea40fae745fabb57fc5f4ed420d0c8fd7d2b917433 |
52 |
-DIST jfreechart-isabelle-component-1.0.14-1.tar.gz 3444825 BLAKE2B 4a24f362d647c9bbe538d18a49f7579cf9c1914854b19c7f4cca29d876870eb5f994df4b53ae2bf6f8bf8aa697306bfebdb272493fb974c6df8050778d173376 SHA512 ee1d84a45e43029d5e3acee823176196da19789322e8d3c2c81d5504930ad81d50e16e5da87655e4151034901daefb4ce6b82334839e39134b3a7ce32203aa67 |
53 |
-DIST jortho-isabelle-component-1.0-2.tar.gz 1723761 BLAKE2B 4f5503c640d25d79a8520a2f137900a8397db141f5f6279e4622bf44c377a3bcd7224d9e59de2f57993867362350bc279aebc54dc548562bab6b78b210110fb7 SHA512 8bef5e025d13b76c86a727bf93887b846cc906b2ce00299c38f69ccf33fb9dc7411e55b6fd1c56ed993c180d83a7e9ed90122f7feb6ae4fb70df93802ac21211 |
54 |
-DIST polyml-isabelle-component-5.6-1.tar.gz 822 BLAKE2B eea808d3cd2ce2c6b5b531fce046eba59e39f671e48e76e3d9093a4d9fadef9fbf3afc20b98eeaf5e672e8e34ed11aaf62441266469f53d3d228252fe9f64f89 SHA512 403239aa48aab8c39e12cd5f82cb5e3ba7c31f9325d88f5137d3ec509bb25ab4eb8b1103a66b8ea5ad45c7c968ef092749c486217528a5db4223819106c00a59 |
55 |
-DIST ssh-java-isabelle-component-20161009.tar.gz 412919 BLAKE2B d05152d92669043ba23d7e0767470a529ac7688866ed8be64432d724329a0c24590586faf5e09c365c44740550441798681b9e8b80a323285516ec61a884beb8 SHA512 685a9b8791046c1bc21aa77614fb1b304e7438715377e179954ebfd1603434ff66fe23e90de928a5af6f51a48ae6ea6f05f9ff8941d98f7c3a43fdda02d3b519 |
56 |
-DIST xz-java-isabelle-component-1.5.tar.gz 315 BLAKE2B b7a385671469fb8643d74d90b4faae2f66621f7bafb0262b7fc7777c883cae4a5939cb5261230c21a6125ce12cafe5285a873fc0a37f78ef0e4059d310c2bd0e SHA512 6dfec49e12c4cafbb6b6386dd54477e86b6bb419a77c52d9606a0305aeea9cd11f087ed6bba77352c7bf9ec656052ef617e845f472e57b5cdfbccf22b2eeb4fa |
57 |
|
58 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch b/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch |
59 |
deleted file mode 100644 |
60 |
index 3e63f1c6223..00000000000 |
61 |
--- a/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch |
62 |
+++ /dev/null |
63 |
@@ -1,11 +0,0 @@ |
64 |
---- Isabelle2012-orig/lib/browser/build 2012-05-20 19:34:33.000000000 +1000 |
65 |
-+++ Isabelle2012/lib/browser/build 2012-05-26 22:18:41.952750622 +1000 |
66 |
-@@ -6,6 +6,8 @@ |
67 |
- # |
68 |
- # Requires proper Isabelle settings environment. |
69 |
- |
70 |
-+ISABELLE_HOME="$(cd "$(dirname "${0}")/../.."; pwd -P)" |
71 |
-+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 |
72 |
- |
73 |
- ## diagnostics |
74 |
- |
75 |
|
76 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch b/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch |
77 |
deleted file mode 100644 |
78 |
index 233ea5b50fa..00000000000 |
79 |
--- a/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch |
80 |
+++ /dev/null |
81 |
@@ -1,12 +0,0 @@ |
82 |
---- Isabelle2012-orig/etc/settings 2012-05-23 03:07:38.000000000 +1000 |
83 |
-+++ Isabelle2012/etc/settings 2012-05-27 12:43:36.209715015 +1000 |
84 |
-@@ -62,8 +62,8 @@ |
85 |
- ### |
86 |
- |
87 |
- ISABELLE_LINE_EDITOR="" |
88 |
--[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" |
89 |
- [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)" |
90 |
-+[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" |
91 |
- |
92 |
- |
93 |
- ### |
94 |
|
95 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2016-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2016-classpath.patch |
96 |
deleted file mode 100644 |
97 |
index 032b18b71f3..00000000000 |
98 |
--- a/sci-mathematics/isabelle/files/isabelle-2016-classpath.patch |
99 |
+++ /dev/null |
100 |
@@ -1,32 +0,0 @@ |
101 |
-Index: Isabelle2016/lib/Tools/java |
102 |
-=================================================================== |
103 |
---- Isabelle2016.orig/lib/Tools/java |
104 |
-+++ Isabelle2016/lib/Tools/java |
105 |
-@@ -10,5 +10,5 @@ declare -a JAVA_ARGS; eval "JAVA_ARGS=($ |
106 |
- unset CLASSPATH |
107 |
- |
108 |
- isabelle_java java "${JAVA_ARGS[@]}" \ |
109 |
-- -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@" |
110 |
-+ -classpath "$(platform_path "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11)")" "$@" |
111 |
- |
112 |
-Index: Isabelle2016/lib/Tools/scala |
113 |
-=================================================================== |
114 |
---- Isabelle2016.orig/lib/Tools/scala |
115 |
-+++ Isabelle2016/lib/Tools/scala |
116 |
-@@ -14,4 +14,4 @@ do |
117 |
- done |
118 |
- |
119 |
- isabelle_scala scala "${SCALA_ARGS[@]}" \ |
120 |
-- -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@" |
121 |
-+ -classpath "$(platform_path "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11)")" "$@" |
122 |
-Index: Isabelle2016/lib/Tools/scalac |
123 |
-=================================================================== |
124 |
---- Isabelle2016.orig/lib/Tools/scalac |
125 |
-+++ Isabelle2016/lib/Tools/scalac |
126 |
-@@ -7,5 +7,5 @@ |
127 |
- isabelle_admin_build jars || exit $? |
128 |
- |
129 |
- isabelle_scala scalac -Dfile.encoding=UTF-8 \ |
130 |
-- -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@" |
131 |
-+ -classpath "$(platform_path "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11)")" "$@" |
132 |
- |
133 |
|
134 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2016-jfreechart-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2016-jfreechart-classpath.patch |
135 |
deleted file mode 100644 |
136 |
index 9a88ebef26c..00000000000 |
137 |
--- a/sci-mathematics/isabelle/files/isabelle-2016-jfreechart-classpath.patch |
138 |
+++ /dev/null |
139 |
@@ -1,16 +0,0 @@ |
140 |
---- Isabelle2016-orig/contrib/jfreechart-1.0.14-1/etc/settings 2013-09-12 07:46:57.000000000 +1000 |
141 |
-+++ Isabelle2016/contrib/jfreechart-1.0.14-1/etc/settings 2016-07-07 17:22:55.716464804 +1000 |
142 |
-@@ -1,9 +1,8 @@ |
143 |
- # -*- shell-script -*- :mode=shellscript: |
144 |
- |
145 |
- JFREECHART_HOME="$COMPONENT" |
146 |
--JFREECHART_JAR_NAMES="iText-2.1.5.jar jcommon-1.0.18.jar jfreechart-1.0.14.jar" |
147 |
-- |
148 |
--classpath "$JFREECHART_HOME/lib/iText-2.1.5.jar" |
149 |
--classpath "$JFREECHART_HOME/lib/jcommon-1.0.18.jar" |
150 |
--classpath "$JFREECHART_HOME/lib/jfreechart-1.0.14.jar" |
151 |
-+JFREECHART_JAR_NAMES="$(java-config --classpath itext | sed -e 's@:@ @g' -e 's@/[^ ]*/@@g') $(java-config --classpath jcommon-1.0 | sed -e 's@:@ @g' -e 's@/[^ ]*/@@g') $(java-config --classpath jfreechart-1.0 | sed -e 's@:@ @g' -e 's@/[^ ]*/@@g')" |
152 |
- |
153 |
-+classpath "$(java-config --classpath itext)" |
154 |
-+classpath "$(java-config --classpath jcommon-1.0)" |
155 |
-+classpath "$(java-config --classpath jfreechart-1.0)" |
156 |
|
157 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-bash_process-1.2.1-settings.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-bash_process-1.2.1-settings.patch |
158 |
deleted file mode 100644 |
159 |
index 38d047199ce..00000000000 |
160 |
--- a/sci-mathematics/isabelle/files/isabelle-2016.1-bash_process-1.2.1-settings.patch |
161 |
+++ /dev/null |
162 |
@@ -1,7 +0,0 @@ |
163 |
---- Isabelle2016-1-orig/contrib/bash_process-1.2.1/etc/settings 2016-02-14 09:48:03.000000000 +1100 |
164 |
-+++ Isabelle2016-1/contrib/bash_process-1.2.1/etc/settings 2017-01-02 13:44:49.355549312 +1100 |
165 |
-@@ -1,3 +1,3 @@ |
166 |
- # -*- shell-script -*- :mode=shellscript: |
167 |
- |
168 |
--ISABELLE_BASH_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bash_process" |
169 |
-+ISABELLE_BASH_PROCESS="$COMPONENT/bash_process" |
170 |
|
171 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-disable-jedit-build-after-install.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-disable-jedit-build-after-install.patch |
172 |
deleted file mode 100644 |
173 |
index 6bac5ccbe74..00000000000 |
174 |
--- a/sci-mathematics/isabelle/files/isabelle-2016.1-disable-jedit-build-after-install.patch |
175 |
+++ /dev/null |
176 |
@@ -1,128 +0,0 @@ |
177 |
---- Isabelle2016-1-orig/src/Tools/jEdit/lib/Tools/jedit 2016-12-13 01:03:49.000000000 +1100 |
178 |
-+++ Isabelle2016-1/src/Tools/jEdit/lib/Tools/jedit 2017-01-01 17:24:50.107722845 +1100 |
179 |
-@@ -239,125 +239,6 @@ |
180 |
- "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar" |
181 |
- ) |
182 |
- |
183 |
-- |
184 |
--# target |
185 |
-- |
186 |
--TARGET="dist/jars/Isabelle-jEdit.jar" |
187 |
-- |
188 |
--declare -a UPDATED=() |
189 |
-- |
190 |
--if [ "$BUILD_JARS" = jars_fresh ]; then |
191 |
-- OUTDATED=true |
192 |
--else |
193 |
-- OUTDATED=false |
194 |
-- if [ ! -e "$TARGET" ]; then |
195 |
-- OUTDATED=true |
196 |
-- else |
197 |
-- if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then |
198 |
-- declare -a DEPS=( |
199 |
-- "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" |
200 |
-- "${SOURCES[@]}" "${RESOURCES[@]}" |
201 |
-- ) |
202 |
-- elif [ -e "$ISABELLE_HOME/Admin/build" ]; then |
203 |
-- declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}") |
204 |
-- else |
205 |
-- declare -a DEPS=() |
206 |
-- fi |
207 |
-- for DEP in "${DEPS[@]}" |
208 |
-- do |
209 |
-- [ ! -e "$DEP" ] && fail "Missing file: $DEP" |
210 |
-- [ "$DEP" -nt "$TARGET" ] && { |
211 |
-- OUTDATED=true |
212 |
-- UPDATED["${#UPDATED[@]}"]="$DEP" |
213 |
-- } |
214 |
-- done |
215 |
-- fi |
216 |
--fi |
217 |
-- |
218 |
-- |
219 |
--# build |
220 |
-- |
221 |
--if [ "$OUTDATED" = true ] |
222 |
--then |
223 |
-- echo "### Building Isabelle/jEdit ..." |
224 |
-- |
225 |
-- [ "${#UPDATED[@]}" -gt 0 ] && { |
226 |
-- echo "Changed files:" |
227 |
-- for FILE in "${UPDATED[@]}" |
228 |
-- do |
229 |
-- echo " $FILE" |
230 |
-- done |
231 |
-- } |
232 |
-- |
233 |
-- [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \ |
234 |
-- fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component" |
235 |
-- |
236 |
-- rm -rf dist || failed |
237 |
-- mkdir -p dist dist/classes || failed |
238 |
-- |
239 |
-- cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/. |
240 |
-- cp -p -R -f "${RESOURCES[@]}" dist/classes/. |
241 |
-- cp src/jEdit.props dist/properties/. |
242 |
-- cp -p -R -f src/modes/. dist/modes/. |
243 |
-- |
244 |
-- perl -i -e 'while (<>) { |
245 |
-- if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/) { } |
246 |
-- elsif (m/NAME="javacc"/) { |
247 |
-- print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>\n\n!; |
248 |
-- print qq!<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n!; |
249 |
-- print qq!<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n!; |
250 |
-- print qq!<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n!; |
251 |
-- print qq!<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n!; |
252 |
-- print; |
253 |
-- } |
254 |
-- elsif (m/NAME="sqr"/) { |
255 |
-- print qq!<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>\n\n!; |
256 |
-- print; |
257 |
-- } |
258 |
-- else { print; } |
259 |
-- }' dist/modes/catalog |
260 |
-- |
261 |
-- cd dist |
262 |
-- isabelle_jdk jar xf jedit.jar |
263 |
-- cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \ |
264 |
-- "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed |
265 |
-- cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \ |
266 |
-- "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed |
267 |
-- isabelle_jdk jar cfe jedit.jar org.gjt.sp.jedit.jEdit org || failed |
268 |
-- rm -rf META-INF org |
269 |
-- cd .. |
270 |
-- |
271 |
-- cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed |
272 |
-- ( |
273 |
-- #FIXME workarounds for scalac 2.11.0 |
274 |
-- export CYGWIN="nodosfilewarning" |
275 |
-- function stty() { :; } |
276 |
-- export -f stty |
277 |
-- |
278 |
-- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" |
279 |
-- do |
280 |
-- classpath "$JAR" |
281 |
-- done |
282 |
-- export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" |
283 |
-- exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}" |
284 |
-- ) || fail "Failed to compile sources" |
285 |
-- |
286 |
-- cd dist/classes |
287 |
-- isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed |
288 |
-- cd ../.. |
289 |
-- rm -rf dist/classes |
290 |
-- |
291 |
-- cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.3.0manual-a4.pdf" dist/doc/jedit-manual.pdf |
292 |
-- cp dist/doc/CHANGES.txt dist/doc/jedit-changes |
293 |
-- cat > dist/doc/Contents <<EOF |
294 |
--Original jEdit Documentation |
295 |
-- jedit-manual jEdit 5.3 User's Guide |
296 |
-- jedit-changes jEdit 5.3 Version History |
297 |
-- |
298 |
--EOF |
299 |
-- |
300 |
--fi |
301 |
-- |
302 |
- popd >/dev/null |
303 |
- |
304 |
- |
305 |
|
306 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-jortho-1.0-2-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-jortho-1.0-2-classpath.patch |
307 |
deleted file mode 100644 |
308 |
index a34cae3fcf4..00000000000 |
309 |
--- a/sci-mathematics/isabelle/files/isabelle-2016.1-jortho-1.0-2-classpath.patch |
310 |
+++ /dev/null |
311 |
@@ -1,8 +0,0 @@ |
312 |
---- Isabelle2016-1-orig/contrib/jortho-1.0-2/etc/settings 2014-04-16 06:03:34.000000000 +1000 |
313 |
-+++ Isabelle2016-1/contrib/jortho-1.0-2/etc/settings 2017-01-02 00:13:01.619790577 +1100 |
314 |
-@@ -3,4 +3,4 @@ |
315 |
- JORTHO_HOME="$COMPONENT" |
316 |
- JORTHO_DICTIONARIES="$JORTHO_HOME/dictionaries/en.gz:$JORTHO_HOME/dictionaries/en_US.gz:$JORTHO_HOME/dictionaries/en_GB-ise.gz:$JORTHO_HOME/dictionaries/en_GB-ize.gz:$JORTHO_HOME/dictionaries/en_CA.gz" |
317 |
- |
318 |
--classpath "$JORTHO_HOME/jortho.jar" |
319 |
-+classpath "$(java-config -p jortho)" |
320 |
|
321 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-libsha1.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-libsha1.patch |
322 |
deleted file mode 100644 |
323 |
index f19436acd1c..00000000000 |
324 |
--- a/sci-mathematics/isabelle/files/isabelle-2016.1-libsha1.patch |
325 |
+++ /dev/null |
326 |
@@ -1,11 +0,0 @@ |
327 |
---- Isabelle2016-1-orig/src/Pure/General/sha1.ML 2016-12-13 01:03:45.000000000 +1100 |
328 |
-+++ Isabelle2016-1/src/Pure/General/sha1.ML 2016-12-28 20:50:36.814706587 +1100 |
329 |
-@@ -146,7 +146,7 @@ |
330 |
- (* C library and memory *) |
331 |
- |
332 |
- val library_path = |
333 |
-- Path.explode ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so")); |
334 |
-+ Path.explode ("$SHA1_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so")); |
335 |
- |
336 |
- fun with_memory n = |
337 |
- Thread_Attributes.uninterruptible (fn restore_attributes => fn f => |
338 |
|
339 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-smt_read_only_certificates.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-smt_read_only_certificates.patch |
340 |
deleted file mode 100644 |
341 |
index d766a957021..00000000000 |
342 |
--- a/sci-mathematics/isabelle/files/isabelle-2016.1-smt_read_only_certificates.patch |
343 |
+++ /dev/null |
344 |
@@ -1,33 +0,0 @@ |
345 |
---- Isabelle2016-1-orig/src/HOL/SMT_Examples/Boogie.thy 2016-12-13 01:03:38.000000000 +1100 |
346 |
-+++ Isabelle2016-1/src/HOL/SMT_Examples/Boogie.thy 2016-12-30 23:46:11.947737290 +1100 |
347 |
-@@ -52,7 +52,7 @@ |
348 |
- section \<open>Verification condition proofs\<close> |
349 |
- |
350 |
- declare [[smt_oracle = false]] |
351 |
--declare [[smt_read_only_certificates = true]] |
352 |
-+declare [[smt_read_only_certificates = false]] |
353 |
- |
354 |
- |
355 |
- declare [[smt_certificates = "Boogie_Max.certs"]] |
356 |
---- Isabelle2016-1-orig/src/HOL/SMT_Examples/SMT_Examples.thy 2016-12-13 01:03:38.000000000 +1100 |
357 |
-+++ Isabelle2016-1/src/HOL/SMT_Examples/SMT_Examples.thy 2016-12-30 23:46:11.953737338 +1100 |
358 |
-@@ -9,7 +9,7 @@ |
359 |
- begin |
360 |
- |
361 |
- declare [[smt_certificates = "SMT_Examples.certs"]] |
362 |
--declare [[smt_read_only_certificates = true]] |
363 |
-+declare [[smt_read_only_certificates = false]] |
364 |
- |
365 |
- |
366 |
- section \<open>Propositional and first-order logic\<close> |
367 |
---- Isabelle2016-1-orig/src/HOL/SMT_Examples/SMT_Word_Examples.thy 2016-12-13 01:03:38.000000000 +1100 |
368 |
-+++ Isabelle2016-1/src/HOL/SMT_Examples/SMT_Word_Examples.thy 2016-12-30 23:46:11.967737450 +1100 |
369 |
-@@ -11,7 +11,7 @@ |
370 |
- declare [[smt_oracle = true]] |
371 |
- declare [[z3_extensions = true]] |
372 |
- declare [[smt_certificates = "SMT_Word_Examples.certs"]] |
373 |
--declare [[smt_read_only_certificates = true]] |
374 |
-+declare [[smt_read_only_certificates = false]] |
375 |
- |
376 |
- text \<open> |
377 |
- Currently, there is no proof reconstruction for words. |
378 |
|
379 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-smt_timeout.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-smt_timeout.patch |
380 |
deleted file mode 100644 |
381 |
index 249c94bd258..00000000000 |
382 |
--- a/sci-mathematics/isabelle/files/isabelle-2016.1-smt_timeout.patch |
383 |
+++ /dev/null |
384 |
@@ -1,22 +0,0 @@ |
385 |
---- Isabelle2016-1-orig/src/HOL/SMT.thy 2016-12-13 01:03:38.000000000 +1100 |
386 |
-+++ Isabelle2016-1/src/HOL/SMT.thy 2016-12-30 14:11:09.379863215 +1100 |
387 |
-@@ -201,7 +201,7 @@ |
388 |
- (given in seconds) to restrict their runtime. |
389 |
- \<close> |
390 |
- |
391 |
--declare [[smt_timeout = 20]] |
392 |
-+declare [[smt_timeout = 300]] |
393 |
- |
394 |
- text \<open> |
395 |
- SMT solvers apply randomized heuristics. In case a problem is not |
396 |
---- Isabelle2016-1-orig/src/HOL/Tools/SMT/smt_config.ML 2016-12-13 01:03:42.000000000 +1100 |
397 |
-+++ Isabelle2016-1/src/HOL/Tools/SMT/smt_config.ML 2016-12-30 14:11:27.186904132 +1100 |
398 |
-@@ -170,7 +170,7 @@ |
399 |
- (* options *) |
400 |
- |
401 |
- val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true) |
402 |
--val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0) |
403 |
-+val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 300.0) |
404 |
- val reconstruction_step_timeout = Attrib.setup_config_real @{binding smt_reconstruction_step_timeout} (K 10.0) |
405 |
- val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1) |
406 |
- val read_only_certificates = Attrib.setup_config_bool @{binding smt_read_only_certificates} (K false) |
407 |
|
408 |
diff --git a/sci-mathematics/isabelle/isabelle-2016.1.ebuild b/sci-mathematics/isabelle/isabelle-2016.1.ebuild |
409 |
deleted file mode 100644 |
410 |
index 3e67fa95fbf..00000000000 |
411 |
--- a/sci-mathematics/isabelle/isabelle-2016.1.ebuild |
412 |
+++ /dev/null |
413 |
@@ -1,328 +0,0 @@ |
414 |
-# Copyright 1999-2018 Gentoo Authors |
415 |
-# Distributed under the terms of the GNU General Public License v2 |
416 |
- |
417 |
-EAPI="6" |
418 |
- |
419 |
-inherit eutils check-reqs java-pkg-2 versionator |
420 |
- |
421 |
-MY_PN="Isabelle" |
422 |
-MY_PV=$(replace_all_version_separators '-') |
423 |
-MY_P="${MY_PN}${MY_PV}" |
424 |
- |
425 |
-BP_PV="1.2.1" |
426 |
-BP_PN="bash_process" |
427 |
-BP_P="${BP_PN}-${BP_PV}" |
428 |
-BP_IC_PN="${BP_PN}-isabelle-component" |
429 |
-BP_IC_P="${BP_IC_PN}-${BP_PV}" |
430 |
- |
431 |
-# csdp is used in the compile of HOL_ex in |
432 |
-# Library/Sum_of_Squares/sos_wrapper.ML where it execs $ISABELLE_CSDP |
433 |
-CSDP_PV="6.x" |
434 |
-CSDP_PN="csdp" |
435 |
-CSDP_P="${CSDP_PN}-${CSDP_PV}" |
436 |
-CSDP_IC_PN="${CSDP_PN}-isabelle-component" |
437 |
-CSDP_IC_P="${CSDP_IC_PN}-${CSDP_PV}" |
438 |
- |
439 |
-ISABELLE_FONTS_PV="20160830" |
440 |
-ISABELLE_FONTS_PN="isabelle_fonts" |
441 |
-ISABELLE_FONTS_P="${ISABELLE_FONTS_PN}-${ISABELLE_FONTS_PV}" |
442 |
-ISABELLE_FONTS_IC_PN="${ISABELLE_FONTS_PN}-isabelle-component" |
443 |
-ISABELLE_FONTS_IC_P="${ISABELLE_FONTS_IC_PN}-${ISABELLE_FONTS_PV}" |
444 |
- |
445 |
-JEDIT_PV="20161024" |
446 |
-JEDIT_PN="jedit_build" |
447 |
-JEDIT_P="${JEDIT_PN}-${JEDIT_PV}" |
448 |
-JEDIT_IC_PN="${JEDIT_PN}-isabelle-component" |
449 |
-JEDIT_IC_P="${JEDIT_IC_PN}-${JEDIT_PV}" |
450 |
- |
451 |
-JORTHO_PV="1.0-2" |
452 |
-JORTHO_PN="jortho" |
453 |
-JORTHO_P="${JORTHO_PN}-${JORTHO_PV}" |
454 |
-JORTHO_IC_PN="${JORTHO_PN}-isabelle-component" |
455 |
-JORTHO_IC_P="${JORTHO_IC_PN}-${JORTHO_PV}" |
456 |
- |
457 |
-JFREECHART_PV="1.0.14-1" |
458 |
-JFREECHART_PN="jfreechart" |
459 |
-JFREECHART_P="${JFREECHART_PN}-${JFREECHART_PV}" |
460 |
-JFREECHART_IC_PN="${JFREECHART_PN}-isabelle-component" |
461 |
-JFREECHART_IC_P="${JFREECHART_IC_PN}-${JFREECHART_PV}" |
462 |
- |
463 |
-POLYML_PV="5.6-1" |
464 |
-POLYML_PN="polyml" |
465 |
-POLYML_P="${POLYML_PN}-${POLYML_PV}" |
466 |
-POLYML_IC_PN="${POLYML_PN}-isabelle-component" |
467 |
-POLYML_IC_P="${POLYML_IC_PN}-${POLYML_PV}" |
468 |
- |
469 |
-SSH_JAVA_PV="20161009" |
470 |
-SSH_JAVA_PN="ssh-java" |
471 |
-SSH_JAVA_P="${SSH_JAVA_PN}-${SSH_JAVA_PV}" |
472 |
-SSH_JAVA_IC_PN="${SSH_JAVA_PN}-isabelle-component" |
473 |
-SSH_JAVA_IC_P="${SSH_JAVA_IC_PN}-${SSH_JAVA_PV}" |
474 |
- |
475 |
-XZ_JAVA_PV="1.5" |
476 |
-XZ_JAVA_PN="xz-java" |
477 |
-XZ_JAVA_P="${XZ_JAVA_PN}-${XZ_JAVA_PV}" |
478 |
-XZ_JAVA_IC_PN="${XZ_JAVA_PN}-isabelle-component" |
479 |
-XZ_JAVA_IC_P="${XZ_JAVA_IC_PN}-${XZ_JAVA_PV}" |
480 |
- |
481 |
-SS="2.12" |
482 |
- |
483 |
-DESCRIPTION="Isabelle is a generic proof assistant" |
484 |
-HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html" |
485 |
-SRC_URI="http://isabelle.in.tum.de/website-${MY_P}/dist/${MY_P}.tar.gz |
486 |
- http://isabelle.in.tum.de/dist/contrib/${BP_P}.tar.gz -> ${BP_IC_P}.tar.gz |
487 |
- https://dev.gentoo.org/~gienah/snapshots/${CSDP_IC_P}.tar.gz |
488 |
- http://isabelle.in.tum.de/dist/contrib/${ISABELLE_FONTS_P}.tar.gz -> ${ISABELLE_FONTS_IC_P}.tar.gz |
489 |
- http://isabelle.in.tum.de/components/${JORTHO_P}.tar.gz -> ${JORTHO_IC_P}.tar.gz |
490 |
- http://isabelle.in.tum.de/components/${JEDIT_P}.tar.gz -> ${JEDIT_IC_P}.tar.gz |
491 |
- http://isabelle.in.tum.de/dist/contrib/${JFREECHART_P}.tar.gz -> ${JFREECHART_IC_P}.tar.gz |
492 |
- https://dev.gentoo.org/~gienah/snapshots/${POLYML_IC_P}.tar.gz |
493 |
- http://isabelle.in.tum.de/dist/contrib/${SSH_JAVA_P}.tar.gz -> ${SSH_JAVA_IC_P}.tar.gz |
494 |
- https://dev.gentoo.org/~gienah/snapshots/${XZ_JAVA_IC_P}.tar.gz" |
495 |
- |
496 |
-LICENSE="BSD" |
497 |
-SLOT="0/${PV}" |
498 |
-KEYWORDS="~amd64 ~x86" |
499 |
-IUSE="doc graphbrowsing ledit readline" |
500 |
- |
501 |
-#upstream says |
502 |
-#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, |
503 |
-#for document preparation: complete LaTeX |
504 |
-DEPEND=">=app-shells/bash-3.0:* |
505 |
- >=dev-java/jcommon-1.0.18:1.0 |
506 |
- dev-java/jortho:0 |
507 |
- >=dev-java/jfreechart-1.0.14:1.0 |
508 |
- >=dev-java/itext-2.1.5:0 |
509 |
- dev-java/xz-java:0 |
510 |
- >=dev-lang/ghc-7.6.3 |
511 |
- >=dev-lang/polyml-5.6:=[-portable] |
512 |
- >=dev-lang/perl-5.8.8-r2 |
513 |
- >=dev-lang/swi-prolog-6.6.6 |
514 |
- sci-libs/coinor-csdp |
515 |
- =sci-mathematics/z3-4.4*[isabelle] |
516 |
- >=virtual/jdk-1.8 |
517 |
- doc? ( |
518 |
- virtual/latex-base |
519 |
- dev-tex/rail |
520 |
- ) |
521 |
- dev-lang/scala:${SS} |
522 |
- ledit? ( |
523 |
- app-misc/ledit |
524 |
- ) |
525 |
- readline? ( |
526 |
- app-misc/rlwrap |
527 |
- )" |
528 |
- |
529 |
-RDEPEND=" |
530 |
- dev-perl/libwww-perl |
531 |
- sci-mathematics/sha1-polyml |
532 |
- >=virtual/jre-1.8" |
533 |
- |
534 |
-S="${WORKDIR}"/Isabelle${MY_PV} |
535 |
-TARGETDIR="/usr/share/Isabelle" |
536 |
- |
537 |
-# Notes on QA warnings: * Class files not found via DEPEND in package.env |
538 |
-# Stuff with $ in the name appear to be spurious: |
539 |
-# isabelle/Markup_Tree$$anonfun$results$1$1.class |
540 |
-# scala/tools/nsc/backend/jvm/GenJVM$BytecodeGenerator$$anonfun$computeLocalVarsIndex$1.class |
541 |
-# It wants javafx, I am unsure how to fix this. I test isabelle with the Sun JDK: |
542 |
-# javafx/application/Platform.class javafx |
543 |
-# Presumably the user can provide the jEdit plugins if they are necessary: |
544 |
-# marker/MarkerSetsPlugin.class http://plugins.jedit.org/plugins/?MarkerSets |
545 |
-# projectviewer/gui/OptionPaneBase.class http://plugins.jedit.org/plugins/?ProjectViewer |
546 |
- |
547 |
-JAVA_GENTOO_CLASSPATH="itext,jcommon-1.0,jortho,jfreechart-1.0,scala-${SS},xz-java" |
548 |
- |
549 |
-CHECKREQS_MEMORY="8192M" |
550 |
-CHECKREQS_DISK_BUILD="17G" |
551 |
-CHECKREQS_DISK_USR="8G" |
552 |
- |
553 |
-src_unpack() { |
554 |
- unpack "${MY_P}.tar.gz" |
555 |
- cd "${S}/contrib" || die |
556 |
- unpack ${BP_IC_P}.tar.gz |
557 |
- unpack ${CSDP_IC_P}.tar.gz |
558 |
- unpack ${ISABELLE_FONTS_IC_P}.tar.gz |
559 |
- unpack ${JEDIT_IC_P}.tar.gz |
560 |
- unpack ${JORTHO_IC_P}.tar.gz |
561 |
- unpack ${JFREECHART_IC_P}.tar.gz |
562 |
- unpack ${POLYML_IC_P}.tar.gz |
563 |
- unpack ${SSH_JAVA_IC_P}.tar.gz |
564 |
- unpack ${XZ_JAVA_IC_P}.tar.gz |
565 |
-} |
566 |
- |
567 |
-pkg_setup() { |
568 |
- java-pkg-2_pkg_setup |
569 |
- check-reqs_pkg_setup |
570 |
-} |
571 |
- |
572 |
-src_prepare() { |
573 |
- java-pkg-2_src_prepare |
574 |
- java-pkg_getjars ${JAVA_GENTOO_CLASSPATH} |
575 |
- rm -rf "${S}/contrib/${BP_P}/{x86-cygwin,x86-darwin,x86_64-darwin,x86-linux,x86_64-linux}" \ |
576 |
- || die "Could not remove bash_process binaries" |
577 |
- rm -f "${S}/contrib/${JORTHI_P}/${JORTHO_PN}.jar" \ |
578 |
- || die "Could not remove contrib/${JORTHI_P}/${JORTHO_PN}.jar" |
579 |
- eapply "${FILESDIR}/${PN}-2016-classpath.patch" |
580 |
- eapply "${FILESDIR}/${PN}-2016-jfreechart-classpath.patch" |
581 |
- eapply "${FILESDIR}/${PN}-2016.1-bash_process-1.2.1-settings.patch" |
582 |
- eapply "${FILESDIR}/${PN}-2012-graphbrowser.patch" |
583 |
- eapply "${FILESDIR}/${PN}-2016.1-libsha1.patch" |
584 |
- eapply "${FILESDIR}/${PN}-2016.1-smt_timeout.patch" |
585 |
- eapply "${FILESDIR}/${PN}-2016.1-smt_read_only_certificates.patch" |
586 |
- eapply "${FILESDIR}/${PN}-2016.1-disable-jedit-build-after-install.patch" |
587 |
- eapply "${FILESDIR}/${PN}-2016.1-jortho-1.0-2-classpath.patch" |
588 |
- local polymlver=$(poly -v | cut -d' ' -f2) |
589 |
- local polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1) |
590 |
- cat <<- EOF >> "${S}/etc/settings" |
591 |
- # Poly/ML Gentoo (${polymlarch,,}) |
592 |
- ML_PLATFORM=${polymlarch,,}-linux |
593 |
- ML_HOME="${ROOT}usr/bin" |
594 |
- ML_SYSTEM=polyml-${polymlver} |
595 |
- ML_OPTIONS="-H 1000" |
596 |
- ML_SOURCES="${ROOT}usr/src/debug/dev-lang/polyml-${polymlver}" |
597 |
- |
598 |
- ISABELLE_GHC="${ROOT}usr/bin/ghc" |
599 |
- ISABELLE_OCAML="${ROOT}usr/bin/ocaml" |
600 |
- ISABELLE_SWIPL="${ROOT}usr/bin/swipl" |
601 |
- ISABELLE_JDK_HOME="\$(java-config --jdk-home)" |
602 |
- ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true" |
603 |
- SCALA_HOME="${ROOT}usr/share/scala-${SS}" |
604 |
- SHA1_HOME="${ROOT}usr/$(get_libdir)/sha1-polyml" |
605 |
- EOF |
606 |
- local Z3_P="$(best_version sci-mathematics/z3 | sed 's:sci-mathematics/::')" |
607 |
- cat <<- EOF >> "${S}/etc/components" |
608 |
- #bundled components |
609 |
- contrib/${BP_P} |
610 |
- contrib/${CSDP_P} |
611 |
- contrib/${ISABELLE_FONTS_P} |
612 |
- contrib/${JEDIT_P} |
613 |
- contrib/${JORTHO_P} |
614 |
- contrib/${JFREECHART_P} |
615 |
- contrib/${POLYML_P} |
616 |
- contrib/${SSH_JAVA_P} |
617 |
- contrib/${XZ_JAVA_P} |
618 |
- contrib/${Z3_P} |
619 |
- EOF |
620 |
- local Z3_RC="${ROOT}usr/share/Isabelle/contrib/${Z3_P}" |
621 |
- [ -d "${Z3_RC}" ] \ |
622 |
- || die "z3 isabelle component directory ${Z3_RC} does not exist" |
623 |
- ln -s "${Z3_RC}" \ |
624 |
- "${S}/contrib/${Z3_P}" \ |
625 |
- || die "Failed to create z3 isabelle component symbolic link" |
626 |
- if use ledit && ! use readline; then |
627 |
- eapply "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch" |
628 |
- fi |
629 |
- rm -f "${S}/contrib/${JFREECHART_P}/lib"/*.jar \ |
630 |
- || die "Could not rm bundled jar files supplied by Gentoo" |
631 |
-} |
632 |
- |
633 |
-src_compile() { |
634 |
- unset DISPLAY |
635 |
- einfo "Building Isabelle. This may take some time." |
636 |
- pushd contrib/${BP_P} || die "Could not cd to contrib/${BP_P}" |
637 |
- $(tc-getCC) ${CFLAGS} ${LDFLAGS} -o ${BP_PN} ${BP_PN}.c \ |
638 |
- || die "Could not build ${BP_PN}" |
639 |
- popd || die |
640 |
- if use graphbrowsing |
641 |
- then |
642 |
- rm -f "${S}/lib/browser/GraphBrowser.jar" \ |
643 |
- || die "failed cleaning graph browser directory" |
644 |
- pushd "${S}/lib/browser" \ |
645 |
- || die "Could not change directory to lib/browser" |
646 |
- ./build || die "failed building the graph browser" |
647 |
- popd |
648 |
- fi |
649 |
- ./bin/isabelle jedit -b -f || die "pide build failed" |
650 |
- pushd "${S}"/src/Pure || die "Could not change directory to src/Pure" |
651 |
- ../../bin/isabelle env ./build-jars -f || die "build-jars failed" |
652 |
- popd || die |
653 |
- ./bin/isabelle build -a -b -s -v || die "isabelle build failed" |
654 |
-} |
655 |
- |
656 |
-src_install() { |
657 |
- local Z3_P="$(best_version sci-mathematics/z3 | sed 's:sci-mathematics/::')" |
658 |
- rm "${S}/contrib/${Z3_P}" \ |
659 |
- || die "Failed to remove z3 isabelle component symbolic link" |
660 |
- |
661 |
- insinto ${TARGETDIR} |
662 |
- doins -r src |
663 |
- doins -r lib |
664 |
- doins -r contrib |
665 |
- doins ROOTS |
666 |
- |
667 |
- docompress -x /usr/share/doc/${PF} |
668 |
- dodoc -r doc |
669 |
- if use doc; then |
670 |
- dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc" |
671 |
- # The build of sci-mathematics/haskabelle with use doc requires |
672 |
- # sci-mathematics/isabelle[doc?]. The haskabelle doc build requires |
673 |
- # the src/Doc directory stuff in the isabelle package. |
674 |
- doins -r src/Doc |
675 |
- for i in $(find ./src/Doc -type f -executable -print) |
676 |
- do |
677 |
- exeinto $(dirname "${TARGETDIR}/${i}") |
678 |
- doexe ${i} |
679 |
- done |
680 |
- fi |
681 |
- |
682 |
- for i in $(find \ |
683 |
- ./{bin,lib,"contrib/${BP_P}/${BP_PN}",src/HOL,src/Pure,src/Tools} \ |
684 |
- -type f -executable -print) |
685 |
- do |
686 |
- exeinto $(dirname "${TARGETDIR}/${i}") |
687 |
- doexe ${i} |
688 |
- done |
689 |
- |
690 |
- insinto /etc/isabelle |
691 |
- doins -r etc/* |
692 |
- dosym /etc/isabelle "${TARGETDIR}/etc" |
693 |
- |
694 |
- local LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV} |
695 |
- dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps" |
696 |
- insinto ${LIBDIR} |
697 |
- doins -r heaps |
698 |
- |
699 |
- ./bin/isabelle install -d ${TARGETDIR} "${ED}usr/bin" \ |
700 |
- || die "isabelle install failed" |
701 |
- newicon lib/icons/"${PN}.xpm" "${PN}.xpm" |
702 |
- newicon lib/icons/"${PN}-mini.xpm" "${PN}-mini.xpm" |
703 |
- |
704 |
- java-pkg_regjar \ |
705 |
- $(find . -type f -name \*.jar -print | sed -e "s@^\.@${ED}${TARGETDIR}@g") |
706 |
- |
707 |
- local DOCS=( "ANNOUNCE" "CONTRIBUTORS" "COPYRIGHT" "NEWS" "README" ) |
708 |
- einstalldocs |
709 |
-} |
710 |
- |
711 |
-pkg_postinst() { |
712 |
- # If any of the directories in /etc/isabelle/components do not exist, then |
713 |
- # even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to |
714 |
- # to delete any non-existing directories. If an old Isabelle version was |
715 |
- # installed with component ebuilds like sci-mathematics/e, then the |
716 |
- # Isabelle version is upgraded, then the contrib directories will not |
717 |
- # exist initially, it is necessary to delete them from /etc/isabelle/components. |
718 |
- # Then these components are rebuilt (creating these directories) using the |
719 |
- # EAPI=5 subslot depends. |
720 |
- for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components") |
721 |
- do |
722 |
- if [ ! -d ${TARGETDIR}/${i} ]; then |
723 |
- sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components" |
724 |
- fi |
725 |
- done |
726 |
- if use ledit && use readline; then |
727 |
- elog "Both readline and ledit use flags specified. The default setting" |
728 |
- elog "if both are installed is to use readline (rlwrap), this can be" |
729 |
- elog "modfied by editing the ISABELLE_LINE_EDITOR setting in" |
730 |
- elog "${ROOT}/etc/isabelle/settings" |
731 |
- fi |
732 |
- elog "Please ensure you have a pdf viewer installed, for example:" |
733 |
- elog "As root: emerge app-text/zathura-pdf-poppler" |
734 |
- elog "Please configure your preferred pdf viewer, something like:" |
735 |
- elog "As normal user: xdg-mime default zathura.desktop application/pdf" |
736 |
- elog "Or alternatively by editing the PDF_VIEWER variable in the system" |
737 |
- elog "settings file ${ROOT}etc/isabelle/settings and/or the user" |
738 |
- elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings" |
739 |
- elog "For nitpick it is necessary to install:" |
740 |
- elog "emerge sci-mathematics/kodkodi" |
741 |
-} |
742 |
|
743 |
diff --git a/sci-mathematics/isabelle/metadata.xml b/sci-mathematics/isabelle/metadata.xml |
744 |
deleted file mode 100644 |
745 |
index d59b385fb4a..00000000000 |
746 |
--- a/sci-mathematics/isabelle/metadata.xml |
747 |
+++ /dev/null |
748 |
@@ -1,29 +0,0 @@ |
749 |
-<?xml version="1.0" encoding="UTF-8"?> |
750 |
-<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> |
751 |
-<pkgmetadata> |
752 |
-<maintainer type="person"> |
753 |
- <email>gienah@g.o</email> |
754 |
-</maintainer> |
755 |
-<maintainer type="project"> |
756 |
- <email>sci-mathematics@g.o</email> |
757 |
- <name>Gentoo Mathematics Project</name> |
758 |
-</maintainer> |
759 |
-<longdescription lang="en"> |
760 |
-Isabelle is a generic proof assistant. It allows mathematical |
761 |
-formulas to be expressed in a formal language and provides tools |
762 |
-for proving those formulas in a logical calculus. The main |
763 |
-application is the formalization of mathematical proofs and in |
764 |
-particular formal verification, which includes proving the |
765 |
-correctness of computer hardware or software and proving |
766 |
-properties of computer languages and protocols. |
767 |
-</longdescription> |
768 |
-<use> |
769 |
- <flag name="graphbrowsing">Generate theory browsing information, |
770 |
- including HTML documents that show a theory's definition, the |
771 |
- theorems proved in its ML file and the relationship with its |
772 |
- ancestors and descendants.</flag> |
773 |
- <flag name="ledit">Use ledit for the isabelle tty line editor</flag> |
774 |
- <flag name="readline">Use readline (rlwrap) for the isabelle tty line |
775 |
- editor</flag> |
776 |
-</use> |
777 |
-</pkgmetadata> |