added a timeout to "try0" in Mirabelle
authorblanchet
Fri May 18 16:43:38 2012 +0200 (2012-05-18)
changeset 4794249b05b9ead33
parent 47941 22e001795641
child 47943 c09326cedb41
added a timeout to "try0" in Mirabelle
src/HOL/IsaMakefile
src/HOL/Mirabelle/Tools/mirabelle_try0.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri May 18 15:08:08 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri May 18 16:43:38 2012 +0200
     1.3 @@ -1334,6 +1334,7 @@
     1.4    Mirabelle/Tools/mirabelle_refute.ML	\
     1.5    Mirabelle/Tools/mirabelle_sledgehammer.ML \
     1.6    Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \
     1.7 +  Mirabelle/Tools/mirabelle_try0.ML \
     1.8    TPTP/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \
     1.9    Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \
    1.10    Library/Inner_Product.thy
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML	Fri May 18 15:08:08 2012 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_try0.ML	Fri May 18 16:43:38 2012 +0200
     2.3 @@ -10,8 +10,10 @@
     2.4  fun init _ = I
     2.5  fun done _ _ = ()
     2.6  
     2.7 -fun run id ({pre, (* timeout, *) log, ...}: Mirabelle.run_args) =
     2.8 -  if Try0.try0 (* (SOME timeout) *) NONE ([], [], [], []) pre
     2.9 +fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time)
    2.10 +
    2.11 +fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
    2.12 +  if TimeLimit.timeLimit (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
    2.13    then log (try0_tag id ^ "succeeded")
    2.14    else ()
    2.15    handle TimeLimit.TimeOut => log (try0_tag id ^ "timeout")