# HG changeset patch
# User boehmes
# Date 1252396653 -7200
# Node ID cea1716eb1061c0ec5117b5790ebd55327a168be
# Parent  f97a1e5c9a5a06ee11b52b2d038c8c28f4a0a7c7
timeout option for ATPs

diff -r f97a1e5c9a5a -r cea1716eb106 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 07 22:13:32 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 08 09:57:33 2009 +0200
@@ -6,6 +6,7 @@
 struct
 
 val proverK = "prover"
+val prover_timeoutK = "prover_timeout"
 val keepK = "keep"
 val metisK = "metis"
 val full_typesK = "full_types"
@@ -179,7 +180,7 @@
 
 fun run_sh (prover_name, prover) timeout st _ =
   let
-    val atp = prover (Time.toSeconds timeout) NONE NONE prover_name 1
+    val atp = prover timeout NONE NONE prover_name 1
     val ((success, (message, thm_names), time_atp, _, _, _), time_isa) =
       Mirabelle.cpu_time atp (Proof.get_goal st)
   in
@@ -204,11 +205,12 @@
 
 in
 
-fun run_sledgehammer args named_thms id {pre=st, timeout, log, ...} =
+fun run_sledgehammer args named_thms id {pre=st, log, ...} =
   let
     val _ = change_data id inc_sh_calls
     val atp as (prover_name, _) = get_atp (Proof.theory_of st) args
     val dir = AList.lookup (op =) args keepK
+    val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
     val (msg, result) = safe init_sh done_sh (run_sh atp timeout st) dir
   in
     case result of
diff -r f97a1e5c9a5a -r cea1716eb106 src/HOL/Mirabelle/doc/options.txt
--- a/src/HOL/Mirabelle/doc/options.txt	Mon Sep 07 22:13:32 2009 +0200
+++ b/src/HOL/Mirabelle/doc/options.txt	Tue Sep 08 09:57:33 2009 +0200
@@ -1,8 +1,9 @@
 Options for sledgehammer:
 
   * prover=NAME: name of the external prover to call
+  * prover_timeout=TIME: timeout for invoked ATP
   * keep=PATH: path where to keep temporary files created by sledgehammer 
   * full_types: enable full-typed encoding
   * minimize: enable minimization of theorem set found by sledgehammer
-  * minimize_timeout: timeout for each minimization step
+  * minimize_timeout=TIME: timeout for each minimization step
   * metis: apply metis with the theorems found by sledgehammer