1 |
commit: 1db4669fbb720d89e5420eb5a5b1c7b0ca508aa6 |
2 |
Author: James Le Cuirot <chewi <AT> gentoo <DOT> org> |
3 |
AuthorDate: Sun Mar 6 12:52:23 2016 +0000 |
4 |
Commit: James Le Cuirot <chewi <AT> gentoo <DOT> org> |
5 |
CommitDate: Sun Mar 6 13:01:33 2016 +0000 |
6 |
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=1db4669f |
7 |
|
8 |
sci-mathematics/isabelle: Remove old |
9 |
|
10 |
Package-Manager: portage-2.2.27 |
11 |
|
12 |
sci-mathematics/isabelle/Manifest | 10 - |
13 |
.../files/isabelle-2011.1-gentoo-settings.patch | 39 --- |
14 |
.../files/isabelle-2011.1-graphbrowser.patch | 11 - |
15 |
.../isabelle/files/isabelle-2011.1-libsha1.patch | 11 - |
16 |
.../isabelle-2011.1-proofgeneral-gentoo-path.patch | 39 --- |
17 |
...isabelle-2011.1-reverse-line-editor-order.patch | 12 - |
18 |
.../files/isabelle-2012-gentoo-settings.patch | 62 ---- |
19 |
...t-equations-in-function-definitions-error.patch | 35 -- |
20 |
.../files/isabelle-2012-signal-handling.patch | 8 - |
21 |
...belle-2013-HOL-Predicate_Compile_Examples.patch | 82 ----- |
22 |
.../isabelle/files/isabelle-2013-classpath.patch | 149 -------- |
23 |
.../isabelle/files/isabelle-2013.2-classpath.patch | 135 -------- |
24 |
sci-mathematics/isabelle/isabelle-2011.1-r2.ebuild | 254 -------------- |
25 |
sci-mathematics/isabelle/isabelle-2011.1.ebuild | 142 -------- |
26 |
sci-mathematics/isabelle/isabelle-2012-r1.ebuild | 320 ------------------ |
27 |
sci-mathematics/isabelle/isabelle-2013-r2.ebuild | 353 ------------------- |
28 |
sci-mathematics/isabelle/isabelle-2013.2-r1.ebuild | 375 --------------------- |
29 |
sci-mathematics/isabelle/metadata.xml | 15 - |
30 |
18 files changed, 2052 deletions(-) |
31 |
|
32 |
diff --git a/sci-mathematics/isabelle/Manifest b/sci-mathematics/isabelle/Manifest |
33 |
index 87a47c5..8e612b8 100644 |
34 |
--- a/sci-mathematics/isabelle/Manifest |
35 |
+++ b/sci-mathematics/isabelle/Manifest |
36 |
@@ -1,17 +1,7 @@ |
37 |
-DIST Isabelle2011-1.tar.gz 42239059 SHA256 48d77fe31a16b44f6015aa7953a60bdad8fcec9e60847630dc7b98c053edfc08 SHA512 213207951455395659a91b0bc6c8520c084cb6c75098c8f24c0800e41474c90c92aae86ffb99415142f6cf63d569556661ba350024fe458daa54a5cc9db372fd WHIRLPOOL 7e7868c3f464f507aceb8e1f648c04394fdd69746242179e66cfad64f927cf4d6aba41970428da5e45cce90a30bcee29bdc373d8a9e4943eb61cd97480d0a366 |
38 |
-DIST Isabelle2012-doc-src.tar.gz 2688496 SHA256 e18965fe0f7f89b286d4707e38201f1edbea81f6b26aed59d63a633c03fec097 SHA512 5aaea56eb67e535d745d63314278b6ee8469e6d3bbf4ce4d7b3f5e04b24557783b56d50d905a5ad69187c42f44407023c95a9bfb6faab125c21edff7638ff21d WHIRLPOOL 278b63a243950b1596376ee04cbfddb7a93c747e9f6ee66c5b069ca0dae4ca8d10bef43e03069b6186a19c703f71a585633fc47c3c1a15de3a886ff468232127 |
39 |
-DIST Isabelle2012.tar.gz 49529865 SHA256 b86f957dee221041f92c9d4ced4758d45b4950339743d0d58b1ea6061e2b53f0 SHA512 1346f563233eba10bc14f7d140706b8bfba8e832f7ee5887316c829926136af07d700914a925272d8adc1275b0bdd682540518957910c136a15bfc60d61285a0 WHIRLPOOL 23b764a1a0044a9525d058e95da318f4425fadf7660edc8ab8f35b248f98dcff0dba2e533ff18d8bf47ea164cec12a9648642749de2a49887bbe84ed4e71a68b |
40 |
-DIST Isabelle2013-2.tar.gz 52603110 SHA256 602e91377b0999c25950ae2a34c0fcb23e3aff3a196bdbc5ce61634bd90d7f22 SHA512 464a2735b2f4e28dcf44e55cd4abb4d8766a6bb7eb86f989f3592e7819e33d97922bdfb6701da85aa9d7c4cc2aee3eadebde1c7e3fc74bb3f6108a5daf5fea45 WHIRLPOOL 0dc354d60e3440ea0909dc09f25b66cb301b82f88fbe21c0b7f4bfef40ecc3631014757abd8657f0464047f0ad32827ad308e3f998fcf2477e05907ff7b19a84 |
41 |
-DIST Isabelle2013.tar.gz 54638791 SHA256 2f2cda9939248bd4346ad7e074cb6b2cfad70708777491c6262a5ae670c8f83a SHA512 e03f9b747f678749a562c3de6100f4f4e010ace51b2eb13bcde0a63591eec0cb4e081f7fad9147d022fe787b56eac3f037ab3a296080fd70cc7d058ea961a789 WHIRLPOOL 5cbcbc93bd2ce4723034c3d95d4678b2de90c924601b795c5da378cb76f58275e5d5f47ce9120234a9ea36e43ab759ced843dca76942378abfa1fb7aff858a65 |
42 |
DIST Isabelle2015.tar.gz 36529154 SHA256 08723d3be6f91c57a7a69a8624c54cc1e0cd31506988bf29ed365a5aa5a5156f SHA512 052bb80316a9345368a295a7c5f3869b58d71a6879548fc6240a04fd2cf8c11406274ead8a1ed098563ef9b7573a826656da543e745044fc1d275322af5cc212 WHIRLPOOL 0be4759a1064f4759c2f227b037c448093ff36b47e16002fbb7e99d2843583e01314c4ea5c7a8cbf4d1304f8f72a383052911e483d51e4af2e68c4c36dea5121 |
43 |
DIST csdp-isabelle-component-6.x.tar.gz 493 SHA256 65dde42fa476095052ca3820df4c0e45089653d4467a53de711c8e13670a1b19 SHA512 9be28ecbf61d0f6ad23e28d44bd7ceb8f06ab22f3a05a7c823a9c5bf52ddcf5e5c300c41e14451d6b8e6a4c32b1bbd17769c731cd890fab335a866cd5e735290 WHIRLPOOL c930c531637172e4c75ec44d68f71e69e748a8b976fa3651ef4015fb6a90e30b568bd092632dc16c6389aac09bc13f3249af6c3ac261f09ad2dc5ad915282f99 |
44 |
DIST exec_process-isabelle-component-1.0.3.tar.gz 814 SHA256 ee3b7b299852bcfd0bf7ffce6c8cd2279f2d71247c4a7b0042971b31c2b2a89d SHA512 7880b7f9843ff5806ab37d938a817a5b33e973772d9a6c6cf76bf04076fb532309bd22dfaa203be7c72c07f5a638f0f97e730c414ed164024fd31f1f09fc7c09 WHIRLPOOL 9d9beb7a41baac8b591ceee31bb7b69e1dd07fce66757511649977f6a85d85eef525ba0be13b0873c1aef47de0eace8bf88283b4a136397000e61cfc81da8d4d |
45 |
-DIST jedit_build-20120414.tar.gz 7509120 SHA256 3c5840fd01b87013b05a92742d41f66f655df6fe9edef1525c6722f92d8f3e41 SHA512 2e2f0db4964a041ba54382a9c787246e1d433e43167019c6ea8d4cf6beb84ce438c0bc559d2588229b0166c91bac603bed39abc45d5d4267020f55eaba1aaa0c WHIRLPOOL 40b883943bde312b4c7adc43607ba4759e5ebe22cab3c922c81393375f917af21d4a8dc068e5692ffcf7bdfb1e7fe3081358dc8e346d1942582bf79e249b0cbb |
46 |
-DIST jedit_build-isabelle-component-20130104.tar.gz 10734679 SHA256 22a4880deb1054a548476b22662b42bfaf5394ceb07b30eba69be433bcea1074 SHA512 bacdb3ca73d48fe9ba71dd32cd68e98333831f205dd3ced69bb9344c5b167ba084662f1108690f371b4b64f6b786955a332bcd51a2dc21c2179fb1b4727430dd WHIRLPOOL fc97923e08202e117ca3112b69f74a9f4663a70f55fa051ac55e02c85be57423f762263cac2ded33d9c2f412736e4fa0937aa07df3f36b915e806959055a796b |
47 |
-DIST jedit_build-isabelle-component-20131106.tar.gz 8796625 SHA256 a13a896263804f5aee82db0e1fe6be7982abe3ca1266cd15f7fe9c8c2f6e2ba5 SHA512 7fc3313916cd408c906e453a4895f49223a8b9dc1e2c577c16468394b73a3724449b411521884d419683cd3d2eb3ef59929608483ff092b9b0e3663efd5e136e WHIRLPOOL 4e7c933df7eea5b9c312f8e0c2c46d44a442d0dd2bb76415bea1fcf307ff75d1f8fb592fe4cad647674dc387fe6fa017dbf4e0cf2ec64459bdafb093470e2abf |
48 |
DIST jedit_build-isabelle-component-20150228.tar.gz 10674317 SHA256 2bee3c5242a3ce4150656f106e658096e82b6bd966e04d590e20023a956be29b SHA512 ba2d0804f21cee596fc3528a592941efc393e98b890efe054aed18fc0d31edfe459047b58ed79b42892e219b4c35a4fb5c8cca0f402b96d641ff8ce62e321339 WHIRLPOOL b2971bdef70e32d858385cb58603d6a5a7e357dbbc9810569093a31332a7838387f43a76a65048a12f259f08de86f200e962ccf2deb2bd3cd4e83dc4c1e41d8b |
49 |
DIST jfreechart-isabelle-component-1.0.14-1.tar.gz 3444825 SHA256 b0eb7365c4c5877379889100f081a4afc4117afc0d332941c3dd01bef2c4aee9 SHA512 ee1d84a45e43029d5e3acee823176196da19789322e8d3c2c81d5504930ad81d50e16e5da87655e4151034901daefb4ce6b82334839e39134b3a7ce32203aa67 WHIRLPOOL e6f9caadb802ecb5b784e86e96c008e9271aa0b1c940152fb0b0358280d9c1e274bb0dee1507f8ff0fe7f43f863db538d631c76e146d1f66ab6e8a8fb27eb42d |
50 |
-DIST jfreechart-isabelle-component-1.0.14.tar.gz 3443727 SHA256 c873ad6f07edbcceb5c76aac2e848c7d7f12c78c93c05f7e97c4b1fdba7c2df0 SHA512 c55ec01b215368f064de2f288f788960a256445adca5565c00aa9c0fab5732707a9e72bcdb3838676c80e735c520b9948855d7a32b9076bf35f1a279320ee72a WHIRLPOOL ba1a75e21525c302a3b755d814502dad60c540c2004dd894f60fdd6966766f85d71bbb45728ca220a4a7cff334de81db756fbb89e1059f32e248cabf0a7b97d6 |
51 |
-DIST polyml-isabelle-component-5.5.1-1.tar.gz 831 SHA256 f19a4dfc3117792423270cb98a5c406f7339f4bd7715c16976a281d964792844 SHA512 35ab69d0fd2737f3c6a13ca022103428bcb0e71032304d244614d271848b9ae8986da25bd4ef02668eef169f3a3a72576a619152ce3cbf036af7aa365e857c1a WHIRLPOOL 682e25b677e1b0401a43d4cff35c69658359b4c74f86d3459c050e7c7b0d17f1de1e7b792f2a51f97acf574ad56b3e89ade688bc24d090b3e89eaf0cb99a08d5 |
52 |
DIST polyml-isabelle-component-5.5.2-3.tar.gz 691 SHA256 1ba253974193efc70711b7fe32cc831d8bcc13107b0b130ddf6087bb6ff6d3e7 SHA512 45d68fa7a07ae9fc39cb21fa4c4c43a34576377fb828c8652002c56cc9ec7b3c7b5fcefb7604fc4bc90ce4868dd2fca41ddf37ce285da4902664ab21e4657b3f WHIRLPOOL 3a85c59b1bb928c5ea91f8150c6ded5309fae96bd7558b56e6c3d8f04c418b03b57fb49565af5ed919179fd9e30c957575ca7b65d938ce69c5d3131d8c55ab1e |
53 |
DIST xz-java-isabelle-component-1.5.tar.gz 315 SHA256 e7fdd433608561c87558d4d0ee39166e8396ce11242e85391417ec7fd3ce7b8e SHA512 6dfec49e12c4cafbb6b6386dd54477e86b6bb419a77c52d9606a0305aeea9cd11f087ed6bba77352c7bf9ec656052ef617e845f472e57b5cdfbccf22b2eeb4fa WHIRLPOOL 9c1fc16db0adc88557b81608902d9d69007dc90d5849f4f7501101930842ce81ded76af0e76e38df8bd0b07d137e53bafaa338bf6c7ae338e97af2a1433d5c1d |
54 |
|
55 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-gentoo-settings.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-gentoo-settings.patch |
56 |
deleted file mode 100644 |
57 |
index 67e3476..0000000 |
58 |
--- a/sci-mathematics/isabelle/files/isabelle-2011.1-gentoo-settings.patch |
59 |
+++ /dev/null |
60 |
@@ -1,39 +0,0 @@ |
61 |
---- Isabelle2011-1-orig/etc/settings 2011-10-10 01:47:58.000000000 +1100 |
62 |
-+++ Isabelle2011-1/etc/settings 2012-01-01 16:33:27.922565527 +1100 |
63 |
-@@ -24,9 +24,16 @@ |
64 |
- "/usr/share/polyml/$ML_PLATFORM" \ |
65 |
- "/opt/polyml/$ML_PLATFORM" \ |
66 |
- "")" |
67 |
--ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") |
68 |
--ML_OPTIONS="-H 200" |
69 |
--ML_SOURCES="$ML_HOME/../src" |
70 |
-+# ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") |
71 |
-+# ML_OPTIONS="-H 200" |
72 |
-+# ML_SOURCES="$ML_HOME/../src" |
73 |
-+ |
74 |
-+# Poly/ML 5.4.0 (64 bit) |
75 |
-+ML_PLATFORM=x86_64-linux |
76 |
-+ML_HOME=/usr/bin |
77 |
-+ML_SYSTEM=polyml-5.4.0 |
78 |
-+ML_OPTIONS="-H 1000" |
79 |
-+#ML_SOURCES="$ML_HOME/../src" |
80 |
- |
81 |
- # Poly/ML 32 bit (manual settings) |
82 |
- #ML_SYSTEM=polyml-5.4.0 |
83 |
-@@ -106,7 +113,7 @@ |
84 |
- ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" |
85 |
- |
86 |
- # Heap input locations. ML system identifier is included in lookup. |
87 |
--ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" |
88 |
-+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:/usr/lib64/Isabelle2011-1/heaps" |
89 |
- |
90 |
- # Heap output location. ML system identifier is appended automatically later on. |
91 |
- ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" |
92 |
-@@ -170,6 +177,7 @@ |
93 |
- "/usr/local/ProofGeneral" \ |
94 |
- "/usr/share/ProofGeneral" \ |
95 |
- "/opt/ProofGeneral" \ |
96 |
-+ "/usr/share/emacs/site-lisp/ProofGeneral" \ |
97 |
- "")" |
98 |
- |
99 |
- PROOFGENERAL_OPTIONS="" |
100 |
|
101 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch |
102 |
deleted file mode 100644 |
103 |
index ed8036a..0000000 |
104 |
--- a/sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch |
105 |
+++ /dev/null |
106 |
@@ -1,11 +0,0 @@ |
107 |
---- Isabelle2011-1-orig/lib/browser/build 2011-10-10 01:47:58.000000000 +1100 |
108 |
-+++ Isabelle2011-1/lib/browser/build 2012-01-08 12:58:06.041444651 +1100 |
109 |
-@@ -6,6 +6,8 @@ |
110 |
- # |
111 |
- # Requires proper Isabelle settings environment. |
112 |
- |
113 |
-+ISABELLE_HOME="$(cd "$(dirname "${0}")/../.."; pwd -P)" |
114 |
-+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 |
115 |
- |
116 |
- ## diagnostics |
117 |
- |
118 |
|
119 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-libsha1.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-libsha1.patch |
120 |
deleted file mode 100644 |
121 |
index 905a1eb..0000000 |
122 |
--- a/sci-mathematics/isabelle/files/isabelle-2011.1-libsha1.patch |
123 |
+++ /dev/null |
124 |
@@ -1,11 +0,0 @@ |
125 |
---- Isabelle2011-1-orig/src/Pure/General/sha1_polyml.ML 2011-10-10 01:47:58.000000000 +1100 |
126 |
-+++ Isabelle2011-1/src/Pure/General/sha1_polyml.ML 2012-12-05 23:28:15.004733643 +1100 |
127 |
-@@ -18,7 +18,7 @@ |
128 |
- in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end |
129 |
- |
130 |
- val lib_path = |
131 |
-- ("$ML_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so")) |
132 |
-+ ("$SHA1_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so")) |
133 |
- |> Path.explode; |
134 |
- |
135 |
- fun digest_external str = |
136 |
|
137 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-proofgeneral-gentoo-path.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-proofgeneral-gentoo-path.patch |
138 |
deleted file mode 100644 |
139 |
index 67e3476..0000000 |
140 |
--- a/sci-mathematics/isabelle/files/isabelle-2011.1-proofgeneral-gentoo-path.patch |
141 |
+++ /dev/null |
142 |
@@ -1,39 +0,0 @@ |
143 |
---- Isabelle2011-1-orig/etc/settings 2011-10-10 01:47:58.000000000 +1100 |
144 |
-+++ Isabelle2011-1/etc/settings 2012-01-01 16:33:27.922565527 +1100 |
145 |
-@@ -24,9 +24,16 @@ |
146 |
- "/usr/share/polyml/$ML_PLATFORM" \ |
147 |
- "/opt/polyml/$ML_PLATFORM" \ |
148 |
- "")" |
149 |
--ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") |
150 |
--ML_OPTIONS="-H 200" |
151 |
--ML_SOURCES="$ML_HOME/../src" |
152 |
-+# ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") |
153 |
-+# ML_OPTIONS="-H 200" |
154 |
-+# ML_SOURCES="$ML_HOME/../src" |
155 |
-+ |
156 |
-+# Poly/ML 5.4.0 (64 bit) |
157 |
-+ML_PLATFORM=x86_64-linux |
158 |
-+ML_HOME=/usr/bin |
159 |
-+ML_SYSTEM=polyml-5.4.0 |
160 |
-+ML_OPTIONS="-H 1000" |
161 |
-+#ML_SOURCES="$ML_HOME/../src" |
162 |
- |
163 |
- # Poly/ML 32 bit (manual settings) |
164 |
- #ML_SYSTEM=polyml-5.4.0 |
165 |
-@@ -106,7 +113,7 @@ |
166 |
- ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" |
167 |
- |
168 |
- # Heap input locations. ML system identifier is included in lookup. |
169 |
--ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" |
170 |
-+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:/usr/lib64/Isabelle2011-1/heaps" |
171 |
- |
172 |
- # Heap output location. ML system identifier is appended automatically later on. |
173 |
- ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" |
174 |
-@@ -170,6 +177,7 @@ |
175 |
- "/usr/local/ProofGeneral" \ |
176 |
- "/usr/share/ProofGeneral" \ |
177 |
- "/opt/ProofGeneral" \ |
178 |
-+ "/usr/share/emacs/site-lisp/ProofGeneral" \ |
179 |
- "")" |
180 |
- |
181 |
- PROOFGENERAL_OPTIONS="" |
182 |
|
183 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-reverse-line-editor-order.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-reverse-line-editor-order.patch |
184 |
deleted file mode 100644 |
185 |
index b2f2c35..0000000 |
186 |
--- a/sci-mathematics/isabelle/files/isabelle-2011.1-reverse-line-editor-order.patch |
187 |
+++ /dev/null |
188 |
@@ -1,12 +0,0 @@ |
189 |
---- Isabelle2011-1-orig/etc/settings 2011-10-10 01:47:58.000000000 +1100 |
190 |
-+++ Isabelle2011-1/etc/settings 2012-05-27 23:28:37.283028668 +1000 |
191 |
-@@ -66,8 +66,8 @@ |
192 |
- ### |
193 |
- |
194 |
- ISABELLE_LINE_EDITOR="" |
195 |
--[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" |
196 |
- [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)" |
197 |
-+[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" |
198 |
- |
199 |
- |
200 |
- ### |
201 |
|
202 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-gentoo-settings.patch b/sci-mathematics/isabelle/files/isabelle-2012-gentoo-settings.patch |
203 |
deleted file mode 100644 |
204 |
index 8994491..0000000 |
205 |
--- a/sci-mathematics/isabelle/files/isabelle-2012-gentoo-settings.patch |
206 |
+++ /dev/null |
207 |
@@ -1,62 +0,0 @@ |
208 |
---- Isabelle2012-orig/etc/settings 2012-05-23 03:07:38.000000000 +1000 |
209 |
-+++ Isabelle2012/etc/settings 2012-05-27 18:07:26.502878614 +1000 |
210 |
-@@ -16,17 +16,24 @@ |
211 |
- # Only one of the sections below should be activated. |
212 |
- |
213 |
- # Poly/ML default (automated settings) |
214 |
--ML_PLATFORM="$ISABELLE_PLATFORM" |
215 |
--ML_HOME="$(choosefrom \ |
216 |
-- "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \ |
217 |
-- "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \ |
218 |
-- "/usr/local/polyml/$ML_PLATFORM" \ |
219 |
-- "/usr/share/polyml/$ML_PLATFORM" \ |
220 |
-- "/opt/polyml/$ML_PLATFORM" \ |
221 |
-- "")" |
222 |
--ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") |
223 |
--ML_OPTIONS="-H 200" |
224 |
--ML_SOURCES="$ML_HOME/../src" |
225 |
-+# ML_PLATFORM="$ISABELLE_PLATFORM" |
226 |
-+# ML_HOME="$(choosefrom \ |
227 |
-+# "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \ |
228 |
-+# "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \ |
229 |
-+# "/usr/local/polyml/$ML_PLATFORM" \ |
230 |
-+# "/usr/share/polyml/$ML_PLATFORM" \ |
231 |
-+# "/opt/polyml/$ML_PLATFORM" \ |
232 |
-+# "")" |
233 |
-+# ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") |
234 |
-+# ML_OPTIONS="-H 200" |
235 |
-+# ML_SOURCES="$ML_HOME/../src" |
236 |
-+ |
237 |
-+# Poly/ML Gentoo (x86_64) |
238 |
-+ML_PLATFORM=x86_64-linux |
239 |
-+ML_HOME="/usr/bin" |
240 |
-+ML_SYSTEM=polyml-5.4.0 |
241 |
-+ML_OPTIONS="-H 1000" |
242 |
-+ML_SOURCES="/usr/src/debug/dev-lang/polyml-5.4.0" |
243 |
- |
244 |
- # Poly/ML 32 bit (manual settings) |
245 |
- #ML_SYSTEM=polyml-5.4.1 |
246 |
-@@ -102,7 +109,7 @@ |
247 |
- ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" |
248 |
- |
249 |
- # Heap input locations. ML system identifier is included in lookup. |
250 |
--ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" |
251 |
-+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:/usr/lib64/Isabelle2012/heaps" |
252 |
- |
253 |
- # Heap output location. ML system identifier is appended automatically later on. |
254 |
- ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" |
255 |
-@@ -161,13 +168,7 @@ |
256 |
- ### |
257 |
- |
258 |
- # Proof General home, look in a variety of places |
259 |
--PROOFGENERAL_HOME="$(choosefrom \ |
260 |
-- "$ISABELLE_HOME/contrib/ProofGeneral" \ |
261 |
-- "$ISABELLE_HOME/../ProofGeneral" \ |
262 |
-- "/usr/local/ProofGeneral" \ |
263 |
-- "/usr/share/ProofGeneral" \ |
264 |
-- "/opt/ProofGeneral" \ |
265 |
-- "")" |
266 |
-+PROOFGENERAL_HOME="/usr/share/emacs/site-lisp/ProofGeneral" |
267 |
- |
268 |
- PROOFGENERAL_OPTIONS="" |
269 |
- #PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets" |
270 |
|
271 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-redundant-equations-in-function-definitions-error.patch b/sci-mathematics/isabelle/files/isabelle-2012-redundant-equations-in-function-definitions-error.patch |
272 |
deleted file mode 100644 |
273 |
index 18ae43d..0000000 |
274 |
--- a/sci-mathematics/isabelle/files/isabelle-2012-redundant-equations-in-function-definitions-error.patch |
275 |
+++ /dev/null |
276 |
@@ -1,35 +0,0 @@ |
277 |
-diff -r dd611ab202a8 -r e7e647949c95 src/HOL/Tools/Function/fun.ML |
278 |
---- a/src/HOL/Tools/Function/fun.ML Wed Jun 06 10:35:05 2012 +0200 |
279 |
-+++ b/src/HOL/Tools/Function/fun.ML Wed Jun 06 21:36:21 2012 +0200 |
280 |
-@@ -84,10 +84,10 @@ |
281 |
- spec @ mk_catchall fixes arity_of |
282 |
- end |
283 |
- |
284 |
--fun warnings ctxt origs tss = |
285 |
-+fun further_checks ctxt origs tss = |
286 |
- let |
287 |
-- fun warn_redundant t = |
288 |
-- warning ("Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)) |
289 |
-+ fun fail_redundant t = |
290 |
-+ error (cat_lines ["Equation is redundant (covered by preceding clauses):", Syntax.string_of_term ctxt t]) |
291 |
- fun warn_missing strs = |
292 |
- warning (cat_lines ("Missing patterns in function definition:" :: strs)) |
293 |
- |
294 |
-@@ -100,7 +100,7 @@ |
295 |
- @ ["(" ^ string_of_int (length rest) ^ " more)"]) |
296 |
- |
297 |
- val _ = (origs ~~ tss') |
298 |
-- |> map (fn (t, ts) => if null ts then warn_redundant t else ()) |
299 |
-+ |> map (fn (t, ts) => if null ts then fail_redundant t else ()) |
300 |
- in |
301 |
- () |
302 |
- end |
303 |
-@@ -119,7 +119,7 @@ |
304 |
- val compleqs = add_catchall ctxt fixes feqs (* Completion *) |
305 |
- |
306 |
- val spliteqs = Function_Split.split_all_equations ctxt compleqs |
307 |
-- |> tap (warnings ctxt feqs) |
308 |
-+ |> tap (further_checks ctxt feqs) |
309 |
- |
310 |
- fun restore_spec thms = |
311 |
- bnds ~~ take (length bnds) (unflat spliteqs thms) |
312 |
|
313 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-signal-handling.patch b/sci-mathematics/isabelle/files/isabelle-2012-signal-handling.patch |
314 |
deleted file mode 100644 |
315 |
index d238f41..0000000 |
316 |
--- a/sci-mathematics/isabelle/files/isabelle-2012-signal-handling.patch |
317 |
+++ /dev/null |
318 |
@@ -1,8 +0,0 @@ |
319 |
-diff -r c79adcae9869 -r 6de952f4069f lib/scripts/run-polyml |
320 |
---- a/lib/scripts/run-polyml Fri May 25 13:23:43 2012 +0200 |
321 |
-+++ b/lib/scripts/run-polyml Fri May 25 17:14:14 2012 +0200 |
322 |
-@@ -76,3 +76,3 @@ |
323 |
- "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
324 |
-- { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
325 |
-+ { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; } |
326 |
- RC="$?" |
327 |
|
328 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch b/sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch |
329 |
deleted file mode 100644 |
330 |
index bce7eec..0000000 |
331 |
--- a/sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch |
332 |
+++ /dev/null |
333 |
@@ -1,82 +0,0 @@ |
334 |
---- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy 2013-02-13 00:31:10.000000000 +1100 |
335 |
-+++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy 2013-08-31 14:37:02.015159000 +1000 |
336 |
-@@ -82,7 +82,7 @@ |
337 |
- setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *} |
338 |
- |
339 |
- lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g" |
340 |
--quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
341 |
-+quickcheck[tester = prolog, iterations = 1] |
342 |
- oops |
343 |
- |
344 |
- section {* Manual setup to find the counterexample *} |
345 |
-@@ -110,7 +110,7 @@ |
346 |
- |
347 |
- lemma |
348 |
- "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g" |
349 |
--quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
350 |
-+quickcheck[tester = prolog, iterations = 1] |
351 |
- oops |
352 |
- |
353 |
- section {* Using a global limit for limiting the execution *} |
354 |
-@@ -146,7 +146,7 @@ |
355 |
- |
356 |
- lemma |
357 |
- "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g" |
358 |
--quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
359 |
-+quickcheck[tester = prolog, iterations = 1] |
360 |
- oops |
361 |
- |
362 |
- end |
363 |
-\ No newline at end of file |
364 |
---- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy 2013-02-13 00:31:10.000000000 +1100 |
365 |
-+++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy 2013-08-31 14:36:47.049851000 +1000 |
366 |
-@@ -33,7 +33,7 @@ |
367 |
- |
368 |
- lemma |
369 |
- "S\<^isub>1p w \<Longrightarrow> w = []" |
370 |
--quickcheck[tester = prolog, iterations=1, expect = counterexample] |
371 |
-+quickcheck[tester = prolog, iterations=1] |
372 |
- oops |
373 |
- |
374 |
- definition "filter_a = filter (\<lambda>x. x = a)" |
375 |
-@@ -67,7 +67,7 @@ |
376 |
- |
377 |
- theorem S\<^isub>1_sound: |
378 |
- "S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
379 |
--quickcheck[tester = prolog, iterations=1, expect = counterexample] |
380 |
-+quickcheck[tester = prolog, iterations=1] |
381 |
- oops |
382 |
- |
383 |
- |
384 |
-@@ -91,7 +91,7 @@ |
385 |
- |
386 |
- theorem S\<^isub>2_sound: |
387 |
- "S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
388 |
--quickcheck[tester = prolog, iterations=1, expect = counterexample] |
389 |
-+quickcheck[tester = prolog, iterations=1] |
390 |
- oops |
391 |
- |
392 |
- inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where |
393 |
---- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy 2013-02-13 00:31:10.000000000 +1100 |
394 |
-+++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy 2013-08-31 14:28:11.784390000 +1000 |
395 |
-@@ -92,7 +92,7 @@ |
396 |
- |
397 |
- lemma |
398 |
- "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U" |
399 |
--quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
400 |
-+quickcheck[tester = prolog, iterations = 1] |
401 |
- oops |
402 |
- |
403 |
- text {* Verifying that the found counterexample really is one by means of a proof *} |
404 |
---- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/List_Examples.thy 2013-02-13 00:31:10.000000000 +1100 |
405 |
-+++ Isabelle2013/src/HOL/Predicate_Compile_Examples/List_Examples.thy 2013-08-31 14:27:52.013962000 +1000 |
406 |
-@@ -21,7 +21,7 @@ |
407 |
- lemma "(xs :: nat list) = ys @ ys --> rev xs = xs" |
408 |
- quickcheck[tester = random, iterations = 10000] |
409 |
- quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample] |
410 |
--quickcheck[tester = prolog, expect = counterexample] |
411 |
-+quickcheck[tester = prolog] |
412 |
- oops |
413 |
- |
414 |
- end |
415 |
-\ No newline at end of file |
416 |
|
417 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch |
418 |
deleted file mode 100644 |
419 |
index e3b2271..0000000 |
420 |
--- a/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch |
421 |
+++ /dev/null |
422 |
@@ -1,149 +0,0 @@ |
423 |
---- Isabelle2013-orig/lib/Tools/java 2013-02-13 00:31:02.000000000 +1100 |
424 |
-+++ Isabelle2013/lib/Tools/java 2015-04-17 12:16:04.734716358 +1000 |
425 |
-@@ -6,5 +6,5 @@ |
426 |
- |
427 |
- CLASSPATH="$(jvmpath "$CLASSPATH")" |
428 |
- isabelle_jdk java -Dfile.encoding=UTF-8 -server \ |
429 |
-- "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@" |
430 |
-+ "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala-2.10 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@" |
431 |
- |
432 |
---- Isabelle2013-orig/lib/Tools/scala 2013-02-13 00:31:02.000000000 +1100 |
433 |
-+++ Isabelle2013/lib/Tools/scala 2015-04-17 12:12:21.606890256 +1000 |
434 |
-@@ -8,4 +8,4 @@ |
435 |
- |
436 |
- CLASSPATH="$(jvmpath "$CLASSPATH")" |
437 |
- isabelle_scala scala -Dfile.encoding=UTF-8 \ |
438 |
-- "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@" |
439 |
-+ "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala-2.10 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@" |
440 |
---- Isabelle2013-orig/lib/Tools/scalac 2013-02-13 00:31:02.000000000 +1100 |
441 |
-+++ Isabelle2013/lib/Tools/scalac 2015-04-17 12:12:36.895871214 +1000 |
442 |
-@@ -8,5 +8,5 @@ |
443 |
- |
444 |
- CLASSPATH="$(jvmpath "$CLASSPATH")" |
445 |
- isabelle_scala scalac -Dfile.encoding=UTF-8 \ |
446 |
-- "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@" |
447 |
-+ "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala-2.10 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@" |
448 |
- |
449 |
---- Isabelle2013-orig/src/Pure/build-jars 2013-02-13 00:31:15.000000000 +1100 |
450 |
-+++ Isabelle2013/src/Pure/build-jars 2013-08-18 12:55:51.400924000 +1000 |
451 |
-@@ -133,7 +133,7 @@ |
452 |
- declare -a JFREECHART_JARS=() |
453 |
- for NAME in $JFREECHART_JAR_NAMES |
454 |
- do |
455 |
-- JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME" |
456 |
-+ JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$NAME" |
457 |
- done |
458 |
- |
459 |
- |
460 |
---- Isabelle2013-orig/src/Tools/jEdit/lib/Tools/jedit 2013-02-13 00:31:16.000000000 +1100 |
461 |
-+++ Isabelle2013/src/Tools/jEdit/lib/Tools/jedit 2013-08-18 16:39:15.495244000 +1000 |
462 |
-@@ -214,97 +214,11 @@ |
463 |
- declare -a JFREECHART_JARS=() |
464 |
- for NAME in $JFREECHART_JAR_NAMES |
465 |
- do |
466 |
-- JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME" |
467 |
-+ JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$NAME" |
468 |
- done |
469 |
- |
470 |
-- |
471 |
--# target |
472 |
-- |
473 |
--TARGET="dist/jars/Isabelle-jEdit.jar" |
474 |
-- |
475 |
--declare -a UPDATED=() |
476 |
-- |
477 |
--if [ "$BUILD_JARS" = jars_fresh ]; then |
478 |
-- OUTDATED=true |
479 |
--else |
480 |
-- OUTDATED=false |
481 |
-- if [ ! -e "$TARGET" ]; then |
482 |
-- OUTDATED=true |
483 |
-- else |
484 |
-- if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then |
485 |
-- declare -a DEPS=( |
486 |
-- "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" |
487 |
-- "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}" |
488 |
-- ) |
489 |
-- elif [ -e "$ISABELLE_HOME/Admin/build" ]; then |
490 |
-- declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}") |
491 |
-- else |
492 |
-- declare -a DEPS=() |
493 |
-- fi |
494 |
-- for DEP in "${DEPS[@]}" |
495 |
-- do |
496 |
-- [ ! -e "$DEP" ] && fail "Missing file: $DEP" |
497 |
-- [ "$DEP" -nt "$TARGET" ] && { |
498 |
-- OUTDATED=true |
499 |
-- UPDATED["${#UPDATED[@]}"]="$DEP" |
500 |
-- } |
501 |
-- done |
502 |
-- fi |
503 |
--fi |
504 |
-- |
505 |
-- |
506 |
--# build |
507 |
-- |
508 |
--if [ "$OUTDATED" = true ] |
509 |
--then |
510 |
-- echo "### Building Isabelle/jEdit ..." |
511 |
-- |
512 |
-- [ "${#UPDATED[@]}" -gt 0 ] && { |
513 |
-- echo "Changed files:" |
514 |
-- for FILE in "${UPDATED[@]}" |
515 |
-- do |
516 |
-- echo " $FILE" |
517 |
-- done |
518 |
-- } |
519 |
-- |
520 |
-- [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \ |
521 |
-- fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component" |
522 |
-- |
523 |
-- rm -rf dist || failed |
524 |
-- mkdir -p dist dist/classes || failed |
525 |
-- |
526 |
-- cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/. |
527 |
-- cp -p -R -f "${RESOURCES[@]}" dist/classes/. |
528 |
-- cp src/jEdit.props dist/properties/. |
529 |
-- cp -p -R -f src/modes/. dist/modes/. |
530 |
-- |
531 |
-- perl -i -e 'while (<>) { |
532 |
-- if (m/NAME="javacc"/) { |
533 |
-- print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; |
534 |
-- print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,; |
535 |
-- print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; } |
536 |
-- print; }' dist/modes/catalog |
537 |
-- |
538 |
-- cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed |
539 |
-- ( |
540 |
-- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$PURE_JAR" \ |
541 |
-- "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar" |
542 |
-- do |
543 |
-- CLASSPATH="$CLASSPATH:$JAR" |
544 |
-- done |
545 |
-- CLASSPATH="$(jvmpath "$CLASSPATH")" |
546 |
-- exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}" |
547 |
-- ) || fail "Failed to compile sources" |
548 |
-- |
549 |
-- cd dist/classes |
550 |
-- isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed |
551 |
-- cd ../.. |
552 |
-- rm -rf dist/classes |
553 |
--fi |
554 |
-- |
555 |
- popd >/dev/null |
556 |
- |
557 |
-- |
558 |
- ## main |
559 |
- |
560 |
- if [ "$BUILD_ONLY" = false ]; then |
561 |
---- Isabelle2013-orig/contrib/jfreechart-1.0.14/etc/settings 2012-12-09 07:23:53.000000000 +1100 |
562 |
-+++ Isabelle2013/contrib/jfreechart-1.0.14/etc/settings 2013-08-18 16:18:10.244698000 +1000 |
563 |
-@@ -1,7 +1,5 @@ |
564 |
- # -*- shell-script -*- :mode=shellscript: |
565 |
- |
566 |
- JFREECHART_HOME="$COMPONENT" |
567 |
--JFREECHART_JAR_NAMES="iText-2.1.5.jar jcommon-1.0.18.jar jfreechart-1.0.14.jar" |
568 |
-- |
569 |
--ISABELLE_JAVA_EXT="$ISABELLE_JAVA_EXT:$JFREECHART_HOME/lib" |
570 |
-+JFREECHART_JAR_NAMES="$(java-config -p itext | sed -e 's@:@ @g') $(java-config -p jcommon-1.0 | sed -e 's@:@ @g') $(java-config -p jfreechart-1.0 | sed -e 's@:@ @g')" |
571 |
- |
572 |
|
573 |
diff --git a/sci-mathematics/isabelle/files/isabelle-2013.2-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2013.2-classpath.patch |
574 |
deleted file mode 100644 |
575 |
index b3ad4ae..0000000 |
576 |
--- a/sci-mathematics/isabelle/files/isabelle-2013.2-classpath.patch |
577 |
+++ /dev/null |
578 |
@@ -1,135 +0,0 @@ |
579 |
---- Isabelle2013-2-orig/lib/Tools/java 2013-12-06 02:18:34.000000000 +1100 |
580 |
-+++ Isabelle2013-2/lib/Tools/java 2015-04-17 12:23:11.535463796 +1000 |
581 |
-@@ -10,5 +10,5 @@ |
582 |
- unset CLASSPATH |
583 |
- |
584 |
- isabelle_jdk java "${JAVA_ARGS[@]}" \ |
585 |
-- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@" |
586 |
-+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@" |
587 |
- |
588 |
---- Isabelle2013-2-orig/lib/Tools/scala 2013-12-06 02:18:34.000000000 +1100 |
589 |
-+++ Isabelle2013-2/lib/Tools/scala 2015-04-17 12:23:24.836455672 +1000 |
590 |
-@@ -7,5 +7,5 @@ |
591 |
- isabelle_admin_build jars || exit $? |
592 |
- |
593 |
- isabelle_scala scala -Dfile.encoding=UTF-8 \ |
594 |
-- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@" |
595 |
-+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@" |
596 |
- |
597 |
---- Isabelle2013-2-orig/lib/Tools/scalac 2013-12-06 02:18:34.000000000 +1100 |
598 |
-+++ Isabelle2013-2/lib/Tools/scalac 2015-04-17 12:23:33.084450628 +1000 |
599 |
-@@ -7,5 +7,5 @@ |
600 |
- isabelle_admin_build jars || exit $? |
601 |
- |
602 |
- isabelle_scala scalac -Dfile.encoding=UTF-8 \ |
603 |
-- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@" |
604 |
-+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@" |
605 |
- |
606 |
---- Isabelle2013-2-orig/src/Tools/jEdit/lib/Tools/jedit 2013-12-06 02:19:04.000000000 +1100 |
607 |
-+++ Isabelle2013-2/src/Tools/jEdit/lib/Tools/jedit 2014-02-09 20:59:14.026841490 +1100 |
608 |
-@@ -211,105 +211,6 @@ |
609 |
- "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar" |
610 |
- ) |
611 |
- |
612 |
-- |
613 |
--# target |
614 |
-- |
615 |
--TARGET="dist/jars/Isabelle-jEdit.jar" |
616 |
-- |
617 |
--declare -a UPDATED=() |
618 |
-- |
619 |
--if [ "$BUILD_JARS" = jars_fresh ]; then |
620 |
-- OUTDATED=true |
621 |
--else |
622 |
-- OUTDATED=false |
623 |
-- if [ ! -e "$TARGET" ]; then |
624 |
-- OUTDATED=true |
625 |
-- else |
626 |
-- if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then |
627 |
-- declare -a DEPS=( |
628 |
-- "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR" |
629 |
-- "${SOURCES[@]}" "${RESOURCES[@]}" |
630 |
-- ) |
631 |
-- elif [ -e "$ISABELLE_HOME/Admin/build" ]; then |
632 |
-- declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}") |
633 |
-- else |
634 |
-- declare -a DEPS=() |
635 |
-- fi |
636 |
-- for DEP in "${DEPS[@]}" |
637 |
-- do |
638 |
-- [ ! -e "$DEP" ] && fail "Missing file: $DEP" |
639 |
-- [ "$DEP" -nt "$TARGET" ] && { |
640 |
-- OUTDATED=true |
641 |
-- UPDATED["${#UPDATED[@]}"]="$DEP" |
642 |
-- } |
643 |
-- done |
644 |
-- fi |
645 |
--fi |
646 |
-- |
647 |
-- |
648 |
--# build |
649 |
-- |
650 |
--if [ "$OUTDATED" = true ] |
651 |
--then |
652 |
-- echo "### Building Isabelle/jEdit ..." |
653 |
-- |
654 |
-- [ "${#UPDATED[@]}" -gt 0 ] && { |
655 |
-- echo "Changed files:" |
656 |
-- for FILE in "${UPDATED[@]}" |
657 |
-- do |
658 |
-- echo " $FILE" |
659 |
-- done |
660 |
-- } |
661 |
-- |
662 |
-- [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \ |
663 |
-- fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component" |
664 |
-- |
665 |
-- rm -rf dist || failed |
666 |
-- mkdir -p dist dist/classes || failed |
667 |
-- |
668 |
-- cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/. |
669 |
-- cp -p -R -f "${RESOURCES[@]}" dist/classes/. |
670 |
-- cp src/jEdit.props dist/properties/. |
671 |
-- cp -p -R -f src/modes/. dist/modes/. |
672 |
-- |
673 |
-- perl -i -e 'while (<>) { |
674 |
-- if (m/NAME="javacc"/) { |
675 |
-- print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; |
676 |
-- print qq,<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n,; |
677 |
-- print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,; |
678 |
-- print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; } |
679 |
-- print; }' dist/modes/catalog |
680 |
-- |
681 |
-- cd dist |
682 |
-- isabelle_jdk jar xf jedit.jar |
683 |
-- cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" \ |
684 |
-- "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed |
685 |
-- cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" \ |
686 |
-- "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed |
687 |
-- isabelle_jdk jar cfe jedit.jar org.gjt.sp.jedit.jEdit org || failed |
688 |
-- rm -rf META-INF org |
689 |
-- cd .. |
690 |
-- |
691 |
-- cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed |
692 |
-- ( |
693 |
-- #workaround for scalac 2.10.2 |
694 |
-- function stty() { :; } |
695 |
-- export -f stty |
696 |
-- |
697 |
-- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR" |
698 |
-- do |
699 |
-- classpath "$JAR" |
700 |
-- done |
701 |
-- export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")" |
702 |
-- exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}" |
703 |
-- ) || fail "Failed to compile sources" |
704 |
-- |
705 |
-- cd dist/classes |
706 |
-- isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed |
707 |
-- cd ../.. |
708 |
-- rm -rf dist/classes |
709 |
--fi |
710 |
-- |
711 |
- popd >/dev/null |
712 |
- |
713 |
- |
714 |
|
715 |
diff --git a/sci-mathematics/isabelle/isabelle-2011.1-r2.ebuild b/sci-mathematics/isabelle/isabelle-2011.1-r2.ebuild |
716 |
deleted file mode 100644 |
717 |
index 6b96bcb..0000000 |
718 |
--- a/sci-mathematics/isabelle/isabelle-2011.1-r2.ebuild |
719 |
+++ /dev/null |
720 |
@@ -1,254 +0,0 @@ |
721 |
-# Copyright 1999-2015 Gentoo Foundation |
722 |
-# Distributed under the terms of the GNU General Public License v2 |
723 |
-# $Id$ |
724 |
- |
725 |
-EAPI="5" |
726 |
- |
727 |
-inherit eutils java-pkg-2 multilib versionator |
728 |
- |
729 |
-MY_PN="Isabelle" |
730 |
-MY_PV=$(replace_all_version_separators '-') |
731 |
-MY_P="${MY_PN}${MY_PV}" |
732 |
- |
733 |
-DESCRIPTION="Isabelle is a generic proof assistant" |
734 |
-HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html" |
735 |
-SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz" |
736 |
- |
737 |
-LICENSE="BSD" |
738 |
-SLOT="0/${PV}" |
739 |
-KEYWORDS="~amd64 ~x86" |
740 |
-ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents" |
741 |
-IUSE="${ALL_LOGICS} doc graphbrowsing ledit readline +proofgeneral test" |
742 |
- |
743 |
-#upstream says |
744 |
-#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, |
745 |
-#for document preparation: complete LaTeX |
746 |
-DEPEND=">=app-shells/bash-3.0:* |
747 |
- >=dev-lang/polyml-5.4.1:=[-portable] |
748 |
- >=dev-lang/perl-5.8.8-r2" |
749 |
- |
750 |
-RDEPEND="dev-perl/libwww-perl |
751 |
- sci-mathematics/sha1-polyml |
752 |
- doc? ( |
753 |
- virtual/latex-base |
754 |
- dev-tex/rail |
755 |
- ) |
756 |
- proofgeneral? ( |
757 |
- app-emacs/proofgeneral |
758 |
- ) |
759 |
- ledit? ( |
760 |
- app-misc/ledit |
761 |
- ) |
762 |
- readline? ( |
763 |
- app-misc/rlwrap |
764 |
- ) |
765 |
- ${DEPEND}" |
766 |
- |
767 |
-S="${WORKDIR}"/Isabelle${MY_PV} |
768 |
-TARGETDIR="/usr/share/Isabelle"${MY_PV} |
769 |
-LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV} |
770 |
- |
771 |
-pkg_setup() { |
772 |
- java-pkg-2_pkg_setup |
773 |
- if ! use proofgeneral |
774 |
- then |
775 |
- ewarn "You have deselected the Proof General interface." |
776 |
- ewarn "Only a text terminal will be installed." |
777 |
- ewarn "Emerge Isabelle with the proofgeneral USE flag enabled" |
778 |
- ewarn "to get the common interface, that most people want." |
779 |
- fi |
780 |
-} |
781 |
- |
782 |
-src_prepare() { |
783 |
- java-pkg-2_src_prepare |
784 |
- epatch "${FILESDIR}/${PN}-2011.1-gentoo-settings.patch" |
785 |
- polymlver=$(poly -v | cut -d' ' -f2) |
786 |
- polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1) |
787 |
- sed -e "s@5.4.0@${polymlver}@g" \ |
788 |
- -i "${S}/etc/settings" \ |
789 |
- || die "Could not configure polyml version in etc/settings" |
790 |
- sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \ |
791 |
- -i "${S}/etc/settings" \ |
792 |
- || die "Could not configure polyml ML_HOME in etc/settings" |
793 |
- sed -e "s@x86_64@${polymlarch}@g" \ |
794 |
- -i "${S}/etc/settings" \ |
795 |
- || die "Could not configure polyml arch in etc/settings" |
796 |
- sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \ |
797 |
- -i "${S}/etc/settings" \ |
798 |
- || die "Could not configure PROOFGENERAL_HOME in etc/settings" |
799 |
- sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \ |
800 |
- -i "${S}/etc/settings" \ |
801 |
- || die "Could not configure Isabelle lib directory in etc/settings" |
802 |
- epatch "${FILESDIR}/${PN}-2011.1-graphbrowser.patch" |
803 |
- epatch "${FILESDIR}/${PN}-2011.1-libsha1.patch" |
804 |
- cat <<- EOF >> "${S}/etc/settings" |
805 |
- |
806 |
- ISABELLE_GHC="${ROOT}usr/bin/ghc" |
807 |
- ISABELLE_OCAML="${ROOT}usr/bin/ocaml" |
808 |
- ISABELLE_SWIPL="${ROOT}usr/bin/swipl" |
809 |
- ISABELLE_JDK_HOME="\$(java-config --jdk-home)" |
810 |
- SCALA_HOME="${ROOT}usr/share/scala" |
811 |
- SHA1_HOME="/usr/$(get_libdir)/sha1-polyml" |
812 |
- EOF |
813 |
- if use ledit && ! use readline; then |
814 |
- epatch "${FILESDIR}/${PN}-2011.1-reverse-line-editor-order.patch" |
815 |
- fi |
816 |
-} |
817 |
- |
818 |
-src_compile() { |
819 |
- LOGICS="" |
820 |
- for l in "${ALL_LOGICS}"; do |
821 |
- if has "${l/+/}"; then |
822 |
- LOGICS="${LOGICS} ${l/+/}" |
823 |
- fi |
824 |
- done |
825 |
- einfo "Building Isabelle logics ${LOGICS}. This may take some time." |
826 |
- ./build -b -i "${LOGICS}" || die "building logics failed" |
827 |
- ./bin/isabelle makeall || die "isabelle makeall failed" |
828 |
- if use graphbrowsing |
829 |
- then |
830 |
- rm -f "${S}/lib/browser/GraphBrowser.jar" \ |
831 |
- || die "failed cleaning graph browser directory" |
832 |
- pushd "${S}/lib/browser" \ |
833 |
- || die "Could not change directory to lib/browser" |
834 |
- ./build || die "failed building the graph browser" |
835 |
- popd |
836 |
- fi |
837 |
-} |
838 |
- |
839 |
-src_test() { |
840 |
- einfo "Running tests. A test run can take up to several hours!" |
841 |
- ./build -b -t || die "tests failed" |
842 |
-} |
843 |
- |
844 |
-src_install() { |
845 |
- exeinto ${TARGETDIR}/bin |
846 |
- doexe bin/isabelle-process bin/isabelle |
847 |
- |
848 |
- insinto ${TARGETDIR} |
849 |
- doins -r src |
850 |
- doins -r lib |
851 |
- |
852 |
- for i in "./build" \ |
853 |
- "src/Pure/mk" \ |
854 |
- "src/Pure/build-jars" \ |
855 |
- "src/Tools/jEdit/dist/build-support/ci/copy_properties.groovy" \ |
856 |
- "src/Tools/jEdit/dist/build-support/ci/ci_release.groovy" \ |
857 |
- "src/Tools/jEdit/lib/Tools/jedit" \ |
858 |
- "src/Tools/Metis/fix_metis_license" \ |
859 |
- "src/Tools/Metis/make_metis" \ |
860 |
- "src/Tools/Metis/scripts/mlpp" \ |
861 |
- "src/Tools/WWW_Find/lib/Tools/wwwfind" \ |
862 |
- "src/Tools/Code/lib/Tools/codegen" \ |
863 |
- "src/HOL/Mirabelle/lib/Tools/mirabelle" \ |
864 |
- "src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \ |
865 |
- "src/HOL/Tools/SMT/lib/scripts/remote_smt" \ |
866 |
- "src/HOL/Tools/ATP/scripts/remote_atp" \ |
867 |
- "src/HOL/Tools/ATP/scripts/spass" \ |
868 |
- "src/HOL/Tools/Nitpick/lib/Tools/nitrox" \ |
869 |
- "src/HOL/Mutabelle/lib/Tools/mutabelle" \ |
870 |
- "src/HOL/Library/Sum_of_Squares/neos_csdp_client" \ |
871 |
- "lib/browser/build" \ |
872 |
- "lib/Tools/tty" \ |
873 |
- "lib/Tools/mkproject" \ |
874 |
- "lib/Tools/keywords" \ |
875 |
- "lib/Tools/browser" \ |
876 |
- "lib/Tools/install" \ |
877 |
- "lib/Tools/mkdir" \ |
878 |
- "lib/Tools/unsymbolize" \ |
879 |
- "lib/Tools/getenv" \ |
880 |
- "lib/Tools/java" \ |
881 |
- "lib/Tools/make" \ |
882 |
- "lib/Tools/emacs" \ |
883 |
- "lib/Tools/scala" \ |
884 |
- "lib/Tools/print" \ |
885 |
- "lib/Tools/latex" \ |
886 |
- "lib/Tools/findlogics" \ |
887 |
- "lib/Tools/doc" \ |
888 |
- "lib/Tools/logo" \ |
889 |
- "lib/Tools/usedir" \ |
890 |
- "lib/Tools/yxml" \ |
891 |
- "lib/Tools/version" \ |
892 |
- "lib/Tools/makeall" \ |
893 |
- "lib/Tools/scalac" \ |
894 |
- "lib/Tools/document" \ |
895 |
- "lib/Tools/env" \ |
896 |
- "lib/Tools/display" \ |
897 |
- "lib/Tools/dimacs2hol" \ |
898 |
- "lib/scripts/keywords" \ |
899 |
- "lib/scripts/unsymbolize" \ |
900 |
- "lib/scripts/run-polyml" \ |
901 |
- "lib/scripts/run-smlnj" \ |
902 |
- "lib/scripts/feeder" \ |
903 |
- "lib/scripts/java_ext_dirs" \ |
904 |
- "lib/scripts/yxml" \ |
905 |
- "lib/scripts/raw_dump" \ |
906 |
- "lib/scripts/polyml-version" \ |
907 |
- "lib/scripts/process" |
908 |
- do |
909 |
- exeinto $(dirname "${TARGETDIR}/${i}") |
910 |
- doexe ${i} |
911 |
- done |
912 |
- |
913 |
- docompress -x /usr/share/doc/${PF} |
914 |
- dodoc -r doc |
915 |
- if use doc; then |
916 |
- dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc" |
917 |
- fi |
918 |
- |
919 |
- dodir /etc/isabelle |
920 |
- insinto /etc/isabelle |
921 |
- doins -r etc/* |
922 |
- |
923 |
- dosym /etc/isabelle "${TARGETDIR}/etc" |
924 |
- dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps" |
925 |
- |
926 |
- insinto ${LIBDIR} |
927 |
- doins -r heaps |
928 |
- |
929 |
- bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \ |
930 |
- || die "isabelle install failed" |
931 |
- newicon lib/icons/isabelle.xpm "${PN}.xpm" |
932 |
- dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README |
933 |
- |
934 |
- java-pkg_regjar \ |
935 |
- "${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \ |
936 |
- "${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \ |
937 |
- "${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \ |
938 |
- "${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \ |
939 |
- "${ED}${TARGETDIR}/lib/classes/java_ext_dirs.jar" |
940 |
-} |
941 |
- |
942 |
-pkg_postinst() { |
943 |
- # If any of the directories in /etc/isabelle/components do not exist, then |
944 |
- # even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to |
945 |
- # to delete any non-existing directories. If an old Isabelle version was |
946 |
- # installed with component ebuilds like sci-mathematics/e, then the |
947 |
- # Isabelle version is upgraded, then the contrib directories will not |
948 |
- # exist initially, it is necessary to delete them from /etc/isabelle/components. |
949 |
- # Then these components are rebuilt (creating these directories) using the |
950 |
- # EAPI=5 subslot depends. |
951 |
- for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components") |
952 |
- do |
953 |
- if [ ! -d /usr/share/Isabelle2012/${i} ]; then |
954 |
- sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components" |
955 |
- fi |
956 |
- done |
957 |
- if use ledit && use readline; then |
958 |
- elog "Both readline and ledit use flags specified. The default setting" |
959 |
- elog "if both are installed is to use readline (rlwrap), this can be" |
960 |
- elog "modfied by editing the ISABELLE_LINE_EDITOR setting in" |
961 |
- elog "${ROOT}/etc/isabelle/settings" |
962 |
- fi |
963 |
- elog "Please ensure you have a pdf viewer installed, for example:" |
964 |
- elog "As root: emerge app-text/zathura-pdf-poppler" |
965 |
- elog "Please configure your preferred pdf viewer, something like:" |
966 |
- elog "As normal user: xdg-mime default zathura.desktop application/pdf" |
967 |
- elog "Or alternatively by editing the PDF_VIEWER variable in the system" |
968 |
- elog "settings file ${ROOT}etc/isabelle/settings and/or the user" |
969 |
- elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings" |
970 |
- elog "To improve sledgehammer performance, consider installing:" |
971 |
- elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass" |
972 |
- elog "For nitpick it is necessary to install:" |
973 |
- elog "emerge sci-mathematics/kodkodi" |
974 |
-} |
975 |
|
976 |
diff --git a/sci-mathematics/isabelle/isabelle-2011.1.ebuild b/sci-mathematics/isabelle/isabelle-2011.1.ebuild |
977 |
deleted file mode 100644 |
978 |
index f0e0c82..0000000 |
979 |
--- a/sci-mathematics/isabelle/isabelle-2011.1.ebuild |
980 |
+++ /dev/null |
981 |
@@ -1,142 +0,0 @@ |
982 |
-# Copyright 1999-2012 Gentoo Foundation |
983 |
-# Distributed under the terms of the GNU General Public License v2 |
984 |
-# $Id$ |
985 |
- |
986 |
-EAPI="4" |
987 |
- |
988 |
-JAVA_PKG_OPT_USE="graphbrowsing" |
989 |
-inherit eutils java-pkg-opt-2 multilib versionator |
990 |
- |
991 |
-MY_PN="Isabelle" |
992 |
-MY_PV=$(replace_all_version_separators '-') |
993 |
-MY_P="${MY_PN}${MY_PV}" |
994 |
- |
995 |
-DESCRIPTION="Isabelle is a generic proof assistant" |
996 |
-HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html" |
997 |
-SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz" |
998 |
- |
999 |
-LICENSE="BSD" |
1000 |
-SLOT="0" |
1001 |
-KEYWORDS="~x86 ~amd64" |
1002 |
-ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents" |
1003 |
-IUSE="${ALL_LOGICS} doc graphbrowsing +proofgeneral test" |
1004 |
- |
1005 |
-#upstream says |
1006 |
-#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, |
1007 |
-#for document preparation: complete LaTeX |
1008 |
-DEPEND=">=app-shells/bash-3.0 |
1009 |
- >=dev-lang/polyml-5.4.1[-portable] |
1010 |
- >=dev-lang/perl-5.8.8-r2" |
1011 |
- |
1012 |
-RDEPEND="doc? ( |
1013 |
- virtual/latex-base |
1014 |
- dev-tex/rail |
1015 |
- ) |
1016 |
- proofgeneral? ( |
1017 |
- app-emacs/proofgeneral |
1018 |
- ) |
1019 |
- ${DEPEND}" |
1020 |
- |
1021 |
-S="${WORKDIR}"/Isabelle${MY_PV} |
1022 |
-TARGETDIR="/usr/share/Isabelle"${MY_PV} |
1023 |
-LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV} |
1024 |
- |
1025 |
-pkg_setup() { |
1026 |
- java-pkg-opt-2_pkg_setup |
1027 |
- if ! use proofgeneral |
1028 |
- then |
1029 |
- ewarn "You have deselected the Proof General interface." |
1030 |
- ewarn "Only a text terminal will be installed." |
1031 |
- ewarn "Emerge Isabelle with the proofgeneral USE flag enabled" |
1032 |
- ewarn "to get the common interface, that most people want." |
1033 |
- fi |
1034 |
-} |
1035 |
- |
1036 |
-src_prepare() { |
1037 |
- java-pkg-opt-2_src_prepare |
1038 |
- if use proofgeneral; then |
1039 |
- epatch "${FILESDIR}/${PN}-2011.1-proofgeneral-gentoo-path.patch" |
1040 |
- polymlver=$(poly -v | cut -d' ' -f2) |
1041 |
- polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1) |
1042 |
- sed -e "s@5.4.0@${polymlver}@g" \ |
1043 |
- -i "${S}/etc/settings" \ |
1044 |
- || die "Could not configure polyml version in etc/settings" |
1045 |
- sed -e "s@x86_64@${polymlarch}@g" \ |
1046 |
- -i "${S}/etc/settings" \ |
1047 |
- || die "Could not configure polyml arch in etc/settings" |
1048 |
- fi |
1049 |
- if use graphbrowsing; then |
1050 |
- epatch "${FILESDIR}/${PN}-2011.1-graphbrowser.patch" |
1051 |
- fi |
1052 |
-} |
1053 |
- |
1054 |
-src_compile() { |
1055 |
- LOGICS="" |
1056 |
- for l in "${ALL_LOGICS}"; do |
1057 |
- if has "${l/+/}"; then |
1058 |
- LOGICS="${LOGICS} ${l/+/}" |
1059 |
- fi |
1060 |
- done |
1061 |
- einfo "Building Isabelle logics ${LOGICS}. This may take some time." |
1062 |
- ./build -b -i "${LOGICS}" || die "building logics failed" |
1063 |
- ./bin/isabelle makeall || die "isabelle makeall failed" |
1064 |
- if use graphbrowsing |
1065 |
- then |
1066 |
- rm -f "${S}/lib/browser/GraphBrowser.jar" \ |
1067 |
- || die "failed cleaning graph browser directory" |
1068 |
- pushd "${S}/lib/browser" \ |
1069 |
- || die "Could not change directory to lib/browser" |
1070 |
- ./build || die "failed building the graph browser" |
1071 |
- popd |
1072 |
- fi |
1073 |
-} |
1074 |
- |
1075 |
-src_test() { |
1076 |
- einfo "Running tests. A test run can take up to several hours!" |
1077 |
- ./build -b -t || die "tests failed" |
1078 |
-} |
1079 |
- |
1080 |
-src_install() { |
1081 |
- exeinto ${TARGETDIR}/bin |
1082 |
- doexe bin/isabelle-process bin/isabelle |
1083 |
- |
1084 |
- exeinto ${TARGETDIR} |
1085 |
- doexe build |
1086 |
- |
1087 |
- insinto ${TARGETDIR} |
1088 |
- doins -r src |
1089 |
- dodoc -r doc |
1090 |
- |
1091 |
- dodir /etc/isabelle |
1092 |
- insinto /etc/isabelle |
1093 |
- doins -r etc/* |
1094 |
- |
1095 |
- dosym /etc/isabelle "${TARGETDIR}/etc" |
1096 |
- dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps" |
1097 |
- |
1098 |
- insinto ${LIBDIR} |
1099 |
- doins -r heaps |
1100 |
- |
1101 |
- # use cp to keep file attributes |
1102 |
- cp -R lib "${ED}${TARGETDIR}" || die "install lib failed" |
1103 |
- |
1104 |
- bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \ |
1105 |
- || die "isabelle install failed" |
1106 |
- newicon lib/icons/isabelle.xpm "${PN}.xpm" |
1107 |
- dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README |
1108 |
- |
1109 |
- java-pkg_regjar \ |
1110 |
- "${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \ |
1111 |
- "${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \ |
1112 |
- "${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \ |
1113 |
- "${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \ |
1114 |
- "${ED}${TARGETDIR}/lib/classes/java_ext_dirs.jar" |
1115 |
-} |
1116 |
- |
1117 |
-pkg_postinst() { |
1118 |
- elog "You will need to re-emerge Isabelle after emerging polyml." |
1119 |
- elog "Please configure your preferred pdf viewer by editing" |
1120 |
- elog "the PDF_VIEWER variable in the system settings file" |
1121 |
- elog "/etc/isabelle/settings and/or the user settings file" |
1122 |
- elog "\$HOME/.isabelle/${MY_P}/etc/settings" |
1123 |
-} |
1124 |
|
1125 |
diff --git a/sci-mathematics/isabelle/isabelle-2012-r1.ebuild b/sci-mathematics/isabelle/isabelle-2012-r1.ebuild |
1126 |
deleted file mode 100644 |
1127 |
index 087bb7e..0000000 |
1128 |
--- a/sci-mathematics/isabelle/isabelle-2012-r1.ebuild |
1129 |
+++ /dev/null |
1130 |
@@ -1,320 +0,0 @@ |
1131 |
-# Copyright 1999-2015 Gentoo Foundation |
1132 |
-# Distributed under the terms of the GNU General Public License v2 |
1133 |
-# $Id$ |
1134 |
- |
1135 |
-EAPI="5" |
1136 |
- |
1137 |
-inherit eutils java-pkg-2 multilib versionator |
1138 |
- |
1139 |
-MY_PN="Isabelle" |
1140 |
-MY_PV=$(replace_all_version_separators '-') |
1141 |
-MY_P="${MY_PN}${MY_PV}" |
1142 |
- |
1143 |
-JEDIT_PV="20120414" |
1144 |
-JEDIT_PN="jedit_build" |
1145 |
-JEDIT_P="${JEDIT_PN}-${JEDIT_PV}" |
1146 |
- |
1147 |
-DESCRIPTION="Isabelle is a generic proof assistant" |
1148 |
-HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html" |
1149 |
-SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz |
1150 |
- doc? ( https://dev.gentoo.org/~gienah/snapshots/${MY_P}-doc-src.tar.gz ) |
1151 |
- pide? ( http://www4.in.tum.de/~wenzelm/test/${JEDIT_P}.tar.gz )" |
1152 |
- |
1153 |
-LICENSE="BSD" |
1154 |
-SLOT="0/${PV}" |
1155 |
-KEYWORDS="~amd64 ~x86" |
1156 |
-ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents" |
1157 |
-IUSE="${ALL_LOGICS} doc graphbrowsing ledit readline pide +proofgeneral test" |
1158 |
- |
1159 |
-#upstream says |
1160 |
-#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, |
1161 |
-#for document preparation: complete LaTeX |
1162 |
-DEPEND=">=app-shells/bash-3.0:* |
1163 |
- >=dev-lang/polyml-5.4.1:=[-portable] |
1164 |
- >=dev-lang/perl-5.8.8-r2" |
1165 |
- |
1166 |
-RDEPEND="dev-perl/libwww-perl |
1167 |
- sci-mathematics/sha1-polyml |
1168 |
- doc? ( |
1169 |
- virtual/latex-base |
1170 |
- dev-tex/rail |
1171 |
- ) |
1172 |
- proofgeneral? ( |
1173 |
- app-emacs/proofgeneral |
1174 |
- ) |
1175 |
- pide? ( |
1176 |
- >=dev-lang/scala-2.8.2 |
1177 |
- ) |
1178 |
- ledit? ( |
1179 |
- app-misc/ledit |
1180 |
- ) |
1181 |
- readline? ( |
1182 |
- app-misc/rlwrap |
1183 |
- ) |
1184 |
- ${DEPEND}" |
1185 |
- |
1186 |
-S="${WORKDIR}"/Isabelle${MY_PV} |
1187 |
-JEDIT_S="${WORKDIR}/${JEDIT_P}" |
1188 |
-TARGETDIR="/usr/share/Isabelle"${MY_PV} |
1189 |
-LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV} |
1190 |
- |
1191 |
-pkg_setup() { |
1192 |
- java-pkg-2_pkg_setup |
1193 |
- if ! use proofgeneral |
1194 |
- then |
1195 |
- ewarn "You have deselected the Proof General interface." |
1196 |
- ewarn "Only a text terminal will be installed." |
1197 |
- ewarn "Emerge Isabelle with the proofgeneral USE flag enabled" |
1198 |
- ewarn "to get the common interface, that most people want." |
1199 |
- fi |
1200 |
-} |
1201 |
- |
1202 |
-src_prepare() { |
1203 |
- java-pkg-2_src_prepare |
1204 |
- epatch "${FILESDIR}/${PN}-2012-gentoo-settings.patch" |
1205 |
- # http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/2732 |
1206 |
- epatch "${FILESDIR}/${PN}-2012-signal-handling.patch" |
1207 |
- # http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/2780 |
1208 |
- epatch "${FILESDIR}/${PN}-2012-redundant-equations-in-function-definitions-error.patch" |
1209 |
- polymlver=$(poly -v | cut -d' ' -f2) |
1210 |
- polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1) |
1211 |
- sed -e "s@5.4.0@${polymlver}@g" \ |
1212 |
- -i "${S}/etc/settings" \ |
1213 |
- || die "Could not configure polyml version in etc/settings" |
1214 |
- sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \ |
1215 |
- -i "${S}/etc/settings" \ |
1216 |
- || die "Could not configure polyml ML_HOME in etc/settings" |
1217 |
- sed -e "s@x86_64@${polymlarch}@g" \ |
1218 |
- -i "${S}/etc/settings" \ |
1219 |
- || die "Could not configure polyml arch in etc/settings" |
1220 |
- sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \ |
1221 |
- -i "${S}/etc/settings" \ |
1222 |
- || die "Could not configure PROOFGENERAL_HOME in etc/settings" |
1223 |
- sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \ |
1224 |
- -i "${S}/etc/settings" \ |
1225 |
- || die "Could not configure Isabelle lib directory in etc/settings" |
1226 |
- epatch "${FILESDIR}/${PN}-2012-graphbrowser.patch" |
1227 |
- epatch "${FILESDIR}/${PN}-2012-libsha1.patch" |
1228 |
- cat <<- EOF >> "${S}/etc/settings" |
1229 |
- |
1230 |
- ISABELLE_GHC="${ROOT}usr/bin/ghc" |
1231 |
- ISABELLE_OCAML="${ROOT}usr/bin/ocaml" |
1232 |
- ISABELLE_SWIPL="${ROOT}usr/bin/swipl" |
1233 |
- ISABELLE_JDK_HOME="\$(java-config --jdk-home)" |
1234 |
- SCALA_HOME="${ROOT}usr/share/scala" |
1235 |
- SHA1_HOME="/usr/$(get_libdir)/sha1-polyml" |
1236 |
- EOF |
1237 |
- if use pide; then |
1238 |
- cat <<- EOF >> "${S}/etc/settings" |
1239 |
- ISABELLE_JEDIT_BUILD_HOME="\$ISABELLE_HOME/${JEDIT_P}" |
1240 |
- init_component ${JEDIT_S} |
1241 |
- EOF |
1242 |
- fi |
1243 |
- if use ledit && ! use readline; then |
1244 |
- epatch "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch" |
1245 |
- fi |
1246 |
-} |
1247 |
- |
1248 |
-src_compile() { |
1249 |
- LOGICS="" |
1250 |
- for l in "${ALL_LOGICS}"; do |
1251 |
- if has "${l/+/}"; then |
1252 |
- LOGICS="${LOGICS} ${l/+/}" |
1253 |
- fi |
1254 |
- done |
1255 |
- einfo "Building Isabelle logics ${LOGICS}. This may take some time." |
1256 |
- ./build -b -i "${LOGICS}" || die "building logics failed" |
1257 |
- ./bin/isabelle makeall || die "isabelle makeall failed" |
1258 |
- if use graphbrowsing |
1259 |
- then |
1260 |
- rm -f "${S}/lib/browser/GraphBrowser.jar" \ |
1261 |
- || die "failed cleaning graph browser directory" |
1262 |
- pushd "${S}/lib/browser" \ |
1263 |
- || die "Could not change directory to lib/browser" |
1264 |
- ./build || die "failed building the graph browser" |
1265 |
- popd |
1266 |
- fi |
1267 |
- if use pide; then |
1268 |
- pushd "${S}/src/Tools/jEdit" \ |
1269 |
- || die "Could not change directory to src/Tools/jEdit" |
1270 |
- "${S}"/bin/isabelle jedit -b -f \ |
1271 |
- || die "pide build failed" |
1272 |
- popd |
1273 |
- # The jedit_build stuff is only required to build |
1274 |
- # Isabelle/jEdit Prover IDE (PIDE). These 2 lines need to be deleted |
1275 |
- # from etc/settings as the jedit_build source code is not installed |
1276 |
- sed -e '/ISABELLE_JEDIT_BUILD_HOME/d' \ |
1277 |
- -e '/init_component/d' \ |
1278 |
- -i "${S}/etc/settings" \ |
1279 |
- || die "Could not delete jedit_build lines from etc/settings" |
1280 |
- fi |
1281 |
-} |
1282 |
- |
1283 |
-src_test() { |
1284 |
- einfo "Running tests. A test run can take up to several hours!" |
1285 |
- ./build -b -t || die "tests failed" |
1286 |
-} |
1287 |
- |
1288 |
-src_install() { |
1289 |
- exeinto ${TARGETDIR}/bin |
1290 |
- doexe bin/isabelle-process bin/isabelle |
1291 |
- |
1292 |
- insinto ${TARGETDIR} |
1293 |
- doins -r src |
1294 |
- doins -r lib |
1295 |
- |
1296 |
- docompress -x /usr/share/doc/${PF} |
1297 |
- dodoc -r doc |
1298 |
- if use doc; then |
1299 |
- dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc" |
1300 |
- # The build of sci-mathematics/haskabelle with use doc requires |
1301 |
- # sci-mathematics/isabelle[doc?]. The haskabelle doc build requires |
1302 |
- # the doc-src directory stuff in the isabelle package. Which is not |
1303 |
- # provided in the Isabelle 2012 src tarball. So extract it from a |
1304 |
- # snapshot of the isabelle repo taken soon after the Isabelle 2012 |
1305 |
- # release. |
1306 |
- doins -r doc-src |
1307 |
- for i in "./doc-src/IsarRef/showsymbols" \ |
1308 |
- "./doc-src/TutorialI/Overview/LNCS/makeDemo" \ |
1309 |
- "./doc-src/TutorialI/isa-index" \ |
1310 |
- "./doc-src/sedindex" |
1311 |
- do |
1312 |
- exeinto $(dirname "${TARGETDIR}/${i}") |
1313 |
- doexe ${i} |
1314 |
- done |
1315 |
- fi |
1316 |
- |
1317 |
- for i in "./build" \ |
1318 |
- "./src/Pure/mk" \ |
1319 |
- "./src/Pure/build-jars" \ |
1320 |
- "./src/Tools/JVM/build" \ |
1321 |
- "./src/Tools/JVM/java_ext_dirs" \ |
1322 |
- "./src/Tools/jEdit/lib/Tools/jedit" \ |
1323 |
- "./src/Tools/Metis/fix_metis_license" \ |
1324 |
- "./src/Tools/Metis/make_metis" \ |
1325 |
- "./src/Tools/Metis/scripts/mlpp" \ |
1326 |
- "./src/Tools/WWW_Find/lib/Tools/wwwfind" \ |
1327 |
- "./src/Tools/Code/lib/Tools/codegen" \ |
1328 |
- "./src/HOL/Mirabelle/lib/Tools/mirabelle" \ |
1329 |
- "./src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \ |
1330 |
- "./src/HOL/Tools/SMT/lib/scripts/remote_smt" \ |
1331 |
- "./src/HOL/Tools/ATP/scripts/remote_atp" \ |
1332 |
- "./src/HOL/Tools/ATP/scripts/spass" \ |
1333 |
- "./src/HOL/Mutabelle/lib/Tools/mutabelle" \ |
1334 |
- "./src/HOL/TPTP/TPTP_Parser/make_mlyacclib" \ |
1335 |
- "./src/HOL/TPTP/TPTP_Parser/make_tptp_parser" \ |
1336 |
- "./src/HOL/TPTP/lib/Tools/tptp_isabelle_demo" \ |
1337 |
- "./src/HOL/TPTP/lib/Tools/tptp_graph" \ |
1338 |
- "./src/HOL/TPTP/lib/Tools/tptp_isabelle_comp" \ |
1339 |
- "./src/HOL/TPTP/lib/Tools/tptp_refute" \ |
1340 |
- "./src/HOL/TPTP/lib/Tools/tptp_translate" \ |
1341 |
- "./src/HOL/TPTP/lib/Tools/tptp_sledgehammer" \ |
1342 |
- "./src/HOL/TPTP/lib/Tools/tptp_nitpick" \ |
1343 |
- "./src/HOL/Library/Sum_of_Squares/neos_csdp_client" \ |
1344 |
- "./src/HOL/IMP/export.sh" \ |
1345 |
- "./lib/browser/build" \ |
1346 |
- "./lib/Tools/tty" \ |
1347 |
- "./lib/Tools/mkproject" \ |
1348 |
- "./lib/Tools/keywords" \ |
1349 |
- "./lib/Tools/browser" \ |
1350 |
- "./lib/Tools/install" \ |
1351 |
- "./lib/Tools/mkdir" \ |
1352 |
- "./lib/Tools/unsymbolize" \ |
1353 |
- "./lib/Tools/getenv" \ |
1354 |
- "./lib/Tools/java" \ |
1355 |
- "./lib/Tools/make" \ |
1356 |
- "./lib/Tools/emacs" \ |
1357 |
- "./lib/Tools/scala" \ |
1358 |
- "./lib/Tools/print" \ |
1359 |
- "./lib/Tools/latex" \ |
1360 |
- "./lib/Tools/findlogics" \ |
1361 |
- "./lib/Tools/doc" \ |
1362 |
- "./lib/Tools/logo" \ |
1363 |
- "./lib/Tools/usedir" \ |
1364 |
- "./lib/Tools/yxml" \ |
1365 |
- "./lib/Tools/version" \ |
1366 |
- "./lib/Tools/makeall" \ |
1367 |
- "./lib/Tools/scalac" \ |
1368 |
- "./lib/Tools/document" \ |
1369 |
- "./lib/Tools/env" \ |
1370 |
- "./lib/Tools/display" \ |
1371 |
- "./lib/Tools/dimacs2hol" \ |
1372 |
- "./lib/scripts/keywords" \ |
1373 |
- "./lib/scripts/unsymbolize" \ |
1374 |
- "./lib/scripts/run-polyml" \ |
1375 |
- "./lib/scripts/run-smlnj" \ |
1376 |
- "./lib/scripts/feeder" \ |
1377 |
- "./lib/scripts/yxml" \ |
1378 |
- "./lib/scripts/polyml-version" \ |
1379 |
- "./lib/scripts/process" |
1380 |
- do |
1381 |
- exeinto $(dirname "${TARGETDIR}/${i}") |
1382 |
- doexe ${i} |
1383 |
- done |
1384 |
- |
1385 |
- dodir /etc/isabelle |
1386 |
- insinto /etc/isabelle |
1387 |
- doins -r etc/* |
1388 |
- |
1389 |
- dosym /etc/isabelle "${TARGETDIR}/etc" |
1390 |
- dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps" |
1391 |
- |
1392 |
- insinto ${LIBDIR} |
1393 |
- doins -r heaps |
1394 |
- |
1395 |
- bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \ |
1396 |
- || die "isabelle install failed" |
1397 |
- newicon lib/icons/isabelle.xpm "${PN}.xpm" |
1398 |
- dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README |
1399 |
- |
1400 |
- java-pkg_regjar \ |
1401 |
- "${ED}${TARGETDIR}/src/Tools/JVM/java_ext_dirs.jar" \ |
1402 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/QuickNotepad.jar" \ |
1403 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Console.jar" \ |
1404 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/ErrorList.jar" \ |
1405 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Hyperlinks.jar" \ |
1406 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/SideKick.jar" \ |
1407 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/cobra.jar" \ |
1408 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/js.jar" \ |
1409 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/scala-compiler.jar" \ |
1410 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" \ |
1411 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jedit.jar" \ |
1412 |
- "${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \ |
1413 |
- "${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \ |
1414 |
- "${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \ |
1415 |
- "${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" |
1416 |
-} |
1417 |
- |
1418 |
-pkg_postinst() { |
1419 |
- # If any of the directories in /etc/isabelle/components do not exist, then |
1420 |
- # even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to |
1421 |
- # to delete any non-existing directories. If an old Isabelle version was |
1422 |
- # installed with component ebuilds like sci-mathematics/e, then the |
1423 |
- # Isabelle version is upgraded, then the contrib directories will not |
1424 |
- # exist initially, it is necessary to delete them from /etc/isabelle/components. |
1425 |
- # Then these components are rebuilt (creating these directories) using the |
1426 |
- # EAPI=5 subslot depends. |
1427 |
- for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components") |
1428 |
- do |
1429 |
- if [ ! -d /usr/share/Isabelle2012/${i} ]; then |
1430 |
- sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components" |
1431 |
- fi |
1432 |
- done |
1433 |
- if use ledit && use readline; then |
1434 |
- elog "Both readline and ledit use flags specified. The default setting" |
1435 |
- elog "if both are installed is to use readline (rlwrap), this can be" |
1436 |
- elog "modfied by editing the ISABELLE_LINE_EDITOR setting in" |
1437 |
- elog "${ROOT}/etc/isabelle/settings" |
1438 |
- fi |
1439 |
- elog "Please ensure you have a pdf viewer installed, for example:" |
1440 |
- elog "As root: emerge app-text/zathura-pdf-poppler" |
1441 |
- elog "Please configure your preferred pdf viewer, something like:" |
1442 |
- elog "As normal user: xdg-mime default zathura.desktop application/pdf" |
1443 |
- elog "Or alternatively by editing the PDF_VIEWER variable in the system" |
1444 |
- elog "settings file ${ROOT}etc/isabelle/settings and/or the user" |
1445 |
- elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings" |
1446 |
- elog "To improve sledgehammer performance, consider installing:" |
1447 |
- elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass" |
1448 |
- elog "For nitpick it is necessary to install:" |
1449 |
- elog "emerge sci-mathematics/kodkodi" |
1450 |
-} |
1451 |
|
1452 |
diff --git a/sci-mathematics/isabelle/isabelle-2013-r2.ebuild b/sci-mathematics/isabelle/isabelle-2013-r2.ebuild |
1453 |
deleted file mode 100644 |
1454 |
index 6b5c7f6..0000000 |
1455 |
--- a/sci-mathematics/isabelle/isabelle-2013-r2.ebuild |
1456 |
+++ /dev/null |
1457 |
@@ -1,353 +0,0 @@ |
1458 |
-# Copyright 1999-2015 Gentoo Foundation |
1459 |
-# Distributed under the terms of the GNU General Public License v2 |
1460 |
-# $Id$ |
1461 |
- |
1462 |
-EAPI="5" |
1463 |
- |
1464 |
-inherit eutils java-pkg-2 multilib versionator |
1465 |
- |
1466 |
-MY_PN="Isabelle" |
1467 |
-MY_PV=$(replace_all_version_separators '-') |
1468 |
-MY_P="${MY_PN}${MY_PV}" |
1469 |
- |
1470 |
-JEDIT_PV="20130104" |
1471 |
-JEDIT_PN="jedit_build" |
1472 |
-JEDIT_P="${JEDIT_PN}-${JEDIT_PV}" |
1473 |
-JEDIT_IC_PN="${JEDIT_PN}-isabelle-component" |
1474 |
-JEDIT_IC_P="${JEDIT_IC_PN}-${JEDIT_PV}" |
1475 |
- |
1476 |
-JFREECHART_PV="1.0.14" |
1477 |
-JFREECHART_PN="jfreechart" |
1478 |
-JFREECHART_P="${JFREECHART_PN}-${JFREECHART_PV}" |
1479 |
-JFREECHART_IC_PN="${JFREECHART_PN}-isabelle-component" |
1480 |
-JFREECHART_IC_P="${JFREECHART_IC_PN}-${JFREECHART_PV}" |
1481 |
- |
1482 |
-SS="2.10" |
1483 |
- |
1484 |
-DESCRIPTION="Isabelle is a generic proof assistant" |
1485 |
-HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html" |
1486 |
-SRC_URI="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/${MY_P}.tar.gz |
1487 |
- http://isabelle.in.tum.de/components/${JEDIT_P}.tar.gz -> ${JEDIT_IC_P}.tar.gz |
1488 |
- http://isabelle.in.tum.de/components/${JFREECHART_P}.tar.gz -> ${JFREECHART_IC_P}.tar.gz" |
1489 |
- |
1490 |
-LICENSE="BSD" |
1491 |
-SLOT="0/${PV}" |
1492 |
-KEYWORDS="~amd64 ~x86" |
1493 |
-IUSE="doc graphbrowsing ledit readline proofgeneral" |
1494 |
- |
1495 |
-#upstream says |
1496 |
-#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, |
1497 |
-#for document preparation: complete LaTeX |
1498 |
-DEPEND=">=app-shells/bash-3.0:* |
1499 |
- dev-java/ant-core:0 |
1500 |
- >=dev-java/jcommon-1.0.18:1.0 |
1501 |
- >=dev-java/jfreechart-1.0.14:1.0 |
1502 |
- >=dev-java/itext-2.1.5:0 |
1503 |
- dev-java/xml-xmlbeans:1 |
1504 |
- >=dev-lang/ghc-7.6.3 |
1505 |
- >=dev-lang/polyml-5.5.0:=[-portable] |
1506 |
- >=dev-lang/perl-5.8.8-r2 |
1507 |
- dev-lang/swi-prolog |
1508 |
- virtual/jdk:1.7 |
1509 |
- doc? ( |
1510 |
- virtual/latex-base |
1511 |
- dev-tex/rail |
1512 |
- ) |
1513 |
- >=dev-lang/scala-2.10.2:${SS} |
1514 |
- ledit? ( |
1515 |
- app-misc/ledit |
1516 |
- ) |
1517 |
- readline? ( |
1518 |
- app-misc/rlwrap |
1519 |
- )" |
1520 |
- |
1521 |
-RDEPEND="dev-perl/libwww-perl |
1522 |
- sci-mathematics/sha1-polyml |
1523 |
- >=virtual/jre-1.7 |
1524 |
- proofgeneral? ( |
1525 |
- >=app-emacs/proofgeneral-4.1 |
1526 |
- ) |
1527 |
- ${DEPEND}" |
1528 |
- |
1529 |
-S="${WORKDIR}"/Isabelle${MY_PV} |
1530 |
-JEDIT_S="${WORKDIR}/${JEDIT_P}" |
1531 |
-JFREECHART_S="${WORKDIR}/${JFREECHART_P}" |
1532 |
-TARGETDIR="/usr/share/Isabelle"${MY_PV} |
1533 |
-LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV} |
1534 |
- |
1535 |
-LIBRARY_PKGS="scala-${SS},itext,jcommon-1.0,jfreechart-1.0,xml-xmlbeans-1" |
1536 |
- |
1537 |
-src_unpack() { |
1538 |
- unpack "${MY_P}.tar.gz" |
1539 |
- pushd "${S}/contrib" || die |
1540 |
- unpack ${JEDIT_IC_P}.tar.gz |
1541 |
- unpack ${JFREECHART_IC_P}.tar.gz |
1542 |
-} |
1543 |
- |
1544 |
-pkg_setup() { |
1545 |
- java-pkg-2_pkg_setup |
1546 |
-} |
1547 |
- |
1548 |
-src_prepare() { |
1549 |
- java-pkg-2_src_prepare |
1550 |
- java-pkg_getjars ${LIBRARY_PKGS} |
1551 |
- epatch "${FILESDIR}/${PN}-2013-gentoo-settings.patch" |
1552 |
- epatch "${FILESDIR}/${PN}-2013-classpath.patch" |
1553 |
- polymlver=$(poly -v | cut -d' ' -f2) |
1554 |
- polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1) |
1555 |
- sed -e "s@5.5.0@${polymlver}@g" \ |
1556 |
- -i "${S}/etc/settings" \ |
1557 |
- || die "Could not configure polyml version in etc/settings" |
1558 |
- sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \ |
1559 |
- -i "${S}/etc/settings" \ |
1560 |
- || die "Could not configure polyml ML_HOME in etc/settings" |
1561 |
- sed -e "s@x86_64@${polymlarch}@g" \ |
1562 |
- -i "${S}/etc/settings" \ |
1563 |
- || die "Could not configure polyml arch in etc/settings" |
1564 |
- sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \ |
1565 |
- -i "${S}/etc/settings" \ |
1566 |
- || die "Could not configure PROOFGENERAL_HOME in etc/settings" |
1567 |
- sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \ |
1568 |
- -i "${S}/etc/settings" \ |
1569 |
- || die "Could not configure Isabelle lib directory in etc/settings" |
1570 |
- epatch "${FILESDIR}/${PN}-2012-graphbrowser.patch" |
1571 |
- epatch "${FILESDIR}/${PN}-2012-libsha1.patch" |
1572 |
- # this example fails to compile with swi-prolog 6.5.2, so patch it so that |
1573 |
- # Isabelle will build, then reverse the patch so that the user can see the |
1574 |
- # original code. |
1575 |
- epatch "${FILESDIR}/${PN}-2013-HOL-Predicate_Compile_Examples.patch" |
1576 |
- cat <<- EOF >> "${S}/etc/settings" |
1577 |
- |
1578 |
- ISABELLE_GHC="${ROOT}usr/bin/ghc" |
1579 |
- ISABELLE_OCAML="${ROOT}usr/bin/ocaml" |
1580 |
- ISABELLE_SWIPL="${ROOT}usr/bin/swipl" |
1581 |
- ISABELLE_JDK_HOME="\$(java-config --jdk-home)" |
1582 |
- SCALA_HOME="${ROOT}usr/share/scala-${SS}" |
1583 |
- SHA1_HOME="/usr/$(get_libdir)/sha1-polyml" |
1584 |
- EOF |
1585 |
- cat <<- EOF >> "${S}/etc/components" |
1586 |
- #bundled components |
1587 |
- contrib/${JEDIT_P} |
1588 |
- contrib/${JFREECHART_P} |
1589 |
- EOF |
1590 |
- if use ledit && ! use readline; then |
1591 |
- epatch "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch" |
1592 |
- fi |
1593 |
- rm -f "${S}/contrib/jfreechart-1.0.14/lib/iText-2.1.5.jar" \ |
1594 |
- "${S}/contrib/jfreechart-1.0.14/lib/jfreechart-1.0.14.jar" \ |
1595 |
- "${S}/contrib/jfreechart-1.0.14/lib/jcommon-1.0.18.jar" \ |
1596 |
- "${S}/lib/classes/ext/scala-actors.jar" \ |
1597 |
- "${S}/lib/classes/ext/scala-compiler.jar" \ |
1598 |
- "${S}/lib/classes/ext/scala-library.jar" \ |
1599 |
- "${S}/lib/classes/ext/scala-reflect.jar" \ |
1600 |
- "${S}/lib/classes/ext/scala-swing.jar" \ |
1601 |
- || die "Could not rm bundled jar files supplied by Gentoo" |
1602 |
-} |
1603 |
- |
1604 |
-src_compile() { |
1605 |
- einfo "Building Isabelle. This may take some time." |
1606 |
- ./bin/isabelle build -a -b -s -v || die "isabelle build failed" |
1607 |
- epatch --reverse "${FILESDIR}/${PN}-2013-HOL-Predicate_Compile_Examples.patch" |
1608 |
- if use graphbrowsing |
1609 |
- then |
1610 |
- rm -f "${S}/lib/browser/GraphBrowser.jar" \ |
1611 |
- || die "failed cleaning graph browser directory" |
1612 |
- pushd "${S}/lib/browser" \ |
1613 |
- || die "Could not change directory to lib/browser" |
1614 |
- ./build || die "failed building the graph browser" |
1615 |
- popd |
1616 |
- fi |
1617 |
- ./bin/isabelle jedit -b -f || die "pide build failed" |
1618 |
-} |
1619 |
- |
1620 |
-src_install() { |
1621 |
- exeinto ${TARGETDIR}/bin |
1622 |
- doexe bin/isabelle-process bin/isabelle |
1623 |
- |
1624 |
- insinto ${TARGETDIR} |
1625 |
- doins -r src |
1626 |
- doins -r lib |
1627 |
- doins -r contrib |
1628 |
- doins ROOTS |
1629 |
- |
1630 |
- docompress -x /usr/share/doc/${PF} |
1631 |
- dodoc -r doc |
1632 |
- if use doc; then |
1633 |
- dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc" |
1634 |
- # The build of sci-mathematics/haskabelle with use doc requires |
1635 |
- # sci-mathematics/isabelle[doc?]. The haskabelle doc build requires |
1636 |
- # the src/Doc directory stuff in the isabelle package. |
1637 |
- doins -r src/Doc |
1638 |
- for i in "./src/Doc/Classes/document/build" \ |
1639 |
- "./src/Doc/Codegen/document/build" \ |
1640 |
- "./src/Doc/Functions/document/build" \ |
1641 |
- "./src/Doc/HOL/document/build" \ |
1642 |
- "./src/Doc/Intro/document/build" \ |
1643 |
- "./src/Doc/IsarImplementation/document/build" \ |
1644 |
- "./src/Doc/IsarRef/document/build" \ |
1645 |
- "./src/Doc/IsarRef/document/showsymbols" \ |
1646 |
- "./src/Doc/LaTeXsugar/document/build" \ |
1647 |
- "./src/Doc/Locales/document/build" \ |
1648 |
- "./src/Doc/Logics/document/build" \ |
1649 |
- "./src/Doc/Main/document/build" \ |
1650 |
- "./src/Doc/Nitpick/document/build" \ |
1651 |
- "./src/Doc/ProgProve/document/build" \ |
1652 |
- "./src/Doc/Ref/document/build" \ |
1653 |
- "./src/Doc/Sledgehammer/document/build" \ |
1654 |
- "./src/Doc/System/document/build" \ |
1655 |
- "./src/Doc/Tutorial/document/build" \ |
1656 |
- "./src/Doc/Tutorial/document/isa-index" \ |
1657 |
- "./src/Doc/ZF/document/build" \ |
1658 |
- "./src/Doc/fixbookmarks" \ |
1659 |
- "./src/Doc/prepare_document" \ |
1660 |
- "./src/Doc/sedindex" |
1661 |
- do |
1662 |
- exeinto $(dirname "${TARGETDIR}/${i}") |
1663 |
- doexe ${i} |
1664 |
- done |
1665 |
- fi |
1666 |
- |
1667 |
- for i in "./Isabelle " \ |
1668 |
- "./bin/isabelle" \ |
1669 |
- "./bin/isabelle-process" \ |
1670 |
- "./lib/Tools/browser" \ |
1671 |
- "./lib/Tools/build" \ |
1672 |
- "./lib/Tools/build_dialog" \ |
1673 |
- "./lib/Tools/components" \ |
1674 |
- "./lib/Tools/dimacs2hol" \ |
1675 |
- "./lib/Tools/display" \ |
1676 |
- "./lib/Tools/doc" \ |
1677 |
- "./lib/Tools/document" \ |
1678 |
- "./lib/Tools/emacs" \ |
1679 |
- "./lib/Tools/env" \ |
1680 |
- "./lib/Tools/findlogics" \ |
1681 |
- "./lib/Tools/getenv" \ |
1682 |
- "./lib/Tools/install" \ |
1683 |
- "./lib/Tools/java" \ |
1684 |
- "./lib/Tools/keywords" \ |
1685 |
- "./lib/Tools/latex" \ |
1686 |
- "./lib/Tools/logo" \ |
1687 |
- "./lib/Tools/make" \ |
1688 |
- "./lib/Tools/mkdir" \ |
1689 |
- "./lib/Tools/mkproject" \ |
1690 |
- "./lib/Tools/mkroot" \ |
1691 |
- "./lib/Tools/options" \ |
1692 |
- "./lib/Tools/print" \ |
1693 |
- "./lib/Tools/scala" \ |
1694 |
- "./lib/Tools/scalac" \ |
1695 |
- "./lib/Tools/tty" \ |
1696 |
- "./lib/Tools/unsymbolize" \ |
1697 |
- "./lib/Tools/usedir" \ |
1698 |
- "./lib/Tools/version" \ |
1699 |
- "./lib/Tools/yxml" \ |
1700 |
- "./lib/browser/build" \ |
1701 |
- "./lib/scripts/feeder" \ |
1702 |
- "./lib/scripts/getsettings" \ |
1703 |
- "./lib/scripts/keywords" \ |
1704 |
- "./lib/scripts/polyml-version" \ |
1705 |
- "./lib/scripts/process" \ |
1706 |
- "./lib/scripts/run-polyml" \ |
1707 |
- "./lib/scripts/run-smlnj" \ |
1708 |
- "./lib/scripts/unsymbolize" \ |
1709 |
- "./lib/scripts/yxml" \ |
1710 |
- "./src/HOL/IMP/export.sh" \ |
1711 |
- "./src/HOL/Library/Sum_of_Squares/neos_csdp_client" \ |
1712 |
- "./src/HOL/Mirabelle/lib/Tools/mirabelle" \ |
1713 |
- "./src/HOL/Mutabelle/lib/Tools/mutabelle" \ |
1714 |
- "./src/HOL/SPARK/Examples/README" \ |
1715 |
- "./src/HOL/TPTP/TPTP_Parser/make_mlyacclib" \ |
1716 |
- "./src/HOL/TPTP/TPTP_Parser/make_tptp_parser" \ |
1717 |
- "./src/HOL/TPTP/lib/Tools/tptp_graph" \ |
1718 |
- "./src/HOL/TPTP/lib/Tools/tptp_isabelle" \ |
1719 |
- "./src/HOL/TPTP/lib/Tools/tptp_isabelle_hot" \ |
1720 |
- "./src/HOL/TPTP/lib/Tools/tptp_nitpick" \ |
1721 |
- "./src/HOL/TPTP/lib/Tools/tptp_refute" \ |
1722 |
- "./src/HOL/TPTP/lib/Tools/tptp_sledgehammer" \ |
1723 |
- "./src/HOL/Tools/ATP/scripts/dummy_atp" \ |
1724 |
- "./src/HOL/Tools/ATP/scripts/remote_atp" \ |
1725 |
- "./src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \ |
1726 |
- "./src/HOL/Tools/SMT/lib/scripts/remote_smt" \ |
1727 |
- "./src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py" \ |
1728 |
- "./src/HOL/Tools/Sledgehammer/MaSh/src/mash.py" \ |
1729 |
- "./src/Pure/build" \ |
1730 |
- "./src/Pure/build-jars" \ |
1731 |
- "./src/Tools/Code/lib/Tools/codegen" \ |
1732 |
- "./src/Tools/Graphview/lib/Tools/graphview" \ |
1733 |
- "./src/Tools/Metis/fix_metis_license" \ |
1734 |
- "./src/Tools/Metis/make_metis" \ |
1735 |
- "./src/Tools/Metis/scripts/mlpp" \ |
1736 |
- "./src/Tools/WWW_Find/lib/Tools/wwwfind" \ |
1737 |
- "./src/Tools/jEdit/lib/Tools/jedit" |
1738 |
- do |
1739 |
- exeinto $(dirname "${TARGETDIR}/${i}") |
1740 |
- doexe ${i} |
1741 |
- done |
1742 |
- |
1743 |
- insinto /etc/isabelle |
1744 |
- doins -r etc/* |
1745 |
- dosym /etc/isabelle "${TARGETDIR}/etc" |
1746 |
- |
1747 |
- dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps" |
1748 |
- insinto ${LIBDIR} |
1749 |
- doins -r heaps |
1750 |
- |
1751 |
- bin/isabelle install -d ${TARGETDIR} "${ED}usr/bin" \ |
1752 |
- || die "isabelle install failed" |
1753 |
- newicon lib/icons/isabelle.xpm "${PN}.xpm" |
1754 |
- dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README |
1755 |
- |
1756 |
- java-pkg_regjar \ |
1757 |
- "${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/Highlight.jar" \ |
1758 |
- "${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/ErrorList.jar" \ |
1759 |
- "${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/Console.jar" \ |
1760 |
- "${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/cobra.jar" \ |
1761 |
- "${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/js.jar" \ |
1762 |
- "${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/jedit-5.0.0-patched/jedit.jar" \ |
1763 |
- "${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/jedit-5.0.0-patched/jars/QuickNotepad.jar" \ |
1764 |
- "${ED}${TARGETDIR}/contrib/jfreechart-1.0.14/jfreechart-1.0.14-demo.jar" \ |
1765 |
- "${ED}${TARGETDIR}/lib/classes/ext/Graphview.jar" \ |
1766 |
- "${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \ |
1767 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Console.jar" \ |
1768 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/ErrorList.jar" \ |
1769 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Highlight.jar" \ |
1770 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" \ |
1771 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/QuickNotepad.jar" \ |
1772 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/SideKick.jar" \ |
1773 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/cobra.jar" \ |
1774 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/js.jar" \ |
1775 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jedit.jar" |
1776 |
-} |
1777 |
- |
1778 |
-pkg_postinst() { |
1779 |
- # If any of the directories in /etc/isabelle/components do not exist, then |
1780 |
- # even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to |
1781 |
- # to delete any non-existing directories. If an old Isabelle version was |
1782 |
- # installed with component ebuilds like sci-mathematics/e, then the |
1783 |
- # Isabelle version is upgraded, then the contrib directories will not |
1784 |
- # exist initially, it is necessary to delete them from /etc/isabelle/components. |
1785 |
- # Then these components are rebuilt (creating these directories) using the |
1786 |
- # EAPI=5 subslot depends. |
1787 |
- for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components") |
1788 |
- do |
1789 |
- if [ ! -d /usr/share/${MY_P}/${i} ]; then |
1790 |
- sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components" |
1791 |
- fi |
1792 |
- done |
1793 |
- if use ledit && use readline; then |
1794 |
- elog "Both readline and ledit use flags specified. The default setting" |
1795 |
- elog "if both are installed is to use readline (rlwrap), this can be" |
1796 |
- elog "modfied by editing the ISABELLE_LINE_EDITOR setting in" |
1797 |
- elog "${ROOT}/etc/isabelle/settings" |
1798 |
- fi |
1799 |
- elog "Please ensure you have a pdf viewer installed, for example:" |
1800 |
- elog "As root: emerge app-text/zathura-pdf-poppler" |
1801 |
- elog "Please configure your preferred pdf viewer, something like:" |
1802 |
- elog "As normal user: xdg-mime default zathura.desktop application/pdf" |
1803 |
- elog "Or alternatively by editing the PDF_VIEWER variable in the system" |
1804 |
- elog "settings file ${ROOT}etc/isabelle/settings and/or the user" |
1805 |
- elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings" |
1806 |
- elog "To improve sledgehammer performance, consider installing:" |
1807 |
- elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass" |
1808 |
- elog "For nitpick it is necessary to install:" |
1809 |
- elog "emerge sci-mathematics/kodkodi" |
1810 |
-} |
1811 |
|
1812 |
diff --git a/sci-mathematics/isabelle/isabelle-2013.2-r1.ebuild b/sci-mathematics/isabelle/isabelle-2013.2-r1.ebuild |
1813 |
deleted file mode 100644 |
1814 |
index 601509a..0000000 |
1815 |
--- a/sci-mathematics/isabelle/isabelle-2013.2-r1.ebuild |
1816 |
+++ /dev/null |
1817 |
@@ -1,375 +0,0 @@ |
1818 |
-# Copyright 1999-2015 Gentoo Foundation |
1819 |
-# Distributed under the terms of the GNU General Public License v2 |
1820 |
-# $Id$ |
1821 |
- |
1822 |
-EAPI="5" |
1823 |
- |
1824 |
-inherit eutils java-pkg-2 multilib versionator |
1825 |
- |
1826 |
-MY_PN="Isabelle" |
1827 |
-MY_PV=$(replace_all_version_separators '-') |
1828 |
-MY_P="${MY_PN}${MY_PV}" |
1829 |
- |
1830 |
-JEDIT_PV="20131106" |
1831 |
-JEDIT_PN="jedit_build" |
1832 |
-JEDIT_P="${JEDIT_PN}-${JEDIT_PV}" |
1833 |
-JEDIT_IC_PN="${JEDIT_PN}-isabelle-component" |
1834 |
-JEDIT_IC_P="${JEDIT_IC_PN}-${JEDIT_PV}" |
1835 |
- |
1836 |
-JFREECHART_PV="1.0.14-1" |
1837 |
-JFREECHART_PN="jfreechart" |
1838 |
-JFREECHART_P="${JFREECHART_PN}-${JFREECHART_PV}" |
1839 |
-JFREECHART_IC_PN="${JFREECHART_PN}-isabelle-component" |
1840 |
-JFREECHART_IC_P="${JFREECHART_IC_PN}-${JFREECHART_PV}" |
1841 |
- |
1842 |
-POLYML_PV="5.5.1-1" |
1843 |
-POLYML_PN="polyml" |
1844 |
-POLYML_P="${POLYML_PN}-${POLYML_PV}" |
1845 |
-POLYML_IC_PN="${POLYML_PN}-isabelle-component" |
1846 |
-POLYML_IC_P="${POLYML_IC_PN}-${POLYML_PV}" |
1847 |
- |
1848 |
-SS="2.11" |
1849 |
- |
1850 |
-DESCRIPTION="Isabelle is a generic proof assistant" |
1851 |
-HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html" |
1852 |
-SRC_URI="http://www.cl.cam.ac.uk/users/lcp/archive/${MY_P}.tar.gz |
1853 |
- http://isabelle.in.tum.de/components/${JEDIT_P}.tar.gz -> ${JEDIT_IC_P}.tar.gz |
1854 |
- http://isabelle.in.tum.de/dist/contrib/${JFREECHART_P}.tar.gz -> ${JFREECHART_IC_P}.tar.gz |
1855 |
- https://dev.gentoo.org/~gienah/snapshots/${POLYML_IC_P}.tar.gz" |
1856 |
- |
1857 |
-LICENSE="BSD" |
1858 |
-SLOT="0/${PV}" |
1859 |
-KEYWORDS="~amd64 ~x86" |
1860 |
-IUSE="doc graphbrowsing ledit readline proofgeneral" |
1861 |
- |
1862 |
-#upstream says |
1863 |
-#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, |
1864 |
-#for document preparation: complete LaTeX |
1865 |
-DEPEND=">=app-shells/bash-3.0:* |
1866 |
- dev-java/ant-core:0 |
1867 |
- >=dev-java/jcommon-1.0.18:1.0 |
1868 |
- >=dev-java/jfreechart-1.0.14:1.0 |
1869 |
- >=dev-java/itext-2.1.5:0 |
1870 |
- dev-java/xml-xmlbeans:1 |
1871 |
- dev-java/xz-java:0 |
1872 |
- >=dev-lang/ghc-7.6.3 |
1873 |
- >=dev-lang/polyml-5.5.1:=[-portable] |
1874 |
- >=dev-lang/perl-5.8.8-r2 |
1875 |
- dev-lang/swi-prolog |
1876 |
- virtual/jdk:1.7 |
1877 |
- doc? ( |
1878 |
- virtual/latex-base |
1879 |
- dev-tex/rail |
1880 |
- ) |
1881 |
- >=dev-lang/scala-2.11.1:${SS} |
1882 |
- ledit? ( |
1883 |
- app-misc/ledit |
1884 |
- ) |
1885 |
- readline? ( |
1886 |
- app-misc/rlwrap |
1887 |
- )" |
1888 |
- |
1889 |
-RDEPEND="dev-perl/libwww-perl |
1890 |
- sci-mathematics/sha1-polyml |
1891 |
- >=virtual/jre-1.7 |
1892 |
- proofgeneral? ( |
1893 |
- >=app-emacs/proofgeneral-4.1 |
1894 |
- ) |
1895 |
- ${DEPEND}" |
1896 |
- |
1897 |
-S="${WORKDIR}"/Isabelle${MY_PV} |
1898 |
-JEDIT_S="${WORKDIR}/${JEDIT_P}" |
1899 |
-JFREECHART_S="${WORKDIR}/${JFREECHART_P}" |
1900 |
-TARGETDIR="/usr/share/Isabelle"${MY_PV} |
1901 |
-LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV} |
1902 |
- |
1903 |
-# Notes on QA warnings: * Class files not found via DEPEND in package.env |
1904 |
-# Stuff with $ in the name appear to be spurious: |
1905 |
-# isabelle/Markup_Tree$$anonfun$results$1$1.class |
1906 |
-# scala/tools/nsc/backend/jvm/GenJVM$BytecodeGenerator$$anonfun$computeLocalVarsIndex$1.class |
1907 |
-# It wants javafx, I am unsure how to fix this. I test isabelle with the Sun JDK: |
1908 |
-# javafx/application/Platform.class javafx |
1909 |
-# Presumably the user can provide the jEdit plugins if they are necessary: |
1910 |
-# marker/MarkerSetsPlugin.class http://plugins.jedit.org/plugins/?MarkerSets |
1911 |
-# projectviewer/gui/OptionPaneBase.class http://plugins.jedit.org/plugins/?ProjectViewer |
1912 |
- |
1913 |
-LIBRARY_PKGS="ant-core,itext,jcommon-1.0,jfreechart-1.0,scala-${SS},xml-xmlbeans-1,xz-java" |
1914 |
- |
1915 |
-src_unpack() { |
1916 |
- unpack "${MY_P}.tar.gz" |
1917 |
- pushd "${S}/contrib" || die |
1918 |
- unpack ${JEDIT_IC_P}.tar.gz |
1919 |
- unpack ${JFREECHART_IC_P}.tar.gz |
1920 |
- unpack ${POLYML_IC_P}.tar.gz |
1921 |
-} |
1922 |
- |
1923 |
-pkg_setup() { |
1924 |
- java-pkg-2_pkg_setup |
1925 |
-} |
1926 |
- |
1927 |
-src_prepare() { |
1928 |
- java-pkg-2_src_prepare |
1929 |
- java-pkg_getjars ${LIBRARY_PKGS} |
1930 |
- epatch "${FILESDIR}/${PN}-2013-gentoo-settings.patch" |
1931 |
- epatch "${FILESDIR}/${PN}-2013.2-classpath.patch" |
1932 |
- polymlver=$(poly -v | cut -d' ' -f2) |
1933 |
- polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1) |
1934 |
- sed -e "s@5.5.0@${polymlver}@g" \ |
1935 |
- -i "${S}/etc/settings" \ |
1936 |
- || die "Could not configure polyml version in etc/settings" |
1937 |
- sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \ |
1938 |
- -i "${S}/etc/settings" \ |
1939 |
- || die "Could not configure polyml ML_HOME in etc/settings" |
1940 |
- sed -e "s@x86_64@${polymlarch}@g" \ |
1941 |
- -i "${S}/etc/settings" \ |
1942 |
- || die "Could not configure polyml arch in etc/settings" |
1943 |
- sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \ |
1944 |
- -i "${S}/etc/settings" \ |
1945 |
- || die "Could not configure PROOFGENERAL_HOME in etc/settings" |
1946 |
- sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \ |
1947 |
- -i "${S}/etc/settings" \ |
1948 |
- || die "Could not configure Isabelle lib directory in etc/settings" |
1949 |
- epatch "${FILESDIR}/${PN}-2012-graphbrowser.patch" |
1950 |
- epatch "${FILESDIR}/${PN}-2012-libsha1.patch" |
1951 |
- # this example fails to compile with swi-prolog 6.5.2, so patch it so that |
1952 |
- # Isabelle will build, then reverse the patch so that the user can see the |
1953 |
- # original code. |
1954 |
- epatch "${FILESDIR}/${PN}-2013.2-HOL-Predicate_Compile_Examples.patch" |
1955 |
- cat <<- EOF >> "${S}/etc/settings" |
1956 |
- |
1957 |
- ISABELLE_GHC="${ROOT}usr/bin/ghc" |
1958 |
- ISABELLE_OCAML="${ROOT}usr/bin/ocaml" |
1959 |
- ISABELLE_SWIPL="${ROOT}usr/bin/swipl" |
1960 |
- ISABELLE_JDK_HOME="\$(java-config --jdk-home)" |
1961 |
- SCALA_HOME="${ROOT}usr/share/scala-${SS}" |
1962 |
- SHA1_HOME="/usr/$(get_libdir)/sha1-polyml" |
1963 |
- EOF |
1964 |
- cat <<- EOF >> "${S}/etc/components" |
1965 |
- #bundled components |
1966 |
- contrib/${JEDIT_P} |
1967 |
- contrib/${JFREECHART_P} |
1968 |
- contrib/${POLYML_P} |
1969 |
- EOF |
1970 |
- if use ledit && ! use readline; then |
1971 |
- epatch "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch" |
1972 |
- fi |
1973 |
- rm -f "${S}/contrib/jfreechart-1.0.14-1/lib/iText-2.1.5.jar" \ |
1974 |
- "${S}/contrib/jfreechart-1.0.14-1/lib/jfreechart-1.0.14.jar" \ |
1975 |
- "${S}/contrib/jfreechart-1.0.14-1/lib/jcommon-1.0.18.jar" \ |
1976 |
- "${S}/lib/classes/ext/scala-actors.jar" \ |
1977 |
- "${S}/lib/classes/ext/scala-compiler.jar" \ |
1978 |
- "${S}/lib/classes/ext/scala-library.jar" \ |
1979 |
- "${S}/lib/classes/ext/scala-reflect.jar" \ |
1980 |
- "${S}/lib/classes/ext/scala-swing.jar" \ |
1981 |
- || die "Could not rm bundled jar files supplied by Gentoo" |
1982 |
-} |
1983 |
- |
1984 |
-src_compile() { |
1985 |
- einfo "Building Isabelle. This may take some time." |
1986 |
- ./bin/isabelle build -a -b -s -v || die "isabelle build failed" |
1987 |
- epatch --reverse "${FILESDIR}/${PN}-2013.2-HOL-Predicate_Compile_Examples.patch" |
1988 |
- if use graphbrowsing |
1989 |
- then |
1990 |
- rm -f "${S}/lib/browser/GraphBrowser.jar" \ |
1991 |
- || die "failed cleaning graph browser directory" |
1992 |
- pushd "${S}/lib/browser" \ |
1993 |
- || die "Could not change directory to lib/browser" |
1994 |
- ./build || die "failed building the graph browser" |
1995 |
- popd |
1996 |
- fi |
1997 |
- ./bin/isabelle jedit -b -f || die "pide build failed" |
1998 |
-} |
1999 |
- |
2000 |
-src_install() { |
2001 |
- insinto ${TARGETDIR} |
2002 |
- doins -r src |
2003 |
- doins -r lib |
2004 |
- doins -r contrib |
2005 |
- doins ROOTS |
2006 |
- |
2007 |
- docompress -x /usr/share/doc/${PF} |
2008 |
- dodoc -r doc |
2009 |
- if use doc; then |
2010 |
- dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc" |
2011 |
- # The build of sci-mathematics/haskabelle with use doc requires |
2012 |
- # sci-mathematics/isabelle[doc?]. The haskabelle doc build requires |
2013 |
- # the src/Doc directory stuff in the isabelle package. |
2014 |
- doins -r src/Doc |
2015 |
- for i in "./src/Doc/Classes/document/build" \ |
2016 |
- "./src/Doc/Codegen/document/build" \ |
2017 |
- "./src/Doc/Datatypes/document/build" \ |
2018 |
- "./src/Doc/fixbookmarks" \ |
2019 |
- "./src/Doc/Functions/document/build" \ |
2020 |
- "./src/Doc/Intro/document/build" \ |
2021 |
- "./src/Doc/IsarImplementation/document/build" \ |
2022 |
- "./src/Doc/IsarRef/document/build" \ |
2023 |
- "./src/Doc/IsarRef/document/showsymbols" \ |
2024 |
- "./src/Doc/JEdit/document/build" \ |
2025 |
- "./src/Doc/LaTeXsugar/document/build" \ |
2026 |
- "./src/Doc/Locales/document/build" \ |
2027 |
- "./src/Doc/Logics/document/build" \ |
2028 |
- "./src/Doc/Main/document/build" \ |
2029 |
- "./src/Doc/Nitpick/document/build" \ |
2030 |
- "./src/Doc/prepare_document" \ |
2031 |
- "./src/Doc/ProgProve/document/build" \ |
2032 |
- "./src/Doc/sedindex" \ |
2033 |
- "./src/Doc/Sledgehammer/document/build" \ |
2034 |
- "./src/Doc/System/document/build" \ |
2035 |
- "./src/Doc/Tutorial/document/build" \ |
2036 |
- "./src/Doc/Tutorial/document/isa-index" \ |
2037 |
- "./src/Doc/ZF/document/build" |
2038 |
- do |
2039 |
- exeinto $(dirname "${TARGETDIR}/${i}") |
2040 |
- doexe ${i} |
2041 |
- done |
2042 |
- fi |
2043 |
- |
2044 |
- for i in "./bin/isabelle" \ |
2045 |
- "./bin/isabelle-process" \ |
2046 |
- "./bin/isabelle_scala_script" \ |
2047 |
- "./lib/browser/build" \ |
2048 |
- "./lib/scripts/feeder" \ |
2049 |
- "./lib/scripts/getsettings" \ |
2050 |
- "./lib/scripts/polyml-version" \ |
2051 |
- "./lib/scripts/process" \ |
2052 |
- "./lib/scripts/run-polyml" \ |
2053 |
- "./lib/scripts/run-polyml-5.5.1" \ |
2054 |
- "./lib/scripts/run-smlnj" \ |
2055 |
- "./lib/scripts/unsymbolize" \ |
2056 |
- "./lib/scripts/update_sub_sup" \ |
2057 |
- "./lib/scripts/yxml" \ |
2058 |
- "./lib/Tools/browser" \ |
2059 |
- "./lib/Tools/build" \ |
2060 |
- "./lib/Tools/components" \ |
2061 |
- "./lib/Tools/display" \ |
2062 |
- "./lib/Tools/doc" \ |
2063 |
- "./lib/Tools/document" \ |
2064 |
- "./lib/Tools/emacs" \ |
2065 |
- "./lib/Tools/env" \ |
2066 |
- "./lib/Tools/findlogics" \ |
2067 |
- "./lib/Tools/getenv" \ |
2068 |
- "./lib/Tools/install" \ |
2069 |
- "./lib/Tools/java" \ |
2070 |
- "./lib/Tools/keywords" \ |
2071 |
- "./lib/Tools/latex" \ |
2072 |
- "./lib/Tools/logo" \ |
2073 |
- "./lib/Tools/mkroot" \ |
2074 |
- "./lib/Tools/options" \ |
2075 |
- "./lib/Tools/scala" \ |
2076 |
- "./lib/Tools/scalac" \ |
2077 |
- "./lib/Tools/tty" \ |
2078 |
- "./lib/Tools/unsymbolize" \ |
2079 |
- "./lib/Tools/update_sub_sup" \ |
2080 |
- "./lib/Tools/version" \ |
2081 |
- "./lib/Tools/yxml" \ |
2082 |
- "./src/HOL/IMP/export.sh" \ |
2083 |
- "./src/HOL/Library/Sum_of_Squares/neos_csdp_client" \ |
2084 |
- "./src/HOL/Mirabelle/lib/Tools/mirabelle" \ |
2085 |
- "./src/HOL/Mutabelle/lib/Tools/mutabelle" \ |
2086 |
- "./src/HOL/SPARK/Examples/README" \ |
2087 |
- "./src/HOL/Tools/ATP/scripts/dummy_atp" \ |
2088 |
- "./src/HOL/Tools/ATP/scripts/remote_atp" \ |
2089 |
- "./src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py" \ |
2090 |
- "./src/HOL/Tools/Sledgehammer/MaSh/src/mash.py" \ |
2091 |
- "./src/HOL/Tools/Sledgehammer/MaSh/src/server.py" \ |
2092 |
- "./src/HOL/Tools/SMT/lib/scripts/remote_smt" \ |
2093 |
- "./src/HOL/TPTP/lib/Tools/tptp_graph" \ |
2094 |
- "./src/HOL/TPTP/lib/Tools/tptp_isabelle" \ |
2095 |
- "./src/HOL/TPTP/lib/Tools/tptp_isabelle_hot" \ |
2096 |
- "./src/HOL/TPTP/lib/Tools/tptp_nitpick" \ |
2097 |
- "./src/HOL/TPTP/lib/Tools/tptp_refute" \ |
2098 |
- "./src/HOL/TPTP/lib/Tools/tptp_sledgehammer" \ |
2099 |
- "./src/HOL/TPTP/TPTP_Parser/make_mlyacclib" \ |
2100 |
- "./src/HOL/TPTP/TPTP_Parser/make_tptp_parser" \ |
2101 |
- "./src/Pure/build" \ |
2102 |
- "./src/Pure/build-jars" \ |
2103 |
- "./src/Tools/Code/lib/Tools/codegen" \ |
2104 |
- "./src/Tools/Graphview/lib/Tools/graphview" \ |
2105 |
- "./src/Tools/jEdit/lib/Tools/jedit" \ |
2106 |
- "./src/Tools/Metis/fix_metis_license" \ |
2107 |
- "./src/Tools/Metis/make_metis" \ |
2108 |
- "./src/Tools/Metis/scripts/mlpp" \ |
2109 |
- "./src/Tools/WWW_Find/lib/Tools/wwwfind" |
2110 |
- do |
2111 |
- exeinto $(dirname "${TARGETDIR}/${i}") |
2112 |
- doexe ${i} |
2113 |
- done |
2114 |
- |
2115 |
- insinto /etc/isabelle |
2116 |
- doins -r etc/* |
2117 |
- dosym /etc/isabelle "${TARGETDIR}/etc" |
2118 |
- |
2119 |
- dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps" |
2120 |
- insinto ${LIBDIR} |
2121 |
- doins -r heaps |
2122 |
- |
2123 |
- bin/isabelle install -d ${TARGETDIR} "${ED}usr/bin" \ |
2124 |
- || die "isabelle install failed" |
2125 |
- newicon lib/icons/"${PN}.xpm" "${PN}.xpm" |
2126 |
- newicon lib/icons/"${PN}-mini.xpm" "${PN}-mini.xpm" |
2127 |
- dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README |
2128 |
- |
2129 |
- java-pkg_regjar \ |
2130 |
- "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/Console.jar" \ |
2131 |
- "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/ErrorList.jar" \ |
2132 |
- "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/Highlight.jar" \ |
2133 |
- "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/idea-icons.jar" \ |
2134 |
- "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/jedit-5.1.0-patched/jars/QuickNotepad.jar" \ |
2135 |
- "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/jedit-5.1.0-patched/jedit.jar" \ |
2136 |
- "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/jsr305-2.0.0.jar" \ |
2137 |
- "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/MacOSX.jar" \ |
2138 |
- "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/SideKick.jar" \ |
2139 |
- "${ED}${TARGETDIR}/contrib/${JFREECHART_P}/jfreechart-1.0.14-demo.jar" \ |
2140 |
- "${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \ |
2141 |
- "${ED}${TARGETDIR}/lib/classes/Graphview.jar" \ |
2142 |
- "${ED}${TARGETDIR}/lib/classes/Pure.jar" \ |
2143 |
- "${ED}${TARGETDIR}/lib/classes/scala-actors.jar" \ |
2144 |
- "${ED}${TARGETDIR}/lib/classes/scala-compiler.jar" \ |
2145 |
- "${ED}${TARGETDIR}/lib/classes/scala-library.jar" \ |
2146 |
- "${ED}${TARGETDIR}/lib/classes/scala-reflect.jar" \ |
2147 |
- "${ED}${TARGETDIR}/lib/classes/scala-swing.jar" \ |
2148 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Console.jar" \ |
2149 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/ErrorList.jar" \ |
2150 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Highlight.jar" \ |
2151 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/idea-icons.jar" \ |
2152 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" \ |
2153 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/jsr305-2.0.0.jar" \ |
2154 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/MacOSX.jar" \ |
2155 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/QuickNotepad.jar" \ |
2156 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/SideKick.jar" \ |
2157 |
- "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jedit.jar" |
2158 |
-} |
2159 |
- |
2160 |
-pkg_postinst() { |
2161 |
- # If any of the directories in /etc/isabelle/components do not exist, then |
2162 |
- # even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to |
2163 |
- # to delete any non-existing directories. If an old Isabelle version was |
2164 |
- # installed with component ebuilds like sci-mathematics/e, then the |
2165 |
- # Isabelle version is upgraded, then the contrib directories will not |
2166 |
- # exist initially, it is necessary to delete them from /etc/isabelle/components. |
2167 |
- # Then these components are rebuilt (creating these directories) using the |
2168 |
- # EAPI=5 subslot depends. |
2169 |
- for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components") |
2170 |
- do |
2171 |
- if [ ! -d /usr/share/${MY_P}/${i} ]; then |
2172 |
- sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components" |
2173 |
- fi |
2174 |
- done |
2175 |
- if use ledit && use readline; then |
2176 |
- elog "Both readline and ledit use flags specified. The default setting" |
2177 |
- elog "if both are installed is to use readline (rlwrap), this can be" |
2178 |
- elog "modfied by editing the ISABELLE_LINE_EDITOR setting in" |
2179 |
- elog "${ROOT}/etc/isabelle/settings" |
2180 |
- fi |
2181 |
- elog "Please ensure you have a pdf viewer installed, for example:" |
2182 |
- elog "As root: emerge app-text/zathura-pdf-poppler" |
2183 |
- elog "Please configure your preferred pdf viewer, something like:" |
2184 |
- elog "As normal user: xdg-mime default zathura.desktop application/pdf" |
2185 |
- elog "Or alternatively by editing the PDF_VIEWER variable in the system" |
2186 |
- elog "settings file ${ROOT}etc/isabelle/settings and/or the user" |
2187 |
- elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings" |
2188 |
- elog "To improve sledgehammer performance, consider installing:" |
2189 |
- elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass" |
2190 |
- elog "For nitpick it is necessary to install:" |
2191 |
- elog "emerge sci-mathematics/kodkodi" |
2192 |
-} |
2193 |
|
2194 |
diff --git a/sci-mathematics/isabelle/metadata.xml b/sci-mathematics/isabelle/metadata.xml |
2195 |
index b1da3cf..a23d48b 100644 |
2196 |
--- a/sci-mathematics/isabelle/metadata.xml |
2197 |
+++ b/sci-mathematics/isabelle/metadata.xml |
2198 |
@@ -18,20 +18,6 @@ correctness of computer hardware or software and proving |
2199 |
properties of computer languages and protocols. |
2200 |
</longdescription> |
2201 |
<use> |
2202 |
- <flag name="Pure">Pure is the basis for all object-logics.</flag> |
2203 |
- <flag name="FOL">FOL (Many-sorted First-Order Logic) provides basic |
2204 |
- classical and intuitionistic first-order logic. It is polymorphic.</flag> |
2205 |
- <flag name="HOL">(Higher-Order Logic) is a version of classical higher-order |
2206 |
- logic resembling that of the HOL System.</flag> |
2207 |
- <flag name="ZF">ZF (Set Theory) offers a formulation of Zermelo-Fraenkel |
2208 |
- set theory on top of FOL.</flag> |
2209 |
- <flag name="CCL">CCL (Classical Computational Logic)</flag> |
2210 |
- <flag name="CTT">CTT (Constructive Type Theory) is an extensional version |
2211 |
- of Martin-Löf's Type Theory.</flag> |
2212 |
- <flag name="Cube">Cube (The Lambda Cube)</flag> |
2213 |
- <flag name="FOLP">FOLP (FOL with Proof Terms)</flag> |
2214 |
- <flag name="LCF">LCF (Logic of Computable Functions)</flag> |
2215 |
- <flag name="Sequents">Sequents (first-order, modal and linear logics)</flag> |
2216 |
<flag name="graphbrowsing">Generate theory browsing information, |
2217 |
including HTML documents that show a theory's definition, the |
2218 |
theorems proved in its ML file and the relationship with its |
2219 |
@@ -41,6 +27,5 @@ properties of computer languages and protocols. |
2220 |
editor</flag> |
2221 |
<flag name="proofgeneral">Add support for the |
2222 |
<pkg>app-emacs/proofgeneral</pkg> proof assistant front end.</flag> |
2223 |
- <flag name="pide">Build Isabelle/jEdit Prover IDE (PIDE).</flag> |
2224 |
</use> |
2225 |
</pkgmetadata> |