# HG changeset patch
# User boehmes
# Date 1256662850 -3600
# Node ID ed1681284f624e51afb322217932c858902a84c3
# Parent  66eddea44a67d33c64df04b994335c471edf434e
measure runtime of ATPs only if requested

diff -r 66eddea44a67 -r ed1681284f62 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 27 16:16:12 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 27 18:00:50 2009 +0100
@@ -302,8 +302,11 @@
 fun run_sh prover hard_timeout timeout dir st =
   let
     val (ctxt, goal) = Proof.get_goal st
-    val ctxt' = if is_none dir then ctxt
-      else Config.put ATP_Wrapper.destdir (the dir) ctxt
+    val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
+    val ctxt' =
+      ctxt
+      |> change_dir dir
+      |> Config.put ATP_Wrapper.measure_runtime true
     val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal);
 
     val time_limit =
diff -r 66eddea44a67 -r ed1681284f62 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Oct 27 16:16:12 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Oct 27 18:00:50 2009 +0100
@@ -9,6 +9,7 @@
   (*hooks for problem files*)
   val destdir: string Config.T
   val problem_prefix: string Config.T
+  val measure_runtime: bool Config.T
   val setup: theory -> theory
 
   (*prover configuration, problem format, and prover result*)
@@ -61,7 +62,10 @@
 val (problem_prefix, problem_prefix_setup) =
   Attrib.config_string "atp_problem_prefix" "prob";
 
-val setup = destdir_setup #> problem_prefix_setup;
+val (measure_runtime, measure_runtime_setup) =
+  Attrib.config_bool "atp_measure_runtime" false;
+
+val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup;
 
 
 (* prover configuration, problem format, and prover result *)
@@ -140,9 +144,14 @@
       end;
 
     (* write out problem file and call prover *)
-    fun cmd_line probfile = "TIMEFORMAT='%3U'; { time " ^ space_implode " "
-      [File.shell_path cmd, args, File.shell_path probfile] ^ " 2> /dev/null" ^
-      " ; } 2>&1"
+    fun cmd_line probfile =
+      if Config.get ctxt measure_runtime
+      then (* Warning: suppresses error messages of ATPs *)
+        "TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd,
+        args, File.shell_path probfile] ^ " 2> /dev/null" ^ " ; } 2>&1"
+      else
+        space_implode " " ["exec", File.shell_path cmd, args,
+        File.shell_path probfile];
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n");
@@ -154,10 +163,12 @@
         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
       in (proof, as_time t) end;
+    fun split_time' s =
+      if Config.get ctxt measure_runtime then split_time s else (s, 0)
     fun run_on probfile =
       if File.exists cmd then
         write probfile clauses
-        |> pair (apfst split_time (system_out (cmd_line probfile)))
+        |> pair (apfst split_time' (system_out (cmd_line probfile)))
       else error ("Bad executable: " ^ Path.implode cmd);
 
     (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)