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

Package-Manager: portage-2.1.10.65/cvs/Linux x86_64

5 files changed, 65 insertions, 7 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/Manifest b/sci-mathematics/isabelle/Manifest
index a23c7de6dead..d1d76ee9ee90 100644
--- a/sci-mathematics/isabelle/Manifest
+++ b/sci-mathematics/isabelle/Manifest
@@ -7,20 +7,22 @@ AUX isabelle-2011.1-proofgeneral-gentoo-path.patch 1265 RMD160 9060454ab5480056b
 AUX isabelle-2011.1-reverse-line-editor-order.patch 427 RMD160 b3c672e939541e3eeb2f4a866628c668cd5d2898 SHA1 9095831f761de457915a10a5391a260de4b8b910 SHA256 1a664c94d400d88dfa5af9af3bdb4c90bacd12792286b3c4933f62ca15e5b9a0
 AUX isabelle-2012-gentoo-settings.patch 2107 RMD160 4ebd777b8c498a833d0264ddf67f367003a424f2 SHA1 b073aae7982a29bfc200c985e53051b882f3aa7d SHA256 5076d6665b367a9b08a2e56ba901028e90910a444c2c02322ebf8d9d9ac328b1
 AUX isabelle-2012-graphbrowser.patch 354 RMD160 68eaee7f3e8c8b92f608cf5936ea8a4315634b41 SHA1 508be51f17ad6bf08d5df71535298f42177a736a SHA256 0b6d3a3736ec89ad870ef24bb2ba3c2006a907e1a29a113e3f63a5ad609ec4b7
+AUX isabelle-2012-redundant-equations-in-function-definitions-error.patch 1319 RMD160 6b188f257c3736d86dda9903c45d9dfa2123b618 SHA1 999028e7f3ea4a184b7311a200ea0cff2c038134 SHA256 87d766c5140708710935bc4156fddb8901a80fa5462d22974290f85bc13b4038
 AUX isabelle-2012-reverse-line-editor-order.patch 423 RMD160 6a51017a64f70fde99decfb2e0b09e281836ec6b SHA1 ff5945dd644dba3b0fd0fcd49ec793e9bf10c2ae SHA256 51a172b46baaaa269488801bad3d46ba4ccd0e3df35b2c15dc9b75592ceb843e
+AUX isabelle-2012-signal-handling.patch 457 RMD160 a42238e2c6fba50087d1231987fddf2613ed154d SHA1 3d8fbab8cc85f0985871e8fdabc308a800cf1737 SHA256 df6e274300a8ac440fa140c7bdb130c42191a45b40067bac46fcf8141861df6f
 DIST Isabelle2011-1.tar.gz 42239059 RMD160 70dadeaf38ae71ff9871f8c5b9ba823c4d5cbcc7 SHA1 2f514bc2cff7e7f7c75a3cb15c71ea71009f8df7 SHA256 48d77fe31a16b44f6015aa7953a60bdad8fcec9e60847630dc7b98c053edfc08
 DIST Isabelle2012-doc-src.tar.gz 2688496 RMD160 cbef295dc2f6b27ab32815b9395dc38f0f344ea8 SHA1 2ed623a40488b7c200282457c240af575fe4b3e6 SHA256 e18965fe0f7f89b286d4707e38201f1edbea81f6b26aed59d63a633c03fec097
 DIST Isabelle2012.tar.gz 49529865 RMD160 62de99689ba65e2d4ff02d9590397db3d3115cf0 SHA1 9ec664d48bb15b679c7316820aa03ba37d6fc56b SHA256 b86f957dee221041f92c9d4ced4758d45b4950339743d0d58b1ea6061e2b53f0
 DIST jedit_build-20120414.tar.gz 7509120 RMD160 f3977207db8df6ccaf85015640a938cc3a475c4c SHA1 6425f622625024c1de27f3730d6811f6370a19cd SHA256 3c5840fd01b87013b05a92742d41f66f655df6fe9edef1525c6722f92d8f3e41
 EBUILD isabelle-2011.1-r1.ebuild 7158 RMD160 a6638676fb40ef87eb2ed3076b8618a451c641d7 SHA1 dfcdf9aa011a72236c5718bc16b08c31d45498fa SHA256 4a751a8893be2d92e4e1d709209ee94f68f3555e73c045136fb41ea83b918a1c
 EBUILD isabelle-2011.1.ebuild 4036 RMD160 363ef11acf50946dcde1151643e053d7c1064339 SHA1 cc9e14c8b1893c03d2efcdfd0262710b23d725e3 SHA256 6063b32c39e50c42e81051197ce46a735bb16448c13b5ff1f8af5018f07b3020
-EBUILD isabelle-2012.ebuild 9776 RMD160 9720486c161c7da9f91e35a8da831e6261679274 SHA1 1ada1c0433db06f3922c2a5f48dbc886f8dd9dd4 SHA256 a830baad156e332e30e44a4b64a77d74c78b7ec6f11aa21ebba30e52bd245d96
-MISC ChangeLog 1677 RMD160 f7e6e9579f92c0ddb4fc3073a82b76229f9d75c6 SHA1 7e1ad7c49bc7d49fe7609ebed7b0e35f5eef319c SHA256 cea75b42cd88b33a1ac5664a8bdbe0cd213c1d3f14fea91ea5a954f2148acd5d
+EBUILD isabelle-2012.ebuild 10080 RMD160 176c79f35fa5550e2b86710e8838d0d5fafab3b9 SHA1 51dca0b5e83c2909213de6655ac5e23c5080267b SHA256 310f2f53477b461184da3b39a41b622205aac41f180ff7724cd21714974146cb
+MISC ChangeLog 2189 RMD160 bc5bed517275cb98dc94a594f735097e35b0fb45 SHA1 39a8d1ef8dd945e9717240243a518ed842665161 SHA256 940938ec2179ea754503ebaa31865d6bb619c2e9744e5f4ad9f3abd9ae8c6740
 MISC metadata.xml 2157 RMD160 ee8247053938f0b3686a6e0ea8dbfe0cf925a700 SHA1 459ec3cc74b389f410d26c2da55bb89a5d842a11 SHA256 bdcce608d1d69f75e4aa0c809f85885dd025cd9ed2c1a12552a446033c4a7fa6
 -----BEGIN PGP SIGNATURE-----
 Version: GnuPG v2.0.17 (GNU/Linux)
 
-iF4EAREIAAYFAk/FbaIACgkQoBEVQmGOlx/UQAEAwuUYY2arR5bF3refK8UCYYdr
-QiY7mn286hs+ktiE5BUBAJ7Clx9wfej5m8lgWVNdobPwTmg9pJIc4VBKXuTjqHSF
-=BVGh
+iF4EAREIAAYFAk/bQm0ACgkQoBEVQmGOlx+pZAEAwfmhDzkQ6Xs89Es6xhfe8D3N
+BZjhgU+RZmrRsf7cDvsBAL8s9xF7a2iI6oAgnL0+vlvXWITCTHmfo+ISt/X5KJfe
+=u1hX
 -----END PGP SIGNATURE-----
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" \