# HG changeset patch # User blanchet # Date 1284468473 -7200 # Node ID 1c4e38d635e18103735ad0bbe5c112a54f19634b # Parent ee65900bfced7c26dbaecee5d00a5121cced72b1 added a timeout around "try" call in Mirabelle diff -r ee65900bfced -r 1c4e38d635e1 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 14 14:22:49 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 14 14:47:53 2010 +0200 @@ -492,7 +492,8 @@ |> snd end -val try_timeout = Time.fromSeconds 30 +val try_inner_timeout = Time.fromSeconds 5 +val try_outer_timeout = Time.fromSeconds 30 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) = let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in @@ -503,9 +504,9 @@ Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) val minimize = AList.defined (op =) args minimizeK val metis_ft = AList.defined (op =) args metis_ftK - - val trivial = Try.invoke_try (SOME try_timeout) pre - + val trivial = TimeLimit.timeLimit try_outer_timeout + (Try.invoke_try (SOME try_inner_timeout)) pre + handle TimeLimit.TimeOut => false fun apply_metis m1 m2 = if metis_ft then