gentoo-mirror/gentoo
1
0
Fork 0
mirror of https://github.com/gentoo-mirror/gentoo.git synced 2026-09-24 04:59:14 -07:00
Code Issues Projects Releases Wiki Activity

sci-mathematics/isabelle: Remove old

Browse Source 
Package-Manager: portage-2.2.27
This commit is contained in:
James Le Cuirot
2016-03-06 12:52:23 +00:00
parent a99db855fb
commit 1db4669fbb
18 changed files with 0 additions and 2052 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
sci-mathematics/isabelle/Manifest
View File

@@ -1,17 +1,7 @@
DIST Isabelle2011-1.tar.gz 42239059 SHA256 48d77fe31a16b44f6015aa7953a60bdad8fcec9e60847630dc7b98c053edfc08 SHA512 213207951455395659a91b0bc6c8520c084cb6c75098c8f24c0800e41474c90c92aae86ffb99415142f6cf63d569556661ba350024fe458daa54a5cc9db372fd WHIRLPOOL 7e7868c3f464f507aceb8e1f648c04394fdd69746242179e66cfad64f927cf4d6aba41970428da5e45cce90a30bcee29bdc373d8a9e4943eb61cd97480d0a366
DIST Isabelle2012-doc-src.tar.gz 2688496 SHA256 e18965fe0f7f89b286d4707e38201f1edbea81f6b26aed59d63a633c03fec097 SHA512 5aaea56eb67e535d745d63314278b6ee8469e6d3bbf4ce4d7b3f5e04b24557783b56d50d905a5ad69187c42f44407023c95a9bfb6faab125c21edff7638ff21d WHIRLPOOL 278b63a243950b1596376ee04cbfddb7a93c747e9f6ee66c5b069ca0dae4ca8d10bef43e03069b6186a19c703f71a585633fc47c3c1a15de3a886ff468232127
DIST Isabelle2012.tar.gz 49529865 SHA256 b86f957dee221041f92c9d4ced4758d45b4950339743d0d58b1ea6061e2b53f0 SHA512 1346f563233eba10bc14f7d140706b8bfba8e832f7ee5887316c829926136af07d700914a925272d8adc1275b0bdd682540518957910c136a15bfc60d61285a0 WHIRLPOOL 23b764a1a0044a9525d058e95da318f4425fadf7660edc8ab8f35b248f98dcff0dba2e533ff18d8bf47ea164cec12a9648642749de2a49887bbe84ed4e71a68b
DIST Isabelle2013-2.tar.gz 52603110 SHA256 602e91377b0999c25950ae2a34c0fcb23e3aff3a196bdbc5ce61634bd90d7f22 SHA512 464a2735b2f4e28dcf44e55cd4abb4d8766a6bb7eb86f989f3592e7819e33d97922bdfb6701da85aa9d7c4cc2aee3eadebde1c7e3fc74bb3f6108a5daf5fea45 WHIRLPOOL 0dc354d60e3440ea0909dc09f25b66cb301b82f88fbe21c0b7f4bfef40ecc3631014757abd8657f0464047f0ad32827ad308e3f998fcf2477e05907ff7b19a84
DIST Isabelle2013.tar.gz 54638791 SHA256 2f2cda9939248bd4346ad7e074cb6b2cfad70708777491c6262a5ae670c8f83a SHA512 e03f9b747f678749a562c3de6100f4f4e010ace51b2eb13bcde0a63591eec0cb4e081f7fad9147d022fe787b56eac3f037ab3a296080fd70cc7d058ea961a789 WHIRLPOOL 5cbcbc93bd2ce4723034c3d95d4678b2de90c924601b795c5da378cb76f58275e5d5f47ce9120234a9ea36e43ab759ced843dca76942378abfa1fb7aff858a65
DIST Isabelle2015.tar.gz 36529154 SHA256 08723d3be6f91c57a7a69a8624c54cc1e0cd31506988bf29ed365a5aa5a5156f SHA512 052bb80316a9345368a295a7c5f3869b58d71a6879548fc6240a04fd2cf8c11406274ead8a1ed098563ef9b7573a826656da543e745044fc1d275322af5cc212 WHIRLPOOL 0be4759a1064f4759c2f227b037c448093ff36b47e16002fbb7e99d2843583e01314c4ea5c7a8cbf4d1304f8f72a383052911e483d51e4af2e68c4c36dea5121
DIST csdp-isabelle-component-6.x.tar.gz 493 SHA256 65dde42fa476095052ca3820df4c0e45089653d4467a53de711c8e13670a1b19 SHA512 9be28ecbf61d0f6ad23e28d44bd7ceb8f06ab22f3a05a7c823a9c5bf52ddcf5e5c300c41e14451d6b8e6a4c32b1bbd17769c731cd890fab335a866cd5e735290 WHIRLPOOL c930c531637172e4c75ec44d68f71e69e748a8b976fa3651ef4015fb6a90e30b568bd092632dc16c6389aac09bc13f3249af6c3ac261f09ad2dc5ad915282f99
DIST exec_process-isabelle-component-1.0.3.tar.gz 814 SHA256 ee3b7b299852bcfd0bf7ffce6c8cd2279f2d71247c4a7b0042971b31c2b2a89d SHA512 7880b7f9843ff5806ab37d938a817a5b33e973772d9a6c6cf76bf04076fb532309bd22dfaa203be7c72c07f5a638f0f97e730c414ed164024fd31f1f09fc7c09 WHIRLPOOL 9d9beb7a41baac8b591ceee31bb7b69e1dd07fce66757511649977f6a85d85eef525ba0be13b0873c1aef47de0eace8bf88283b4a136397000e61cfc81da8d4d
DIST jedit_build-20120414.tar.gz 7509120 SHA256 3c5840fd01b87013b05a92742d41f66f655df6fe9edef1525c6722f92d8f3e41 SHA512 2e2f0db4964a041ba54382a9c787246e1d433e43167019c6ea8d4cf6beb84ce438c0bc559d2588229b0166c91bac603bed39abc45d5d4267020f55eaba1aaa0c WHIRLPOOL 40b883943bde312b4c7adc43607ba4759e5ebe22cab3c922c81393375f917af21d4a8dc068e5692ffcf7bdfb1e7fe3081358dc8e346d1942582bf79e249b0cbb
DIST jedit_build-isabelle-component-20130104.tar.gz 10734679 SHA256 22a4880deb1054a548476b22662b42bfaf5394ceb07b30eba69be433bcea1074 SHA512 bacdb3ca73d48fe9ba71dd32cd68e98333831f205dd3ced69bb9344c5b167ba084662f1108690f371b4b64f6b786955a332bcd51a2dc21c2179fb1b4727430dd WHIRLPOOL fc97923e08202e117ca3112b69f74a9f4663a70f55fa051ac55e02c85be57423f762263cac2ded33d9c2f412736e4fa0937aa07df3f36b915e806959055a796b
DIST jedit_build-isabelle-component-20131106.tar.gz 8796625 SHA256 a13a896263804f5aee82db0e1fe6be7982abe3ca1266cd15f7fe9c8c2f6e2ba5 SHA512 7fc3313916cd408c906e453a4895f49223a8b9dc1e2c577c16468394b73a3724449b411521884d419683cd3d2eb3ef59929608483ff092b9b0e3663efd5e136e WHIRLPOOL 4e7c933df7eea5b9c312f8e0c2c46d44a442d0dd2bb76415bea1fcf307ff75d1f8fb592fe4cad647674dc387fe6fa017dbf4e0cf2ec64459bdafb093470e2abf
DIST jedit_build-isabelle-component-20150228.tar.gz 10674317 SHA256 2bee3c5242a3ce4150656f106e658096e82b6bd966e04d590e20023a956be29b SHA512 ba2d0804f21cee596fc3528a592941efc393e98b890efe054aed18fc0d31edfe459047b58ed79b42892e219b4c35a4fb5c8cca0f402b96d641ff8ce62e321339 WHIRLPOOL b2971bdef70e32d858385cb58603d6a5a7e357dbbc9810569093a31332a7838387f43a76a65048a12f259f08de86f200e962ccf2deb2bd3cd4e83dc4c1e41d8b
DIST jfreechart-isabelle-component-1.0.14-1.tar.gz 3444825 SHA256 b0eb7365c4c5877379889100f081a4afc4117afc0d332941c3dd01bef2c4aee9 SHA512 ee1d84a45e43029d5e3acee823176196da19789322e8d3c2c81d5504930ad81d50e16e5da87655e4151034901daefb4ce6b82334839e39134b3a7ce32203aa67 WHIRLPOOL e6f9caadb802ecb5b784e86e96c008e9271aa0b1c940152fb0b0358280d9c1e274bb0dee1507f8ff0fe7f43f863db538d631c76e146d1f66ab6e8a8fb27eb42d
DIST jfreechart-isabelle-component-1.0.14.tar.gz 3443727 SHA256 c873ad6f07edbcceb5c76aac2e848c7d7f12c78c93c05f7e97c4b1fdba7c2df0 SHA512 c55ec01b215368f064de2f288f788960a256445adca5565c00aa9c0fab5732707a9e72bcdb3838676c80e735c520b9948855d7a32b9076bf35f1a279320ee72a WHIRLPOOL ba1a75e21525c302a3b755d814502dad60c540c2004dd894f60fdd6966766f85d71bbb45728ca220a4a7cff334de81db756fbb89e1059f32e248cabf0a7b97d6
DIST polyml-isabelle-component-5.5.1-1.tar.gz 831 SHA256 f19a4dfc3117792423270cb98a5c406f7339f4bd7715c16976a281d964792844 SHA512 35ab69d0fd2737f3c6a13ca022103428bcb0e71032304d244614d271848b9ae8986da25bd4ef02668eef169f3a3a72576a619152ce3cbf036af7aa365e857c1a WHIRLPOOL 682e25b677e1b0401a43d4cff35c69658359b4c74f86d3459c050e7c7b0d17f1de1e7b792f2a51f97acf574ad56b3e89ade688bc24d090b3e89eaf0cb99a08d5
DIST polyml-isabelle-component-5.5.2-3.tar.gz 691 SHA256 1ba253974193efc70711b7fe32cc831d8bcc13107b0b130ddf6087bb6ff6d3e7 SHA512 45d68fa7a07ae9fc39cb21fa4c4c43a34576377fb828c8652002c56cc9ec7b3c7b5fcefb7604fc4bc90ce4868dd2fca41ddf37ce285da4902664ab21e4657b3f WHIRLPOOL 3a85c59b1bb928c5ea91f8150c6ded5309fae96bd7558b56e6c3d8f04c418b03b57fb49565af5ed919179fd9e30c957575ca7b65d938ce69c5d3131d8c55ab1e
DIST xz-java-isabelle-component-1.5.tar.gz 315 SHA256 e7fdd433608561c87558d4d0ee39166e8396ce11242e85391417ec7fd3ce7b8e SHA512 6dfec49e12c4cafbb6b6386dd54477e86b6bb419a77c52d9606a0305aeea9cd11f087ed6bba77352c7bf9ec656052ef617e845f472e57b5cdfbccf22b2eeb4fa WHIRLPOOL 9c1fc16db0adc88557b81608902d9d69007dc90d5849f4f7501101930842ce81ded76af0e76e38df8bd0b07d137e53bafaa338bf6c7ae338e97af2a1433d5c1d

39
sci-mathematics/isabelle/files/isabelle-2011.1-gentoo-settings.patch
View File

@@ -1,39 +0,0 @@
--- Isabelle2011-1-orig/etc/settings 2011-10-10 01:47:58.000000000 +1100
+++ Isabelle2011-1/etc/settings 2012-01-01 16:33:27.922565527 +1100
@@ -24,9 +24,16 @@
"/usr/share/polyml/$ML_PLATFORM" \
"/opt/polyml/$ML_PLATFORM" \
"")"
-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
-ML_OPTIONS="-H 200"
-ML_SOURCES="$ML_HOME/../src"
+# ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
+# ML_OPTIONS="-H 200"
+# ML_SOURCES="$ML_HOME/../src"
+
+# Poly/ML 5.4.0 (64 bit)
+ML_PLATFORM=x86_64-linux
+ML_HOME=/usr/bin
+ML_SYSTEM=polyml-5.4.0
+ML_OPTIONS="-H 1000"
+#ML_SOURCES="$ML_HOME/../src"
# Poly/ML 32 bit (manual settings)
#ML_SYSTEM=polyml-5.4.0
@@ -106,7 +113,7 @@
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:/usr/lib64/Isabelle2011-1/heaps"
# Heap output location. ML system identifier is appended automatically later on.
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
@@ -170,6 +177,7 @@
"/usr/local/ProofGeneral" \
"/usr/share/ProofGeneral" \
"/opt/ProofGeneral" \
+ "/usr/share/emacs/site-lisp/ProofGeneral" \
"")"
PROOFGENERAL_OPTIONS=""

11
sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch
View File

@@ -1,11 +0,0 @@
--- Isabelle2011-1-orig/lib/browser/build 2011-10-10 01:47:58.000000000 +1100
+++ Isabelle2011-1/lib/browser/build 2012-01-08 12:58:06.041444651 +1100
@@ -6,6 +6,8 @@
#
# Requires proper Isabelle settings environment.
+ISABELLE_HOME="$(cd "$(dirname "${0}")/../.."; pwd -P)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
## diagnostics

11
sci-mathematics/isabelle/files/isabelle-2011.1-libsha1.patch
View File

@@ -1,11 +0,0 @@
--- Isabelle2011-1-orig/src/Pure/General/sha1_polyml.ML 2011-10-10 01:47:58.000000000 +1100
+++ Isabelle2011-1/src/Pure/General/sha1_polyml.ML 2012-12-05 23:28:15.004733643 +1100
@@ -18,7 +18,7 @@
in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
val lib_path =
- ("$ML_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so"))
+ ("$SHA1_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so"))
|> Path.explode;
fun digest_external str =

39
sci-mathematics/isabelle/files/isabelle-2011.1-proofgeneral-gentoo-path.patch
View File

@@ -1,39 +0,0 @@
--- Isabelle2011-1-orig/etc/settings 2011-10-10 01:47:58.000000000 +1100
+++ Isabelle2011-1/etc/settings 2012-01-01 16:33:27.922565527 +1100
@@ -24,9 +24,16 @@
"/usr/share/polyml/$ML_PLATFORM" \
"/opt/polyml/$ML_PLATFORM" \
"")"
-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
-ML_OPTIONS="-H 200"
-ML_SOURCES="$ML_HOME/../src"
+# ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
+# ML_OPTIONS="-H 200"
+# ML_SOURCES="$ML_HOME/../src"
+
+# Poly/ML 5.4.0 (64 bit)
+ML_PLATFORM=x86_64-linux
+ML_HOME=/usr/bin
+ML_SYSTEM=polyml-5.4.0
+ML_OPTIONS="-H 1000"
+#ML_SOURCES="$ML_HOME/../src"
# Poly/ML 32 bit (manual settings)
#ML_SYSTEM=polyml-5.4.0
@@ -106,7 +113,7 @@
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:/usr/lib64/Isabelle2011-1/heaps"
# Heap output location. ML system identifier is appended automatically later on.
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
@@ -170,6 +177,7 @@
"/usr/local/ProofGeneral" \
"/usr/share/ProofGeneral" \
"/opt/ProofGeneral" \
+ "/usr/share/emacs/site-lisp/ProofGeneral" \
"")"
PROOFGENERAL_OPTIONS=""

12
sci-mathematics/isabelle/files/isabelle-2011.1-reverse-line-editor-order.patch
View File

@@ -1,12 +0,0 @@
--- Isabelle2011-1-orig/etc/settings 2011-10-10 01:47:58.000000000 +1100
+++ Isabelle2011-1/etc/settings 2012-05-27 23:28:37.283028668 +1000
@@ -66,8 +66,8 @@
###
ISABELLE_LINE_EDITOR=""
-[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
+[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
###

62
sci-mathematics/isabelle/files/isabelle-2012-gentoo-settings.patch
View File

@@ -1,62 +0,0 @@
--- Isabelle2012-orig/etc/settings 2012-05-23 03:07:38.000000000 +1000
+++ Isabelle2012/etc/settings 2012-05-27 18:07:26.502878614 +1000
@@ -16,17 +16,24 @@
# Only one of the sections below should be activated.
# Poly/ML default (automated settings)
-ML_PLATFORM="$ISABELLE_PLATFORM"
-ML_HOME="$(choosefrom \
- "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
- "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
- "/usr/local/polyml/$ML_PLATFORM" \
- "/usr/share/polyml/$ML_PLATFORM" \
- "/opt/polyml/$ML_PLATFORM" \
- "")"
-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
-ML_OPTIONS="-H 200"
-ML_SOURCES="$ML_HOME/../src"
+# ML_PLATFORM="$ISABELLE_PLATFORM"
+# ML_HOME="$(choosefrom \
+# "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
+# "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
+# "/usr/local/polyml/$ML_PLATFORM" \
+# "/usr/share/polyml/$ML_PLATFORM" \
+# "/opt/polyml/$ML_PLATFORM" \
+# "")"
+# ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
+# ML_OPTIONS="-H 200"
+# ML_SOURCES="$ML_HOME/../src"
+
+# Poly/ML Gentoo (x86_64)
+ML_PLATFORM=x86_64-linux
+ML_HOME="/usr/bin"
+ML_SYSTEM=polyml-5.4.0
+ML_OPTIONS="-H 1000"
+ML_SOURCES="/usr/src/debug/dev-lang/polyml-5.4.0"
# Poly/ML 32 bit (manual settings)
#ML_SYSTEM=polyml-5.4.1
@@ -102,7 +109,7 @@
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:/usr/lib64/Isabelle2012/heaps"
# Heap output location. ML system identifier is appended automatically later on.
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
@@ -161,13 +168,7 @@
###
# Proof General home, look in a variety of places
-PROOFGENERAL_HOME="$(choosefrom \
- "$ISABELLE_HOME/contrib/ProofGeneral" \
- "$ISABELLE_HOME/../ProofGeneral" \
- "/usr/local/ProofGeneral" \
- "/usr/share/ProofGeneral" \
- "/opt/ProofGeneral" \
- "")"
+PROOFGENERAL_HOME="/usr/share/emacs/site-lisp/ProofGeneral"
PROOFGENERAL_OPTIONS=""
#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"

35
sci-mathematics/isabelle/files/isabelle-2012-redundant-equations-in-function-definitions-error.patch
View File

@@ -1,35 +0,0 @@
diff -r dd611ab202a8 -r e7e647949c95 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/Tools/Function/fun.ML Wed Jun 06 21:36:21 2012 +0200
@@ -84,10 +84,10 @@
spec @ mk_catchall fixes arity_of
end
-fun warnings ctxt origs tss =
+fun further_checks ctxt origs tss =
let
- fun warn_redundant t =
- warning ("Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t))
+ fun fail_redundant t =
+ error (cat_lines ["Equation is redundant (covered by preceding clauses):", Syntax.string_of_term ctxt t])
fun warn_missing strs =
warning (cat_lines ("Missing patterns in function definition:" :: strs))
@@ -100,7 +100,7 @@
@ ["(" ^ string_of_int (length rest) ^ " more)"])
val _ = (origs ~~ tss')
- |> map (fn (t, ts) => if null ts then warn_redundant t else ())
+ |> map (fn (t, ts) => if null ts then fail_redundant t else ())
in
()
end
@@ -119,7 +119,7 @@
val compleqs = add_catchall ctxt fixes feqs (* Completion *)
val spliteqs = Function_Split.split_all_equations ctxt compleqs
- |> tap (warnings ctxt feqs)
+ |> tap (further_checks ctxt feqs)
fun restore_spec thms =
bnds ~~ take (length bnds) (unflat spliteqs thms)

8
sci-mathematics/isabelle/files/isabelle-2012-signal-handling.patch
View File

@@ -1,8 +0,0 @@
diff -r c79adcae9869 -r 6de952f4069f lib/scripts/run-polyml
--- a/lib/scripts/run-polyml Fri May 25 13:23:43 2012 +0200
+++ b/lib/scripts/run-polyml Fri May 25 17:14:14 2012 +0200
@@ -76,3 +76,3 @@
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+ { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
RC="$?"

82
sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch
View File

@@ -1,82 +0,0 @@
--- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy 2013-02-13 00:31:10.000000000 +1100
+++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy 2013-08-31 14:37:02.015159000 +1000
@@ -82,7 +82,7 @@
setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1]
oops
section {* Manual setup to find the counterexample *}
@@ -110,7 +110,7 @@
lemma
"hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1]
oops
section {* Using a global limit for limiting the execution *}
@@ -146,7 +146,7 @@
lemma
"hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1]
oops
end
\ No newline at end of file
--- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy 2013-02-13 00:31:10.000000000 +1100
+++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy 2013-08-31 14:36:47.049851000 +1000
@@ -33,7 +33,7 @@
lemma
"S\<^isub>1p w \<Longrightarrow> w = []"
-quickcheck[tester = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1]
oops
definition "filter_a = filter (\<lambda>x. x = a)"
@@ -67,7 +67,7 @@
theorem S\<^isub>1_sound:
"S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[tester = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1]
oops
@@ -91,7 +91,7 @@
theorem S\<^isub>2_sound:
"S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[tester = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1]
oops
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
--- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy 2013-02-13 00:31:10.000000000 +1100
+++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy 2013-08-31 14:28:11.784390000 +1000
@@ -92,7 +92,7 @@
lemma
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1]
oops
text {* Verifying that the found counterexample really is one by means of a proof *}
--- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/List_Examples.thy 2013-02-13 00:31:10.000000000 +1100
+++ Isabelle2013/src/HOL/Predicate_Compile_Examples/List_Examples.thy 2013-08-31 14:27:52.013962000 +1000
@@ -21,7 +21,7 @@
lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
quickcheck[tester = random, iterations = 10000]
quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
-quickcheck[tester = prolog, expect = counterexample]
+quickcheck[tester = prolog]
oops
end
\ No newline at end of file

149
sci-mathematics/isabelle/files/isabelle-2013-classpath.patch
View File

@@ -1,149 +0,0 @@
--- Isabelle2013-orig/lib/Tools/java 2013-02-13 00:31:02.000000000 +1100
+++ Isabelle2013/lib/Tools/java 2015-04-17 12:16:04.734716358 +1000
@@ -6,5 +6,5 @@
CLASSPATH="$(jvmpath "$CLASSPATH")"
isabelle_jdk java -Dfile.encoding=UTF-8 -server \
- "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
+ "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala-2.10 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
--- Isabelle2013-orig/lib/Tools/scala 2013-02-13 00:31:02.000000000 +1100
+++ Isabelle2013/lib/Tools/scala 2015-04-17 12:12:21.606890256 +1000
@@ -8,4 +8,4 @@
CLASSPATH="$(jvmpath "$CLASSPATH")"
isabelle_scala scala -Dfile.encoding=UTF-8 \
- "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
+ "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala-2.10 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
--- Isabelle2013-orig/lib/Tools/scalac 2013-02-13 00:31:02.000000000 +1100
+++ Isabelle2013/lib/Tools/scalac 2015-04-17 12:12:36.895871214 +1000
@@ -8,5 +8,5 @@
CLASSPATH="$(jvmpath "$CLASSPATH")"
isabelle_scala scalac -Dfile.encoding=UTF-8 \
- "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
+ "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala-2.10 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
--- Isabelle2013-orig/src/Pure/build-jars 2013-02-13 00:31:15.000000000 +1100
+++ Isabelle2013/src/Pure/build-jars 2013-08-18 12:55:51.400924000 +1000
@@ -133,7 +133,7 @@
declare -a JFREECHART_JARS=()
for NAME in $JFREECHART_JAR_NAMES
do
- JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
+ JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$NAME"
done
--- Isabelle2013-orig/src/Tools/jEdit/lib/Tools/jedit 2013-02-13 00:31:16.000000000 +1100
+++ Isabelle2013/src/Tools/jEdit/lib/Tools/jedit 2013-08-18 16:39:15.495244000 +1000
@@ -214,97 +214,11 @@
declare -a JFREECHART_JARS=()
for NAME in $JFREECHART_JAR_NAMES
do
- JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
+ JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$NAME"
done
-
-# target
-
-TARGET="dist/jars/Isabelle-jEdit.jar"
-
-declare -a UPDATED=()
-
-if [ "$BUILD_JARS" = jars_fresh ]; then
- OUTDATED=true
-else
- OUTDATED=false
- if [ ! -e "$TARGET" ]; then
- OUTDATED=true
- else
- if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
- declare -a DEPS=(
- "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}"
- "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
- )
- elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
- declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
- else
- declare -a DEPS=()
- fi
- for DEP in "${DEPS[@]}"
- do
- [ ! -e "$DEP" ] && fail "Missing file: $DEP"
- [ "$DEP" -nt "$TARGET" ] && {
- OUTDATED=true
- UPDATED["${#UPDATED[@]}"]="$DEP"
- }
- done
- fi
-fi
-
-
-# build
-
-if [ "$OUTDATED" = true ]
-then
- echo "### Building Isabelle/jEdit ..."
-
- [ "${#UPDATED[@]}" -gt 0 ] && {
- echo "Changed files:"
- for FILE in "${UPDATED[@]}"
- do
- echo " $FILE"
- done
- }
-
- [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
- fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
-
- rm -rf dist || failed
- mkdir -p dist dist/classes || failed
-
- cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
- cp -p -R -f "${RESOURCES[@]}" dist/classes/.
- cp src/jEdit.props dist/properties/.
- cp -p -R -f src/modes/. dist/modes/.
-
- perl -i -e 'while (<>) {
- if (m/NAME="javacc"/) {
- print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
- print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,;
- print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
- print; }' dist/modes/catalog
-
- cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
- (
- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$PURE_JAR" \
- "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
- do
- CLASSPATH="$CLASSPATH:$JAR"
- done
- CLASSPATH="$(jvmpath "$CLASSPATH")"
- exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}"
- ) || fail "Failed to compile sources"
-
- cd dist/classes
- isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed
- cd ../..
- rm -rf dist/classes
-fi
-
popd >/dev/null
-
## main
if [ "$BUILD_ONLY" = false ]; then
--- Isabelle2013-orig/contrib/jfreechart-1.0.14/etc/settings 2012-12-09 07:23:53.000000000 +1100
+++ Isabelle2013/contrib/jfreechart-1.0.14/etc/settings 2013-08-18 16:18:10.244698000 +1000
@@ -1,7 +1,5 @@
# -*- shell-script -*- :mode=shellscript:
JFREECHART_HOME="$COMPONENT"
-JFREECHART_JAR_NAMES="iText-2.1.5.jar jcommon-1.0.18.jar jfreechart-1.0.14.jar"
-
-ISABELLE_JAVA_EXT="$ISABELLE_JAVA_EXT:$JFREECHART_HOME/lib"
+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')"

135
sci-mathematics/isabelle/files/isabelle-2013.2-classpath.patch
View File

@@ -1,135 +0,0 @@
--- Isabelle2013-2-orig/lib/Tools/java 2013-12-06 02:18:34.000000000 +1100
+++ Isabelle2013-2/lib/Tools/java 2015-04-17 12:23:11.535463796 +1000
@@ -10,5 +10,5 @@
unset CLASSPATH
isabelle_jdk java "${JAVA_ARGS[@]}" \
- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
--- Isabelle2013-2-orig/lib/Tools/scala 2013-12-06 02:18:34.000000000 +1100
+++ Isabelle2013-2/lib/Tools/scala 2015-04-17 12:23:24.836455672 +1000
@@ -7,5 +7,5 @@
isabelle_admin_build jars || exit $?
isabelle_scala scala -Dfile.encoding=UTF-8 \
- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
--- Isabelle2013-2-orig/lib/Tools/scalac 2013-12-06 02:18:34.000000000 +1100
+++ Isabelle2013-2/lib/Tools/scalac 2015-04-17 12:23:33.084450628 +1000
@@ -7,5 +7,5 @@
isabelle_admin_build jars || exit $?
isabelle_scala scalac -Dfile.encoding=UTF-8 \
- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11 | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
--- Isabelle2013-2-orig/src/Tools/jEdit/lib/Tools/jedit 2013-12-06 02:19:04.000000000 +1100
+++ Isabelle2013-2/src/Tools/jEdit/lib/Tools/jedit 2014-02-09 20:59:14.026841490 +1100
@@ -211,105 +211,6 @@
"$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar"
)
-
-# target
-
-TARGET="dist/jars/Isabelle-jEdit.jar"
-
-declare -a UPDATED=()
-
-if [ "$BUILD_JARS" = jars_fresh ]; then
- OUTDATED=true
-else
- OUTDATED=false
- if [ ! -e "$TARGET" ]; then
- OUTDATED=true
- else
- if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
- declare -a DEPS=(
- "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
- "${SOURCES[@]}" "${RESOURCES[@]}"
- )
- elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
- declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
- else
- declare -a DEPS=()
- fi
- for DEP in "${DEPS[@]}"
- do
- [ ! -e "$DEP" ] && fail "Missing file: $DEP"
- [ "$DEP" -nt "$TARGET" ] && {
- OUTDATED=true
- UPDATED["${#UPDATED[@]}"]="$DEP"
- }
- done
- fi
-fi
-
-
-# build
-
-if [ "$OUTDATED" = true ]
-then
- echo "### Building Isabelle/jEdit ..."
-
- [ "${#UPDATED[@]}" -gt 0 ] && {
- echo "Changed files:"
- for FILE in "${UPDATED[@]}"
- do
- echo " $FILE"
- done
- }
-
- [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
- fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
-
- rm -rf dist || failed
- mkdir -p dist dist/classes || failed
-
- cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
- cp -p -R -f "${RESOURCES[@]}" dist/classes/.
- cp src/jEdit.props dist/properties/.
- cp -p -R -f src/modes/. dist/modes/.
-
- perl -i -e 'while (<>) {
- if (m/NAME="javacc"/) {
- print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
- print qq,<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n,;
- print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,;
- print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
- print; }' dist/modes/catalog
-
- cd dist
- isabelle_jdk jar xf jedit.jar
- cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" \
- "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed
- cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" \
- "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed
- isabelle_jdk jar cfe jedit.jar org.gjt.sp.jedit.jEdit org || failed
- rm -rf META-INF org
- cd ..
-
- cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
- (
- #workaround for scalac 2.10.2
- function stty() { :; }
- export -f stty
-
- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
- do
- classpath "$JAR"
- done
- export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
- exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}"
- ) || fail "Failed to compile sources"
-
- cd dist/classes
- isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed
- cd ../..
- rm -rf dist/classes
-fi
-
popd >/dev/null

254
sci-mathematics/isabelle/isabelle-2011.1-r2.ebuild
View File

@@ -1,254 +0,0 @@
# Copyright 1999-2015 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Id$
EAPI="5"
inherit eutils java-pkg-2 multilib versionator
MY_PN="Isabelle"
MY_PV=$(replace_all_version_separators '-')
MY_P="${MY_PN}${MY_PV}"
DESCRIPTION="Isabelle is a generic proof assistant"
HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html"
SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz"
LICENSE="BSD"
SLOT="0/${PV}"
KEYWORDS="~amd64 ~x86"
ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents"
IUSE="${ALL_LOGICS} doc graphbrowsing ledit readline +proofgeneral test"
#upstream says
#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
#for document preparation: complete LaTeX
DEPEND=">=app-shells/bash-3.0:*
>=dev-lang/polyml-5.4.1:=[-portable]
>=dev-lang/perl-5.8.8-r2"
RDEPEND="dev-perl/libwww-perl
sci-mathematics/sha1-polyml
doc? (
virtual/latex-base
dev-tex/rail
)
proofgeneral? (
app-emacs/proofgeneral
)
ledit? (
app-misc/ledit
)
readline? (
app-misc/rlwrap
)
${DEPEND}"
S="${WORKDIR}"/Isabelle${MY_PV}
TARGETDIR="/usr/share/Isabelle"${MY_PV}
LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
pkg_setup() {
java-pkg-2_pkg_setup
if ! use proofgeneral
then
ewarn "You have deselected the Proof General interface."
ewarn "Only a text terminal will be installed."
ewarn "Emerge Isabelle with the proofgeneral USE flag enabled"
ewarn "to get the common interface, that most people want."
fi
}
src_prepare() {
java-pkg-2_src_prepare
epatch "${FILESDIR}/${PN}-2011.1-gentoo-settings.patch"
polymlver=$(poly -v | cut -d' ' -f2)
polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
sed -e "s@5.4.0@${polymlver}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml version in etc/settings"
sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml ML_HOME in etc/settings"
sed -e "s@x86_64@${polymlarch}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml arch in etc/settings"
sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \
-i "${S}/etc/settings" \
|| die "Could not configure PROOFGENERAL_HOME in etc/settings"
sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure Isabelle lib directory in etc/settings"
epatch "${FILESDIR}/${PN}-2011.1-graphbrowser.patch"
epatch "${FILESDIR}/${PN}-2011.1-libsha1.patch"
cat <<- EOF >> "${S}/etc/settings"
ISABELLE_GHC="${ROOT}usr/bin/ghc"
ISABELLE_OCAML="${ROOT}usr/bin/ocaml"
ISABELLE_SWIPL="${ROOT}usr/bin/swipl"
ISABELLE_JDK_HOME="\$(java-config --jdk-home)"
SCALA_HOME="${ROOT}usr/share/scala"
SHA1_HOME="/usr/$(get_libdir)/sha1-polyml"
EOF
if use ledit && ! use readline; then
epatch "${FILESDIR}/${PN}-2011.1-reverse-line-editor-order.patch"
fi
}
src_compile() {
LOGICS=""
for l in "${ALL_LOGICS}"; do
if has "${l/+/}"; then
LOGICS="${LOGICS} ${l/+/}"
fi
done
einfo "Building Isabelle logics ${LOGICS}. This may take some time."
./build -b -i "${LOGICS}" || die "building logics failed"
./bin/isabelle makeall || die "isabelle makeall failed"
if use graphbrowsing
then
rm -f "${S}/lib/browser/GraphBrowser.jar" \
|| die "failed cleaning graph browser directory"
pushd "${S}/lib/browser" \
|| die "Could not change directory to lib/browser"
./build || die "failed building the graph browser"
popd
fi
}
src_test() {
einfo "Running tests. A test run can take up to several hours!"
./build -b -t || die "tests failed"
}
src_install() {
exeinto ${TARGETDIR}/bin
doexe bin/isabelle-process bin/isabelle
insinto ${TARGETDIR}
doins -r src
doins -r lib
for i in "./build" \
"src/Pure/mk" \
"src/Pure/build-jars" \
"src/Tools/jEdit/dist/build-support/ci/copy_properties.groovy" \
"src/Tools/jEdit/dist/build-support/ci/ci_release.groovy" \
"src/Tools/jEdit/lib/Tools/jedit" \
"src/Tools/Metis/fix_metis_license" \
"src/Tools/Metis/make_metis" \
"src/Tools/Metis/scripts/mlpp" \
"src/Tools/WWW_Find/lib/Tools/wwwfind" \
"src/Tools/Code/lib/Tools/codegen" \
"src/HOL/Mirabelle/lib/Tools/mirabelle" \
"src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \
"src/HOL/Tools/SMT/lib/scripts/remote_smt" \
"src/HOL/Tools/ATP/scripts/remote_atp" \
"src/HOL/Tools/ATP/scripts/spass" \
"src/HOL/Tools/Nitpick/lib/Tools/nitrox" \
"src/HOL/Mutabelle/lib/Tools/mutabelle" \
"src/HOL/Library/Sum_of_Squares/neos_csdp_client" \
"lib/browser/build" \
"lib/Tools/tty" \
"lib/Tools/mkproject" \
"lib/Tools/keywords" \
"lib/Tools/browser" \
"lib/Tools/install" \
"lib/Tools/mkdir" \
"lib/Tools/unsymbolize" \
"lib/Tools/getenv" \
"lib/Tools/java" \
"lib/Tools/make" \
"lib/Tools/emacs" \
"lib/Tools/scala" \
"lib/Tools/print" \
"lib/Tools/latex" \
"lib/Tools/findlogics" \
"lib/Tools/doc" \
"lib/Tools/logo" \
"lib/Tools/usedir" \
"lib/Tools/yxml" \
"lib/Tools/version" \
"lib/Tools/makeall" \
"lib/Tools/scalac" \
"lib/Tools/document" \
"lib/Tools/env" \
"lib/Tools/display" \
"lib/Tools/dimacs2hol" \
"lib/scripts/keywords" \
"lib/scripts/unsymbolize" \
"lib/scripts/run-polyml" \
"lib/scripts/run-smlnj" \
"lib/scripts/feeder" \
"lib/scripts/java_ext_dirs" \
"lib/scripts/yxml" \
"lib/scripts/raw_dump" \
"lib/scripts/polyml-version" \
"lib/scripts/process"
do
exeinto $(dirname "${TARGETDIR}/${i}")
doexe ${i}
done
docompress -x /usr/share/doc/${PF}
dodoc -r doc
if use doc; then
dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc"
fi
dodir /etc/isabelle
insinto /etc/isabelle
doins -r etc/*
dosym /etc/isabelle "${TARGETDIR}/etc"
dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
insinto ${LIBDIR}
doins -r heaps
bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \
|| die "isabelle install failed"
newicon lib/icons/isabelle.xpm "${PN}.xpm"
dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README
java-pkg_regjar \
"${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \
"${ED}${TARGETDIR}/lib/classes/java_ext_dirs.jar"
}
pkg_postinst() {
# If any of the directories in /etc/isabelle/components do not exist, then
# even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to
# to delete any non-existing directories. If an old Isabelle version was
# installed with component ebuilds like sci-mathematics/e, then the
# Isabelle version is upgraded, then the contrib directories will not
# exist initially, it is necessary to delete them from /etc/isabelle/components.
# Then these components are rebuilt (creating these directories) using the
# EAPI=5 subslot depends.
for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components")
do
if [ ! -d /usr/share/Isabelle2012/${i} ]; then
sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components"
fi
done
if use ledit && use readline; then
elog "Both readline and ledit use flags specified. The default setting"
elog "if both are installed is to use readline (rlwrap), this can be"
elog "modfied by editing the ISABELLE_LINE_EDITOR setting in"
elog "${ROOT}/etc/isabelle/settings"
fi
elog "Please ensure you have a pdf viewer installed, for example:"
elog "As root: emerge app-text/zathura-pdf-poppler"
elog "Please configure your preferred pdf viewer, something like:"
elog "As normal user: xdg-mime default zathura.desktop application/pdf"
elog "Or alternatively by editing the PDF_VIEWER variable in the system"
elog "settings file ${ROOT}etc/isabelle/settings and/or the user"
elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings"
elog "To improve sledgehammer performance, consider installing:"
elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass"
elog "For nitpick it is necessary to install:"
elog "emerge sci-mathematics/kodkodi"
}

142
sci-mathematics/isabelle/isabelle-2011.1.ebuild
View File

@@ -1,142 +0,0 @@
# Copyright 1999-2012 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Id$
EAPI="4"
JAVA_PKG_OPT_USE="graphbrowsing"
inherit eutils java-pkg-opt-2 multilib versionator
MY_PN="Isabelle"
MY_PV=$(replace_all_version_separators '-')
MY_P="${MY_PN}${MY_PV}"
DESCRIPTION="Isabelle is a generic proof assistant"
HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html"
SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz"
LICENSE="BSD"
SLOT="0"
KEYWORDS="~x86 ~amd64"
ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents"
IUSE="${ALL_LOGICS} doc graphbrowsing +proofgeneral test"
#upstream says
#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
#for document preparation: complete LaTeX
DEPEND=">=app-shells/bash-3.0
>=dev-lang/polyml-5.4.1[-portable]
>=dev-lang/perl-5.8.8-r2"
RDEPEND="doc? (
virtual/latex-base
dev-tex/rail
)
proofgeneral? (
app-emacs/proofgeneral
)
${DEPEND}"
S="${WORKDIR}"/Isabelle${MY_PV}
TARGETDIR="/usr/share/Isabelle"${MY_PV}
LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
pkg_setup() {
java-pkg-opt-2_pkg_setup
if ! use proofgeneral
then
ewarn "You have deselected the Proof General interface."
ewarn "Only a text terminal will be installed."
ewarn "Emerge Isabelle with the proofgeneral USE flag enabled"
ewarn "to get the common interface, that most people want."
fi
}
src_prepare() {
java-pkg-opt-2_src_prepare
if use proofgeneral; then
epatch "${FILESDIR}/${PN}-2011.1-proofgeneral-gentoo-path.patch"
polymlver=$(poly -v | cut -d' ' -f2)
polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
sed -e "s@5.4.0@${polymlver}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml version in etc/settings"
sed -e "s@x86_64@${polymlarch}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml arch in etc/settings"
fi
if use graphbrowsing; then
epatch "${FILESDIR}/${PN}-2011.1-graphbrowser.patch"
fi
}
src_compile() {
LOGICS=""
for l in "${ALL_LOGICS}"; do
if has "${l/+/}"; then
LOGICS="${LOGICS} ${l/+/}"
fi
done
einfo "Building Isabelle logics ${LOGICS}. This may take some time."
./build -b -i "${LOGICS}" || die "building logics failed"
./bin/isabelle makeall || die "isabelle makeall failed"
if use graphbrowsing
then
rm -f "${S}/lib/browser/GraphBrowser.jar" \
|| die "failed cleaning graph browser directory"
pushd "${S}/lib/browser" \
|| die "Could not change directory to lib/browser"
./build || die "failed building the graph browser"
popd
fi
}
src_test() {
einfo "Running tests. A test run can take up to several hours!"
./build -b -t || die "tests failed"
}
src_install() {
exeinto ${TARGETDIR}/bin
doexe bin/isabelle-process bin/isabelle
exeinto ${TARGETDIR}
doexe build
insinto ${TARGETDIR}
doins -r src
dodoc -r doc
dodir /etc/isabelle
insinto /etc/isabelle
doins -r etc/*
dosym /etc/isabelle "${TARGETDIR}/etc"
dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
insinto ${LIBDIR}
doins -r heaps
# use cp to keep file attributes
cp -R lib "${ED}${TARGETDIR}" || die "install lib failed"
bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \
|| die "isabelle install failed"
newicon lib/icons/isabelle.xpm "${PN}.xpm"
dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README
java-pkg_regjar \
"${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \
"${ED}${TARGETDIR}/lib/classes/java_ext_dirs.jar"
}
pkg_postinst() {
elog "You will need to re-emerge Isabelle after emerging polyml."
elog "Please configure your preferred pdf viewer by editing"
elog "the PDF_VIEWER variable in the system settings file"
elog "/etc/isabelle/settings and/or the user settings file"
elog "\$HOME/.isabelle/${MY_P}/etc/settings"
}

320
sci-mathematics/isabelle/isabelle-2012-r1.ebuild
View File

@@ -1,320 +0,0 @@
# Copyright 1999-2015 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Id$
EAPI="5"
inherit eutils java-pkg-2 multilib versionator
MY_PN="Isabelle"
MY_PV=$(replace_all_version_separators '-')
MY_P="${MY_PN}${MY_PV}"
JEDIT_PV="20120414"
JEDIT_PN="jedit_build"
JEDIT_P="${JEDIT_PN}-${JEDIT_PV}"
DESCRIPTION="Isabelle is a generic proof assistant"
HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html"
SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz
doc? ( https://dev.gentoo.org/~gienah/snapshots/${MY_P}-doc-src.tar.gz )
pide? ( http://www4.in.tum.de/~wenzelm/test/${JEDIT_P}.tar.gz )"
LICENSE="BSD"
SLOT="0/${PV}"
KEYWORDS="~amd64 ~x86"
ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents"
IUSE="${ALL_LOGICS} doc graphbrowsing ledit readline pide +proofgeneral test"
#upstream says
#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
#for document preparation: complete LaTeX
DEPEND=">=app-shells/bash-3.0:*
>=dev-lang/polyml-5.4.1:=[-portable]
>=dev-lang/perl-5.8.8-r2"
RDEPEND="dev-perl/libwww-perl
sci-mathematics/sha1-polyml
doc? (
virtual/latex-base
dev-tex/rail
)
proofgeneral? (
app-emacs/proofgeneral
)
pide? (
>=dev-lang/scala-2.8.2
)
ledit? (
app-misc/ledit
)
readline? (
app-misc/rlwrap
)
${DEPEND}"
S="${WORKDIR}"/Isabelle${MY_PV}
JEDIT_S="${WORKDIR}/${JEDIT_P}"
TARGETDIR="/usr/share/Isabelle"${MY_PV}
LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
pkg_setup() {
java-pkg-2_pkg_setup
if ! use proofgeneral
then
ewarn "You have deselected the Proof General interface."
ewarn "Only a text terminal will be installed."
ewarn "Emerge Isabelle with the proofgeneral USE flag enabled"
ewarn "to get the common interface, that most people want."
fi
}
src_prepare() {
java-pkg-2_src_prepare
epatch "${FILESDIR}/${PN}-2012-gentoo-settings.patch"
# http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/2732
epatch "${FILESDIR}/${PN}-2012-signal-handling.patch"
# http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/2780
epatch "${FILESDIR}/${PN}-2012-redundant-equations-in-function-definitions-error.patch"
polymlver=$(poly -v | cut -d' ' -f2)
polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
sed -e "s@5.4.0@${polymlver}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml version in etc/settings"
sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml ML_HOME in etc/settings"
sed -e "s@x86_64@${polymlarch}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml arch in etc/settings"
sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \
-i "${S}/etc/settings" \
|| die "Could not configure PROOFGENERAL_HOME in etc/settings"
sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure Isabelle lib directory in etc/settings"
epatch "${FILESDIR}/${PN}-2012-graphbrowser.patch"
epatch "${FILESDIR}/${PN}-2012-libsha1.patch"
cat <<- EOF >> "${S}/etc/settings"
ISABELLE_GHC="${ROOT}usr/bin/ghc"
ISABELLE_OCAML="${ROOT}usr/bin/ocaml"
ISABELLE_SWIPL="${ROOT}usr/bin/swipl"
ISABELLE_JDK_HOME="\$(java-config --jdk-home)"
SCALA_HOME="${ROOT}usr/share/scala"
SHA1_HOME="/usr/$(get_libdir)/sha1-polyml"
EOF
if use pide; then
cat <<- EOF >> "${S}/etc/settings"
ISABELLE_JEDIT_BUILD_HOME="\$ISABELLE_HOME/${JEDIT_P}"
init_component ${JEDIT_S}
EOF
fi
if use ledit && ! use readline; then
epatch "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch"
fi
}
src_compile() {
LOGICS=""
for l in "${ALL_LOGICS}"; do
if has "${l/+/}"; then
LOGICS="${LOGICS} ${l/+/}"
fi
done
einfo "Building Isabelle logics ${LOGICS}. This may take some time."
./build -b -i "${LOGICS}" || die "building logics failed"
./bin/isabelle makeall || die "isabelle makeall failed"
if use graphbrowsing
then
rm -f "${S}/lib/browser/GraphBrowser.jar" \
|| die "failed cleaning graph browser directory"
pushd "${S}/lib/browser" \
|| die "Could not change directory to lib/browser"
./build || die "failed building the graph browser"
popd
fi
if use pide; then
pushd "${S}/src/Tools/jEdit" \
|| die "Could not change directory to src/Tools/jEdit"
"${S}"/bin/isabelle jedit -b -f \
|| die "pide build failed"
popd
# The jedit_build stuff is only required to build
# Isabelle/jEdit Prover IDE (PIDE). These 2 lines need to be deleted
# from etc/settings as the jedit_build source code is not installed
sed -e '/ISABELLE_JEDIT_BUILD_HOME/d' \
-e '/init_component/d' \
-i "${S}/etc/settings" \
|| die "Could not delete jedit_build lines from etc/settings"
fi
}
src_test() {
einfo "Running tests. A test run can take up to several hours!"
./build -b -t || die "tests failed"
}
src_install() {
exeinto ${TARGETDIR}/bin
doexe bin/isabelle-process bin/isabelle
insinto ${TARGETDIR}
doins -r src
doins -r lib
docompress -x /usr/share/doc/${PF}
dodoc -r doc
if use doc; then
dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc"
# The build of sci-mathematics/haskabelle with use doc requires
# sci-mathematics/isabelle[doc?]. The haskabelle doc build requires
# the doc-src directory stuff in the isabelle package. Which is not
# provided in the Isabelle 2012 src tarball. So extract it from a
# snapshot of the isabelle repo taken soon after the Isabelle 2012
# release.
doins -r doc-src
for i in "./doc-src/IsarRef/showsymbols" \
"./doc-src/TutorialI/Overview/LNCS/makeDemo" \
"./doc-src/TutorialI/isa-index" \
"./doc-src/sedindex"
do
exeinto $(dirname "${TARGETDIR}/${i}")
doexe ${i}
done
fi
for i in "./build" \
"./src/Pure/mk" \
"./src/Pure/build-jars" \
"./src/Tools/JVM/build" \
"./src/Tools/JVM/java_ext_dirs" \
"./src/Tools/jEdit/lib/Tools/jedit" \
"./src/Tools/Metis/fix_metis_license" \
"./src/Tools/Metis/make_metis" \
"./src/Tools/Metis/scripts/mlpp" \
"./src/Tools/WWW_Find/lib/Tools/wwwfind" \
"./src/Tools/Code/lib/Tools/codegen" \
"./src/HOL/Mirabelle/lib/Tools/mirabelle" \
"./src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \
"./src/HOL/Tools/SMT/lib/scripts/remote_smt" \
"./src/HOL/Tools/ATP/scripts/remote_atp" \
"./src/HOL/Tools/ATP/scripts/spass" \
"./src/HOL/Mutabelle/lib/Tools/mutabelle" \
"./src/HOL/TPTP/TPTP_Parser/make_mlyacclib" \
"./src/HOL/TPTP/TPTP_Parser/make_tptp_parser" \
"./src/HOL/TPTP/lib/Tools/tptp_isabelle_demo" \
"./src/HOL/TPTP/lib/Tools/tptp_graph" \
"./src/HOL/TPTP/lib/Tools/tptp_isabelle_comp" \
"./src/HOL/TPTP/lib/Tools/tptp_refute" \
"./src/HOL/TPTP/lib/Tools/tptp_translate" \
"./src/HOL/TPTP/lib/Tools/tptp_sledgehammer" \
"./src/HOL/TPTP/lib/Tools/tptp_nitpick" \
"./src/HOL/Library/Sum_of_Squares/neos_csdp_client" \
"./src/HOL/IMP/export.sh" \
"./lib/browser/build" \
"./lib/Tools/tty" \
"./lib/Tools/mkproject" \
"./lib/Tools/keywords" \
"./lib/Tools/browser" \
"./lib/Tools/install" \
"./lib/Tools/mkdir" \
"./lib/Tools/unsymbolize" \
"./lib/Tools/getenv" \
"./lib/Tools/java" \
"./lib/Tools/make" \
"./lib/Tools/emacs" \
"./lib/Tools/scala" \
"./lib/Tools/print" \
"./lib/Tools/latex" \
"./lib/Tools/findlogics" \
"./lib/Tools/doc" \
"./lib/Tools/logo" \
"./lib/Tools/usedir" \
"./lib/Tools/yxml" \
"./lib/Tools/version" \
"./lib/Tools/makeall" \
"./lib/Tools/scalac" \
"./lib/Tools/document" \
"./lib/Tools/env" \
"./lib/Tools/display" \
"./lib/Tools/dimacs2hol" \
"./lib/scripts/keywords" \
"./lib/scripts/unsymbolize" \
"./lib/scripts/run-polyml" \
"./lib/scripts/run-smlnj" \
"./lib/scripts/feeder" \
"./lib/scripts/yxml" \
"./lib/scripts/polyml-version" \
"./lib/scripts/process"
do
exeinto $(dirname "${TARGETDIR}/${i}")
doexe ${i}
done
dodir /etc/isabelle
insinto /etc/isabelle
doins -r etc/*
dosym /etc/isabelle "${TARGETDIR}/etc"
dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
insinto ${LIBDIR}
doins -r heaps
bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \
|| die "isabelle install failed"
newicon lib/icons/isabelle.xpm "${PN}.xpm"
dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README
java-pkg_regjar \
"${ED}${TARGETDIR}/src/Tools/JVM/java_ext_dirs.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/QuickNotepad.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Console.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/ErrorList.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Hyperlinks.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/SideKick.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/cobra.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/js.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/scala-compiler.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jedit.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \
"${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar"
}
pkg_postinst() {
# If any of the directories in /etc/isabelle/components do not exist, then
# even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to
# to delete any non-existing directories. If an old Isabelle version was
# installed with component ebuilds like sci-mathematics/e, then the
# Isabelle version is upgraded, then the contrib directories will not
# exist initially, it is necessary to delete them from /etc/isabelle/components.
# Then these components are rebuilt (creating these directories) using the
# EAPI=5 subslot depends.
for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components")
do
if [ ! -d /usr/share/Isabelle2012/${i} ]; then
sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components"
fi
done
if use ledit && use readline; then
elog "Both readline and ledit use flags specified. The default setting"
elog "if both are installed is to use readline (rlwrap), this can be"
elog "modfied by editing the ISABELLE_LINE_EDITOR setting in"
elog "${ROOT}/etc/isabelle/settings"
fi
elog "Please ensure you have a pdf viewer installed, for example:"
elog "As root: emerge app-text/zathura-pdf-poppler"
elog "Please configure your preferred pdf viewer, something like:"
elog "As normal user: xdg-mime default zathura.desktop application/pdf"
elog "Or alternatively by editing the PDF_VIEWER variable in the system"
elog "settings file ${ROOT}etc/isabelle/settings and/or the user"
elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings"
elog "To improve sledgehammer performance, consider installing:"
elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass"
elog "For nitpick it is necessary to install:"
elog "emerge sci-mathematics/kodkodi"
}

353
sci-mathematics/isabelle/isabelle-2013-r2.ebuild
View File

@@ -1,353 +0,0 @@
# Copyright 1999-2015 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Id$
EAPI="5"
inherit eutils java-pkg-2 multilib versionator
MY_PN="Isabelle"
MY_PV=$(replace_all_version_separators '-')
MY_P="${MY_PN}${MY_PV}"
JEDIT_PV="20130104"
JEDIT_PN="jedit_build"
JEDIT_P="${JEDIT_PN}-${JEDIT_PV}"
JEDIT_IC_PN="${JEDIT_PN}-isabelle-component"
JEDIT_IC_P="${JEDIT_IC_PN}-${JEDIT_PV}"
JFREECHART_PV="1.0.14"
JFREECHART_PN="jfreechart"
JFREECHART_P="${JFREECHART_PN}-${JFREECHART_PV}"
JFREECHART_IC_PN="${JFREECHART_PN}-isabelle-component"
JFREECHART_IC_P="${JFREECHART_IC_PN}-${JFREECHART_PV}"
SS="2.10"
DESCRIPTION="Isabelle is a generic proof assistant"
HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html"
SRC_URI="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/${MY_P}.tar.gz
http://isabelle.in.tum.de/components/${JEDIT_P}.tar.gz -> ${JEDIT_IC_P}.tar.gz
http://isabelle.in.tum.de/components/${JFREECHART_P}.tar.gz -> ${JFREECHART_IC_P}.tar.gz"
LICENSE="BSD"
SLOT="0/${PV}"
KEYWORDS="~amd64 ~x86"
IUSE="doc graphbrowsing ledit readline proofgeneral"
#upstream says
#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
#for document preparation: complete LaTeX
DEPEND=">=app-shells/bash-3.0:*
dev-java/ant-core:0
>=dev-java/jcommon-1.0.18:1.0
>=dev-java/jfreechart-1.0.14:1.0
>=dev-java/itext-2.1.5:0
dev-java/xml-xmlbeans:1
>=dev-lang/ghc-7.6.3
>=dev-lang/polyml-5.5.0:=[-portable]
>=dev-lang/perl-5.8.8-r2
dev-lang/swi-prolog
virtual/jdk:1.7
doc? (
virtual/latex-base
dev-tex/rail
)
>=dev-lang/scala-2.10.2:${SS}
ledit? (
app-misc/ledit
)
readline? (
app-misc/rlwrap
)"
RDEPEND="dev-perl/libwww-perl
sci-mathematics/sha1-polyml
>=virtual/jre-1.7
proofgeneral? (
>=app-emacs/proofgeneral-4.1
)
${DEPEND}"
S="${WORKDIR}"/Isabelle${MY_PV}
JEDIT_S="${WORKDIR}/${JEDIT_P}"
JFREECHART_S="${WORKDIR}/${JFREECHART_P}"
TARGETDIR="/usr/share/Isabelle"${MY_PV}
LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
LIBRARY_PKGS="scala-${SS},itext,jcommon-1.0,jfreechart-1.0,xml-xmlbeans-1"
src_unpack() {
unpack "${MY_P}.tar.gz"
pushd "${S}/contrib" || die
unpack ${JEDIT_IC_P}.tar.gz
unpack ${JFREECHART_IC_P}.tar.gz
}
pkg_setup() {
java-pkg-2_pkg_setup
}
src_prepare() {
java-pkg-2_src_prepare
java-pkg_getjars ${LIBRARY_PKGS}
epatch "${FILESDIR}/${PN}-2013-gentoo-settings.patch"
epatch "${FILESDIR}/${PN}-2013-classpath.patch"
polymlver=$(poly -v | cut -d' ' -f2)
polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
sed -e "s@5.5.0@${polymlver}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml version in etc/settings"
sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml ML_HOME in etc/settings"
sed -e "s@x86_64@${polymlarch}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml arch in etc/settings"
sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \
-i "${S}/etc/settings" \
|| die "Could not configure PROOFGENERAL_HOME in etc/settings"
sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure Isabelle lib directory in etc/settings"
epatch "${FILESDIR}/${PN}-2012-graphbrowser.patch"
epatch "${FILESDIR}/${PN}-2012-libsha1.patch"
# this example fails to compile with swi-prolog 6.5.2, so patch it so that
# Isabelle will build, then reverse the patch so that the user can see the
# original code.
epatch "${FILESDIR}/${PN}-2013-HOL-Predicate_Compile_Examples.patch"
cat <<- EOF >> "${S}/etc/settings"
ISABELLE_GHC="${ROOT}usr/bin/ghc"
ISABELLE_OCAML="${ROOT}usr/bin/ocaml"
ISABELLE_SWIPL="${ROOT}usr/bin/swipl"
ISABELLE_JDK_HOME="\$(java-config --jdk-home)"
SCALA_HOME="${ROOT}usr/share/scala-${SS}"
SHA1_HOME="/usr/$(get_libdir)/sha1-polyml"
EOF
cat <<- EOF >> "${S}/etc/components"
#bundled components
contrib/${JEDIT_P}
contrib/${JFREECHART_P}
EOF
if use ledit && ! use readline; then
epatch "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch"
fi
rm -f "${S}/contrib/jfreechart-1.0.14/lib/iText-2.1.5.jar" \
"${S}/contrib/jfreechart-1.0.14/lib/jfreechart-1.0.14.jar" \
"${S}/contrib/jfreechart-1.0.14/lib/jcommon-1.0.18.jar" \
"${S}/lib/classes/ext/scala-actors.jar" \
"${S}/lib/classes/ext/scala-compiler.jar" \
"${S}/lib/classes/ext/scala-library.jar" \
"${S}/lib/classes/ext/scala-reflect.jar" \
"${S}/lib/classes/ext/scala-swing.jar" \
|| die "Could not rm bundled jar files supplied by Gentoo"
}
src_compile() {
einfo "Building Isabelle. This may take some time."
./bin/isabelle build -a -b -s -v || die "isabelle build failed"
epatch --reverse "${FILESDIR}/${PN}-2013-HOL-Predicate_Compile_Examples.patch"
if use graphbrowsing
then
rm -f "${S}/lib/browser/GraphBrowser.jar" \
|| die "failed cleaning graph browser directory"
pushd "${S}/lib/browser" \
|| die "Could not change directory to lib/browser"
./build || die "failed building the graph browser"
popd
fi
./bin/isabelle jedit -b -f || die "pide build failed"
}
src_install() {
exeinto ${TARGETDIR}/bin
doexe bin/isabelle-process bin/isabelle
insinto ${TARGETDIR}
doins -r src
doins -r lib
doins -r contrib
doins ROOTS
docompress -x /usr/share/doc/${PF}
dodoc -r doc
if use doc; then
dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc"
# The build of sci-mathematics/haskabelle with use doc requires
# sci-mathematics/isabelle[doc?]. The haskabelle doc build requires
# the src/Doc directory stuff in the isabelle package.
doins -r src/Doc
for i in "./src/Doc/Classes/document/build" \
"./src/Doc/Codegen/document/build" \
"./src/Doc/Functions/document/build" \
"./src/Doc/HOL/document/build" \
"./src/Doc/Intro/document/build" \
"./src/Doc/IsarImplementation/document/build" \
"./src/Doc/IsarRef/document/build" \
"./src/Doc/IsarRef/document/showsymbols" \
"./src/Doc/LaTeXsugar/document/build" \
"./src/Doc/Locales/document/build" \
"./src/Doc/Logics/document/build" \
"./src/Doc/Main/document/build" \
"./src/Doc/Nitpick/document/build" \
"./src/Doc/ProgProve/document/build" \
"./src/Doc/Ref/document/build" \
"./src/Doc/Sledgehammer/document/build" \
"./src/Doc/System/document/build" \
"./src/Doc/Tutorial/document/build" \
"./src/Doc/Tutorial/document/isa-index" \
"./src/Doc/ZF/document/build" \
"./src/Doc/fixbookmarks" \
"./src/Doc/prepare_document" \
"./src/Doc/sedindex"
do
exeinto $(dirname "${TARGETDIR}/${i}")
doexe ${i}
done
fi
for i in "./Isabelle " \
"./bin/isabelle" \
"./bin/isabelle-process" \
"./lib/Tools/browser" \
"./lib/Tools/build" \
"./lib/Tools/build_dialog" \
"./lib/Tools/components" \
"./lib/Tools/dimacs2hol" \
"./lib/Tools/display" \
"./lib/Tools/doc" \
"./lib/Tools/document" \
"./lib/Tools/emacs" \
"./lib/Tools/env" \
"./lib/Tools/findlogics" \
"./lib/Tools/getenv" \
"./lib/Tools/install" \
"./lib/Tools/java" \
"./lib/Tools/keywords" \
"./lib/Tools/latex" \
"./lib/Tools/logo" \
"./lib/Tools/make" \
"./lib/Tools/mkdir" \
"./lib/Tools/mkproject" \
"./lib/Tools/mkroot" \
"./lib/Tools/options" \
"./lib/Tools/print" \
"./lib/Tools/scala" \
"./lib/Tools/scalac" \
"./lib/Tools/tty" \
"./lib/Tools/unsymbolize" \
"./lib/Tools/usedir" \
"./lib/Tools/version" \
"./lib/Tools/yxml" \
"./lib/browser/build" \
"./lib/scripts/feeder" \
"./lib/scripts/getsettings" \
"./lib/scripts/keywords" \
"./lib/scripts/polyml-version" \
"./lib/scripts/process" \
"./lib/scripts/run-polyml" \
"./lib/scripts/run-smlnj" \
"./lib/scripts/unsymbolize" \
"./lib/scripts/yxml" \
"./src/HOL/IMP/export.sh" \
"./src/HOL/Library/Sum_of_Squares/neos_csdp_client" \
"./src/HOL/Mirabelle/lib/Tools/mirabelle" \
"./src/HOL/Mutabelle/lib/Tools/mutabelle" \
"./src/HOL/SPARK/Examples/README" \
"./src/HOL/TPTP/TPTP_Parser/make_mlyacclib" \
"./src/HOL/TPTP/TPTP_Parser/make_tptp_parser" \
"./src/HOL/TPTP/lib/Tools/tptp_graph" \
"./src/HOL/TPTP/lib/Tools/tptp_isabelle" \
"./src/HOL/TPTP/lib/Tools/tptp_isabelle_hot" \
"./src/HOL/TPTP/lib/Tools/tptp_nitpick" \
"./src/HOL/TPTP/lib/Tools/tptp_refute" \
"./src/HOL/TPTP/lib/Tools/tptp_sledgehammer" \
"./src/HOL/Tools/ATP/scripts/dummy_atp" \
"./src/HOL/Tools/ATP/scripts/remote_atp" \
"./src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version" \
"./src/HOL/Tools/SMT/lib/scripts/remote_smt" \
"./src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py" \
"./src/HOL/Tools/Sledgehammer/MaSh/src/mash.py" \
"./src/Pure/build" \
"./src/Pure/build-jars" \
"./src/Tools/Code/lib/Tools/codegen" \
"./src/Tools/Graphview/lib/Tools/graphview" \
"./src/Tools/Metis/fix_metis_license" \
"./src/Tools/Metis/make_metis" \
"./src/Tools/Metis/scripts/mlpp" \
"./src/Tools/WWW_Find/lib/Tools/wwwfind" \
"./src/Tools/jEdit/lib/Tools/jedit"
do
exeinto $(dirname "${TARGETDIR}/${i}")
doexe ${i}
done
insinto /etc/isabelle
doins -r etc/*
dosym /etc/isabelle "${TARGETDIR}/etc"
dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
insinto ${LIBDIR}
doins -r heaps
bin/isabelle install -d ${TARGETDIR} "${ED}usr/bin" \
|| die "isabelle install failed"
newicon lib/icons/isabelle.xpm "${PN}.xpm"
dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README
java-pkg_regjar \
"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/Highlight.jar" \
"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/ErrorList.jar" \
"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/Console.jar" \
"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/cobra.jar" \
"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/js.jar" \
"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/jedit-5.0.0-patched/jedit.jar" \
"${ED}${TARGETDIR}/contrib/jedit_build-20130104/contrib/jedit-5.0.0-patched/jars/QuickNotepad.jar" \
"${ED}${TARGETDIR}/contrib/jfreechart-1.0.14/jfreechart-1.0.14-demo.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/Graphview.jar" \
"${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Console.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/ErrorList.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Highlight.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/QuickNotepad.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/SideKick.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/cobra.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/js.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jedit.jar"
}
pkg_postinst() {
# If any of the directories in /etc/isabelle/components do not exist, then
# even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to
# to delete any non-existing directories. If an old Isabelle version was
# installed with component ebuilds like sci-mathematics/e, then the
# Isabelle version is upgraded, then the contrib directories will not
# exist initially, it is necessary to delete them from /etc/isabelle/components.
# Then these components are rebuilt (creating these directories) using the
# EAPI=5 subslot depends.
for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components")
do
if [ ! -d /usr/share/${MY_P}/${i} ]; then
sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components"
fi
done
if use ledit && use readline; then
elog "Both readline and ledit use flags specified. The default setting"
elog "if both are installed is to use readline (rlwrap), this can be"
elog "modfied by editing the ISABELLE_LINE_EDITOR setting in"
elog "${ROOT}/etc/isabelle/settings"
fi
elog "Please ensure you have a pdf viewer installed, for example:"
elog "As root: emerge app-text/zathura-pdf-poppler"
elog "Please configure your preferred pdf viewer, something like:"
elog "As normal user: xdg-mime default zathura.desktop application/pdf"
elog "Or alternatively by editing the PDF_VIEWER variable in the system"
elog "settings file ${ROOT}etc/isabelle/settings and/or the user"
elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings"
elog "To improve sledgehammer performance, consider installing:"
elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass"
elog "For nitpick it is necessary to install:"
elog "emerge sci-mathematics/kodkodi"
}

375
sci-mathematics/isabelle/isabelle-2013.2-r1.ebuild
View File

@@ -1,375 +0,0 @@
# Copyright 1999-2015 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Id$
EAPI="5"
inherit eutils java-pkg-2 multilib versionator
MY_PN="Isabelle"
MY_PV=$(replace_all_version_separators '-')
MY_P="${MY_PN}${MY_PV}"
JEDIT_PV="20131106"
JEDIT_PN="jedit_build"
JEDIT_P="${JEDIT_PN}-${JEDIT_PV}"
JEDIT_IC_PN="${JEDIT_PN}-isabelle-component"
JEDIT_IC_P="${JEDIT_IC_PN}-${JEDIT_PV}"
JFREECHART_PV="1.0.14-1"
JFREECHART_PN="jfreechart"
JFREECHART_P="${JFREECHART_PN}-${JFREECHART_PV}"
JFREECHART_IC_PN="${JFREECHART_PN}-isabelle-component"
JFREECHART_IC_P="${JFREECHART_IC_PN}-${JFREECHART_PV}"
POLYML_PV="5.5.1-1"
POLYML_PN="polyml"
POLYML_P="${POLYML_PN}-${POLYML_PV}"
POLYML_IC_PN="${POLYML_PN}-isabelle-component"
POLYML_IC_P="${POLYML_IC_PN}-${POLYML_PV}"
SS="2.11"
DESCRIPTION="Isabelle is a generic proof assistant"
HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html"
SRC_URI="http://www.cl.cam.ac.uk/users/lcp/archive/${MY_P}.tar.gz
http://isabelle.in.tum.de/components/${JEDIT_P}.tar.gz -> ${JEDIT_IC_P}.tar.gz
http://isabelle.in.tum.de/dist/contrib/${JFREECHART_P}.tar.gz -> ${JFREECHART_IC_P}.tar.gz
https://dev.gentoo.org/~gienah/snapshots/${POLYML_IC_P}.tar.gz"
LICENSE="BSD"
SLOT="0/${PV}"
KEYWORDS="~amd64 ~x86"
IUSE="doc graphbrowsing ledit readline proofgeneral"
#upstream says
#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
#for document preparation: complete LaTeX
DEPEND=">=app-shells/bash-3.0:*
dev-java/ant-core:0
>=dev-java/jcommon-1.0.18:1.0
>=dev-java/jfreechart-1.0.14:1.0
>=dev-java/itext-2.1.5:0
dev-java/xml-xmlbeans:1
dev-java/xz-java:0
>=dev-lang/ghc-7.6.3
>=dev-lang/polyml-5.5.1:=[-portable]
>=dev-lang/perl-5.8.8-r2
dev-lang/swi-prolog
virtual/jdk:1.7
doc? (
virtual/latex-base
dev-tex/rail
)
>=dev-lang/scala-2.11.1:${SS}
ledit? (
app-misc/ledit
)
readline? (
app-misc/rlwrap
)"
RDEPEND="dev-perl/libwww-perl
sci-mathematics/sha1-polyml
>=virtual/jre-1.7
proofgeneral? (
>=app-emacs/proofgeneral-4.1
)
${DEPEND}"
S="${WORKDIR}"/Isabelle${MY_PV}
JEDIT_S="${WORKDIR}/${JEDIT_P}"
JFREECHART_S="${WORKDIR}/${JFREECHART_P}"
TARGETDIR="/usr/share/Isabelle"${MY_PV}
LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
# Notes on QA warnings: * Class files not found via DEPEND in package.env
# Stuff with $ in the name appear to be spurious:
# isabelle/Markup_Tree$$anonfun$results$1$1.class
# scala/tools/nsc/backend/jvm/GenJVM$BytecodeGenerator$$anonfun$computeLocalVarsIndex$1.class
# It wants javafx, I am unsure how to fix this. I test isabelle with the Sun JDK:
# javafx/application/Platform.class javafx
# Presumably the user can provide the jEdit plugins if they are necessary:
# marker/MarkerSetsPlugin.class http://plugins.jedit.org/plugins/?MarkerSets
# projectviewer/gui/OptionPaneBase.class http://plugins.jedit.org/plugins/?ProjectViewer
LIBRARY_PKGS="ant-core,itext,jcommon-1.0,jfreechart-1.0,scala-${SS},xml-xmlbeans-1,xz-java"
src_unpack() {
unpack "${MY_P}.tar.gz"
pushd "${S}/contrib" || die
unpack ${JEDIT_IC_P}.tar.gz
unpack ${JFREECHART_IC_P}.tar.gz
unpack ${POLYML_IC_P}.tar.gz
}
pkg_setup() {
java-pkg-2_pkg_setup
}
src_prepare() {
java-pkg-2_src_prepare
java-pkg_getjars ${LIBRARY_PKGS}
epatch "${FILESDIR}/${PN}-2013-gentoo-settings.patch"
epatch "${FILESDIR}/${PN}-2013.2-classpath.patch"
polymlver=$(poly -v | cut -d' ' -f2)
polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
sed -e "s@5.5.0@${polymlver}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml version in etc/settings"
sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml ML_HOME in etc/settings"
sed -e "s@x86_64@${polymlarch}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure polyml arch in etc/settings"
sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \
-i "${S}/etc/settings" \
|| die "Could not configure PROOFGENERAL_HOME in etc/settings"
sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \
-i "${S}/etc/settings" \
|| die "Could not configure Isabelle lib directory in etc/settings"
epatch "${FILESDIR}/${PN}-2012-graphbrowser.patch"
epatch "${FILESDIR}/${PN}-2012-libsha1.patch"
# this example fails to compile with swi-prolog 6.5.2, so patch it so that
# Isabelle will build, then reverse the patch so that the user can see the
# original code.
epatch "${FILESDIR}/${PN}-2013.2-HOL-Predicate_Compile_Examples.patch"
cat <<- EOF >> "${S}/etc/settings"
ISABELLE_GHC="${ROOT}usr/bin/ghc"
ISABELLE_OCAML="${ROOT}usr/bin/ocaml"
ISABELLE_SWIPL="${ROOT}usr/bin/swipl"
ISABELLE_JDK_HOME="\$(java-config --jdk-home)"
SCALA_HOME="${ROOT}usr/share/scala-${SS}"
SHA1_HOME="/usr/$(get_libdir)/sha1-polyml"
EOF
cat <<- EOF >> "${S}/etc/components"
#bundled components
contrib/${JEDIT_P}
contrib/${JFREECHART_P}
contrib/${POLYML_P}
EOF
if use ledit && ! use readline; then
epatch "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch"
fi
rm -f "${S}/contrib/jfreechart-1.0.14-1/lib/iText-2.1.5.jar" \
"${S}/contrib/jfreechart-1.0.14-1/lib/jfreechart-1.0.14.jar" \
"${S}/contrib/jfreechart-1.0.14-1/lib/jcommon-1.0.18.jar" \
"${S}/lib/classes/ext/scala-actors.jar" \
"${S}/lib/classes/ext/scala-compiler.jar" \
"${S}/lib/classes/ext/scala-library.jar" \
"${S}/lib/classes/ext/scala-reflect.jar" \
"${S}/lib/classes/ext/scala-swing.jar" \
|| die "Could not rm bundled jar files supplied by Gentoo"
}
src_compile() {
einfo "Building Isabelle. This may take some time."
./bin/isabelle build -a -b -s -v || die "isabelle build failed"
epatch --reverse "${FILESDIR}/${PN}-2013.2-HOL-Predicate_Compile_Examples.patch"
if use graphbrowsing
then
rm -f "${S}/lib/browser/GraphBrowser.jar" \
|| die "failed cleaning graph browser directory"
pushd "${S}/lib/browser" \
|| die "Could not change directory to lib/browser"
./build || die "failed building the graph browser"
popd
fi
./bin/isabelle jedit -b -f || die "pide build failed"
}
src_install() {
insinto ${TARGETDIR}
doins -r src
doins -r lib
doins -r contrib
doins ROOTS
docompress -x /usr/share/doc/${PF}
dodoc -r doc
if use doc; then
dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc"
# The build of sci-mathematics/haskabelle with use doc requires
# sci-mathematics/isabelle[doc?]. The haskabelle doc build requires
# the src/Doc directory stuff in the isabelle package.
doins -r src/Doc
for i in "./src/Doc/Classes/document/build" \
"./src/Doc/Codegen/document/build" \
"./src/Doc/Datatypes/document/build" \
"./src/Doc/fixbookmarks" \
"./src/Doc/Functions/document/build" \
"./src/Doc/Intro/document/build" \
"./src/Doc/IsarImplementation/document/build" \
"./src/Doc/IsarRef/document/build" \
"./src/Doc/IsarRef/document/showsymbols" \
"./src/Doc/JEdit/document/build" \
"./src/Doc/LaTeXsugar/document/build" \
"./src/Doc/Locales/document/build" \
"./src/Doc/Logics/document/build" \
"./src/Doc/Main/document/build" \
"./src/Doc/Nitpick/document/build" \
"./src/Doc/prepare_document" \
"./src/Doc/ProgProve/document/build" \
"./src/Doc/sedindex" \
"./src/Doc/Sledgehammer/document/build" \
"./src/Doc/System/document/build" \
"./src/Doc/Tutorial/document/build" \
"./src/Doc/Tutorial/document/isa-index" \
"./src/Doc/ZF/document/build"
do
exeinto $(dirname "${TARGETDIR}/${i}")
doexe ${i}
done
fi
for i in "./bin/isabelle" \
"./bin/isabelle-process" \
"./bin/isabelle_scala_script" \
"./lib/browser/build" \
"./lib/scripts/feeder" \
"./lib/scripts/getsettings" \
"./lib/scripts/polyml-version" \
"./lib/scripts/process" \
"./lib/scripts/run-polyml" \
"./lib/scripts/run-polyml-5.5.1" \
"./lib/scripts/run-smlnj" \
"./lib/scripts/unsymbolize" \
"./lib/scripts/update_sub_sup" \
"./lib/scripts/yxml" \
"./lib/Tools/browser" \
"./lib/Tools/build" \
"./lib/Tools/components" \
"./lib/Tools/display" \
"./lib/Tools/doc" \
"./lib/Tools/document" \
"./lib/Tools/emacs" \
"./lib/Tools/env" \
"./lib/Tools/findlogics" \
"./lib/Tools/getenv" \
"./lib/Tools/install" \
"./lib/Tools/java" \
"./lib/Tools/keywords" \
"./lib/Tools/latex" \
"./lib/Tools/logo" \
"./lib/Tools/mkroot" \
"./lib/Tools/options" \
"./lib/Tools/scala" \
"./lib/Tools/scalac" \
"./lib/Tools/tty" \
"./lib/Tools/unsymbolize" \
"./lib/Tools/update_sub_sup" \
"./lib/Tools/version" \
"./lib/Tools/yxml" \
"./src/HOL/IMP/export.sh" \
"./src/HOL/Library/Sum_of_Squares/neos_csdp_client" \
"./src/HOL/Mirabelle/lib/Tools/mirabelle" \
"./src/HOL/Mutabelle/lib/Tools/mutabelle" \
"./src/HOL/SPARK/Examples/README" \
"./src/HOL/Tools/ATP/scripts/dummy_atp" \
"./src/HOL/Tools/ATP/scripts/remote_atp" \
"./src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py" \
"./src/HOL/Tools/Sledgehammer/MaSh/src/mash.py" \
"./src/HOL/Tools/Sledgehammer/MaSh/src/server.py" \
"./src/HOL/Tools/SMT/lib/scripts/remote_smt" \
"./src/HOL/TPTP/lib/Tools/tptp_graph" \
"./src/HOL/TPTP/lib/Tools/tptp_isabelle" \
"./src/HOL/TPTP/lib/Tools/tptp_isabelle_hot" \
"./src/HOL/TPTP/lib/Tools/tptp_nitpick" \
"./src/HOL/TPTP/lib/Tools/tptp_refute" \
"./src/HOL/TPTP/lib/Tools/tptp_sledgehammer" \
"./src/HOL/TPTP/TPTP_Parser/make_mlyacclib" \
"./src/HOL/TPTP/TPTP_Parser/make_tptp_parser" \
"./src/Pure/build" \
"./src/Pure/build-jars" \
"./src/Tools/Code/lib/Tools/codegen" \
"./src/Tools/Graphview/lib/Tools/graphview" \
"./src/Tools/jEdit/lib/Tools/jedit" \
"./src/Tools/Metis/fix_metis_license" \
"./src/Tools/Metis/make_metis" \
"./src/Tools/Metis/scripts/mlpp" \
"./src/Tools/WWW_Find/lib/Tools/wwwfind"
do
exeinto $(dirname "${TARGETDIR}/${i}")
doexe ${i}
done
insinto /etc/isabelle
doins -r etc/*
dosym /etc/isabelle "${TARGETDIR}/etc"
dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
insinto ${LIBDIR}
doins -r heaps
bin/isabelle install -d ${TARGETDIR} "${ED}usr/bin" \
|| die "isabelle install failed"
newicon lib/icons/"${PN}.xpm" "${PN}.xpm"
newicon lib/icons/"${PN}-mini.xpm" "${PN}-mini.xpm"
dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README
java-pkg_regjar \
"${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/Console.jar" \
"${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/ErrorList.jar" \
"${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/Highlight.jar" \
"${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/idea-icons.jar" \
"${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/jedit-5.1.0-patched/jars/QuickNotepad.jar" \
"${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/jedit-5.1.0-patched/jedit.jar" \
"${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/jsr305-2.0.0.jar" \
"${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/MacOSX.jar" \
"${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/SideKick.jar" \
"${ED}${TARGETDIR}/contrib/${JFREECHART_P}/jfreechart-1.0.14-demo.jar" \
"${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \
"${ED}${TARGETDIR}/lib/classes/Graphview.jar" \
"${ED}${TARGETDIR}/lib/classes/Pure.jar" \
"${ED}${TARGETDIR}/lib/classes/scala-actors.jar" \
"${ED}${TARGETDIR}/lib/classes/scala-compiler.jar" \
"${ED}${TARGETDIR}/lib/classes/scala-library.jar" \
"${ED}${TARGETDIR}/lib/classes/scala-reflect.jar" \
"${ED}${TARGETDIR}/lib/classes/scala-swing.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Console.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/ErrorList.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Highlight.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/idea-icons.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/jsr305-2.0.0.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/MacOSX.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/QuickNotepad.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/SideKick.jar" \
"${ED}${TARGETDIR}/src/Tools/jEdit/dist/jedit.jar"
}
pkg_postinst() {
# If any of the directories in /etc/isabelle/components do not exist, then
# even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to
# to delete any non-existing directories. If an old Isabelle version was
# installed with component ebuilds like sci-mathematics/e, then the
# Isabelle version is upgraded, then the contrib directories will not
# exist initially, it is necessary to delete them from /etc/isabelle/components.
# Then these components are rebuilt (creating these directories) using the
# EAPI=5 subslot depends.
for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components")
do
if [ ! -d /usr/share/${MY_P}/${i} ]; then
sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components"
fi
done
if use ledit && use readline; then
elog "Both readline and ledit use flags specified. The default setting"
elog "if both are installed is to use readline (rlwrap), this can be"
elog "modfied by editing the ISABELLE_LINE_EDITOR setting in"
elog "${ROOT}/etc/isabelle/settings"
fi
elog "Please ensure you have a pdf viewer installed, for example:"
elog "As root: emerge app-text/zathura-pdf-poppler"
elog "Please configure your preferred pdf viewer, something like:"
elog "As normal user: xdg-mime default zathura.desktop application/pdf"
elog "Or alternatively by editing the PDF_VIEWER variable in the system"
elog "settings file ${ROOT}etc/isabelle/settings and/or the user"
elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings"
elog "To improve sledgehammer performance, consider installing:"
elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass"
elog "For nitpick it is necessary to install:"
elog "emerge sci-mathematics/kodkodi"
}

15
sci-mathematics/isabelle/metadata.xml
View File

@@ -18,20 +18,6 @@ correctness of computer hardware or software and proving
properties of computer languages and protocols.
</longdescription>
<use>
<flag name="Pure">Pure is the basis for all object-logics.</flag>
<flag name="FOL">FOL (Many-sorted First-Order Logic) provides basic
classical and intuitionistic first-order logic. It is polymorphic.</flag>
<flag name="HOL">(Higher-Order Logic) is a version of classical higher-order
logic resembling that of the HOL System.</flag>
<flag name="ZF">ZF (Set Theory) offers a formulation of Zermelo-Fraenkel
set theory on top of FOL.</flag>
<flag name="CCL">CCL (Classical Computational Logic)</flag>
<flag name="CTT">CTT (Constructive Type Theory) is an extensional version
of Martin-Löf's Type Theory.</flag>
<flag name="Cube">Cube (The Lambda Cube)</flag>
<flag name="FOLP">FOLP (FOL with Proof Terms)</flag>
<flag name="LCF">LCF (Logic of Computable Functions)</flag>
<flag name="Sequents">Sequents (first-order, modal and linear logics)</flag>
<flag name="graphbrowsing">Generate theory browsing information,
including HTML documents that show a theory's definition, the
theorems proved in its ML file and the relationship with its
@@ -41,6 +27,5 @@ properties of computer languages and protocols.
editor</flag>
<flag name="proofgeneral">Add support for the
<pkg>app-emacs/proofgeneral</pkg> proof assistant front end.</flag>
<flag name="pide">Build Isabelle/jEdit Prover IDE (PIDE).</flag>
</use>
</pkgmetadata>