--- 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
--- 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