diff options
Diffstat (limited to 'sci-mathematics/isabelle')
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" \ |