# HG changeset patch
# User blanchet
# Date 1337352218 -7200
# Node ID 49b05b9ead33ed666c9653fa68e53617e975360d
# Parent  22e00179564185f83fdf8a16e5839b1ed8a89d94
added a timeout to "try0" in Mirabelle

diff -r 22e001795641 -r 49b05b9ead33 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 18 15:08:08 2012 +0200
+++ b/src/HOL/IsaMakefile	Fri May 18 16:43:38 2012 +0200
@@ -1334,6 +1334,7 @@
   Mirabelle/Tools/mirabelle_refute.ML	\
   Mirabelle/Tools/mirabelle_sledgehammer.ML \
   Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \
+  Mirabelle/Tools/mirabelle_try0.ML \
   TPTP/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \
   Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \
   Library/Inner_Product.thy
diff -r 22e001795641 -r 49b05b9ead33 src/HOL/Mirabelle/Tools/mirabelle_try0.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML	Fri May 18 15:08:08 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_try0.ML	Fri May 18 16:43:38 2012 +0200
@@ -10,8 +10,10 @@
 fun init _ = I
 fun done _ _ = ()
 
-fun run id ({pre, (* timeout, *) log, ...}: Mirabelle.run_args) =
-  if Try0.try0 (* (SOME timeout) *) NONE ([], [], [], []) pre
+fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time)
+
+fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
+  if TimeLimit.timeLimit (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
   then log (try0_tag id ^ "succeeded")
   else ()
   handle TimeLimit.TimeOut => log (try0_tag id ^ "timeout")