Patch signal handling: http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/2732 Change "Ignoring redundant equation" warning to an error to avoid proofs being undertaken on the basis of a mistaken definition: http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/2780

(Portage version: 2.1.10.65/cvs/Linux x86_64)

4 files changed, 58 insertions, 2 deletions

diff --git a/sci-mathematics/isabelle/ChangeLog b/sci-mathematics/isabelle/ChangeLog
index 5f501379ce89..f88149ff7d5a 100644
--- a/sci-mathematics/isabelle/ChangeLog
+++ b/sci-mathematics/isabelle/ChangeLog
@@ -1,6 +1,15 @@
 # ChangeLog for sci-mathematics/isabelle
 # Copyright 1999-2012 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/ChangeLog,v 1.4 2012/05/30 00:45:06 gienah Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/ChangeLog,v 1.5 2012/06/15 14:10:40 gienah Exp $
+
+  15 Jun 2012; Mark Wright <gienah@gentoo.org>
+  +files/isabelle-2012-redundant-equations-in-function-definitions-error.patch,
+  +files/isabelle-2012-signal-handling.patch, isabelle-2012.ebuild:
+  Patch signal handling:
+  http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/2732
+  Change "Ignoring redundant equation" warning to an error to avoid proofs being
+  undertaken on the basis of a mistaken definition:
+  http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/2780
 
 *isabelle-2012 (30 May 2012)
 *isabelle-2011.1-r1 (30 May 2012)
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-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/isabelle-2012.ebuild b/sci-mathematics/isabelle/isabelle-2012.ebuild
index 3d66f3f4ece9..a938d0371b22 100644
--- a/sci-mathematics/isabelle/isabelle-2012.ebuild
+++ b/sci-mathematics/isabelle/isabelle-2012.ebuild
@@ -1,6 +1,6 @@
 # Copyright 1999-2012 Gentoo Foundation
 # Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/isabelle-2012.ebuild,v 1.1 2012/05/30 00:45:06 gienah Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/isabelle-2012.ebuild,v 1.2 2012/06/15 14:10:40 gienah Exp $
 
 EAPI="4"
 
@@ -71,6 +71,10 @@ pkg_setup() {
 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" \