proj/gentoo: Initial commit

This commit represents a new era for Gentoo:
Storing the gentoo-x86 tree in Git, as converted from CVS.

This commit is the start of the NEW history.
Any historical data is intended to be grafted onto this point.

Creation process:
1. Take final CVS checkout snapshot
2. Remove ALL ChangeLog* files
3. Transform all Manifests to thin
4. Remove empty Manifests
5. Convert all stale $Header$/$Id$ CVS keywords to non-expanded Git $Id$
5.1. Do not touch files with -kb/-ko keyword flags.

Signed-off-by: Robin H. Johnson <robbat2@gentoo.org>
X-Thanks: Alec Warner <antarus@gentoo.org> - did the GSoC 2006 migration tests
X-Thanks: Robin H. Johnson <robbat2@gentoo.org> - infra guy, herding this project
X-Thanks: Nguyen Thai Ngoc Duy <pclouds@gentoo.org> - Former Gentoo developer, wrote Git features for the migration
X-Thanks: Brian Harring <ferringb@gentoo.org> - wrote much python to improve cvs2svn
X-Thanks: Rich Freeman <rich0@gentoo.org> - validation scripts
X-Thanks: Patrick Lauer <patrick@gentoo.org> - Gentoo dev, running new 2014 work in migration
X-Thanks: Michał Górny <mgorny@gentoo.org> - scripts, QA, nagging
X-Thanks: All of other Gentoo developers - many ideas and lots of paint on the bikeshed

16 files changed, 725 insertions, 0 deletions

diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-gentoo-settings.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-gentoo-settings.patch
new file mode 100644
index 000000000000..67e3476f2170
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2011.1-gentoo-settings.patch
@@ -0,0 +1,39 @@
+--- 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=""
diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch
new file mode 100644
index 000000000000..ed8036a9b2d4
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch
@@ -0,0 +1,11 @@
+--- 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
+ 
diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-libsha1.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-libsha1.patch
new file mode 100644
index 000000000000..905a1eb60e5f
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2011.1-libsha1.patch
@@ -0,0 +1,11 @@
+--- 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 =
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
new file mode 100644
index 000000000000..67e3476f2170
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2011.1-proofgeneral-gentoo-path.patch
@@ -0,0 +1,39 @@
+--- 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=""
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
new file mode 100644
index 000000000000..b2f2c35ee087
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2011.1-reverse-line-editor-order.patch
@@ -0,0 +1,12 @@
+--- 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)"
+ 
+ 
+ ###
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-gentoo-settings.patch b/sci-mathematics/isabelle/files/isabelle-2012-gentoo-settings.patch
new file mode 100644
index 000000000000..8994491445d5
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2012-gentoo-settings.patch
@@ -0,0 +1,62 @@
+--- 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"
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch b/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch
new file mode 100644
index 000000000000..3e63f1c62237
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch
@@ -0,0 +1,11 @@
+--- Isabelle2012-orig/lib/browser/build	2012-05-20 19:34:33.000000000 +1000
++++ Isabelle2012/lib/browser/build	2012-05-26 22:18:41.952750622 +1000
+@@ -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
+ 
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-libsha1.patch b/sci-mathematics/isabelle/files/isabelle-2012-libsha1.patch
new file mode 100644
index 000000000000..06933669de7f
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2012-libsha1.patch
@@ -0,0 +1,11 @@
+--- Isabelle2012-orig/src/Pure/General/sha1_polyml.ML	2012-05-20 19:34:33.000000000 +1000
++++ Isabelle2012/src/Pure/General/sha1_polyml.ML	2012-12-05 23:24:06.263793934 +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 =
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
new file mode 100644
index 000000000000..18ae43d00fe5
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2012-redundant-equations-in-function-definitions-error.patch
@@ -0,0 +1,35 @@
+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)
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch b/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch
new file mode 100644
index 000000000000..233ea5b50fad
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch
@@ -0,0 +1,12 @@
+--- Isabelle2012-orig/etc/settings	2012-05-23 03:07:38.000000000 +1000
++++ Isabelle2012/etc/settings	2012-05-27 12:43:36.209715015 +1000
+@@ -62,8 +62,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)"
+ 
+ 
+ ###
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-signal-handling.patch b/sci-mathematics/isabelle/files/isabelle-2012-signal-handling.patch
new file mode 100644
index 000000000000..d238f41bd32b
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2012-signal-handling.patch
@@ -0,0 +1,8 @@
+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="$?"
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
new file mode 100644
index 000000000000..bce7eec4417c
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch
@@ -0,0 +1,82 @@
+--- 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
diff --git a/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch
new file mode 100644
index 000000000000..e3b2271a30c5
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch
@@ -0,0 +1,149 @@
+--- 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')"
+ 
diff --git a/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch b/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch
new file mode 100644
index 000000000000..7066c6b875a2
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch
@@ -0,0 +1,19 @@
+--- Isabelle2013-orig/etc/settings	2013-02-13 00:31:02.000000000 +1100
++++ Isabelle2013/etc/settings	2013-08-17 14:47:46.045988000 +1000
+@@ -176,3 +176,16 @@
+ #ISABELLE_GHC="/usr/bin/ghc"
+ #ISABELLE_OCAML="/usr/bin/ocaml"
+ #ISABELLE_SWIPL="/usr/bin/swipl"
++
++# Poly/ML Gentoo (x86_64)
++ML_PLATFORM=x86_64-linux
++ML_HOME="/usr/bin"
++ML_SYSTEM=polyml-5.5.0
++ML_OPTIONS="-H 1000"
++ML_SOURCES="/usr/src/debug/dev-lang/polyml-5.5.0"
++
++# Proof General home
++PROOFGENERAL_HOME="/usr/share/emacs/site-lisp/ProofGeneral"
++PROOFGENERAL_OPTIONS=""
++#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"
++
diff --git a/sci-mathematics/isabelle/files/isabelle-2013.2-HOL-Predicate_Compile_Examples.patch b/sci-mathematics/isabelle/files/isabelle-2013.2-HOL-Predicate_Compile_Examples.patch
new file mode 100644
index 000000000000..e1253016837b
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2013.2-HOL-Predicate_Compile_Examples.patch
@@ -0,0 +1,89 @@
+--- Isabelle2013-2-orig/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	2013-12-06 02:18:50.000000000 +1100
++++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	2014-02-09 22:21:20.676081140 +1100
+@@ -87,7 +87,7 @@
+ *}
+ 
+ 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 *}
+@@ -115,7 +115,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 *} 
+@@ -151,7 +151,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-2-orig/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	2013-12-06 02:18:50.000000000 +1100
++++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	2014-02-09 22:27:26.826238011 +1100
+@@ -36,7 +36,7 @@
+ 
+ lemma
+   "S\<^sub>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)"
+@@ -70,7 +70,7 @@
+ 
+ theorem S\<^sub>1_sound:
+ "S\<^sub>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
+ 
+ 
+@@ -94,7 +94,7 @@
+ 
+ theorem S\<^sub>2_sound:
+   "S\<^sub>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\<^sub>3 and A\<^sub>3 and B\<^sub>3 where
+@@ -171,4 +171,4 @@
+ hide_const a b
+ 
+ 
+-end
+\ No newline at end of file
++end
+--- Isabelle2013-2-orig/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	2013-12-06 02:18:50.000000000 +1100
++++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	2014-02-09 22:21:20.677081168 +1100
+@@ -95,7 +95,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-2-orig/src/HOL/Predicate_Compile_Examples/List_Examples.thy	2013-12-06 02:18:50.000000000 +1100
++++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/List_Examples.thy	2014-02-09 22:21:20.678081196 +1100
+@@ -24,7 +24,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
diff --git a/sci-mathematics/isabelle/files/isabelle-2013.2-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2013.2-classpath.patch
new file mode 100644
index 000000000000..b3ad4ae95cd9
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2013.2-classpath.patch
@@ -0,0 +1,135 @@
+--- 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
+ 
+