# HG changeset patch
# User boehmes
# Date 1253021351 -7200
# Node ID 719426c9e1eb656340a73457066aaf663b5f873b
# Parent  076da2bd61f4db3a460063104cf3993c080d2af9
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
separate Perl script to invoke local ATPs and measure their user time, with proper setup of process groups required by E

diff -r 076da2bd61f4 -r 719426c9e1eb src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 15 13:09:13 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 15 15:29:11 2009 +0200
@@ -7,6 +7,7 @@
 
 val proverK = "prover"
 val prover_timeoutK = "prover_timeout"
+val prover_hard_timeoutK = "prover_hard_timeout"
 val keepK = "keep"
 val full_typesK = "full_types"
 val minimizeK = "minimize"
@@ -273,17 +274,22 @@
   SH_FAIL of int * int |
   SH_ERROR
 
-fun run_sh (prover_name, prover) timeout st _ =
+fun run_sh (prover_name, prover) hard_timeout timeout st _ =
   let
     val atp = prover timeout NONE NONE prover_name 1
+    val time_limit =
+      (case hard_timeout of
+        NONE => I
+      | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     val ((success, (message, thm_names), time_atp, _, _, _), time_isa) =
-      Mirabelle.cpu_time atp (Proof.get_goal st)
+      time_limit (Mirabelle.cpu_time atp) (Proof.get_goal st)
   in
     if success then (message, SH_OK (time_isa, time_atp, thm_names))
     else (message, SH_FAIL(time_isa, time_atp))
   end
   handle ResHolClause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
        | ERROR msg => ("error: " ^ msg, SH_ERROR)
+       | TimeLimit.TimeOut => ("timeout", SH_ERROR)
 
 fun thms_of_name ctxt name =
   let
@@ -306,7 +312,10 @@
     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
+    val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
+      |> Option.map (fst o read_int o explode)
+    val (msg, result) = safe init_sh done_sh
+      (run_sh atp hard_timeout timeout st) dir
   in
     case result of
       SH_OK (time_isa, time_atp, names) =>
diff -r 076da2bd61f4 -r 719426c9e1eb src/HOL/Mirabelle/doc/options.txt
--- a/src/HOL/Mirabelle/doc/options.txt	Tue Sep 15 13:09:13 2009 +0200
+++ b/src/HOL/Mirabelle/doc/options.txt	Tue Sep 15 15:29:11 2009 +0200
@@ -1,9 +1,11 @@
 Options for sledgehammer:
 
   * prover=NAME: name of the external prover to call
-  * prover_timeout=TIME: timeout for invoked ATP
+  * prover_timeout=TIME: timeout for invoked ATP (seconds of process time)
+  * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed time)
   * 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=TIME: timeout for each minimization step
+  * minimize_timeout=TIME: timeout for each minimization step (seconds of
+    process time)
   * metis: apply metis with the theorems found by sledgehammer
diff -r 076da2bd61f4 -r 719426c9e1eb src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Sep 15 13:09:13 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Sep 15 15:29:11 2009 +0200
@@ -79,14 +79,14 @@
       preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
 
     (* write out problem file and call prover *)
-    fun cmd_line probfile = "TIMEFORMAT='%3U'; ((time " ^ space_implode " "
-      [File.shell_path cmd, args, File.platform_path probfile] ^ ") 2>&1)"
+    val perl_script = "perl -w $ISABELLE_ATP_MANAGER/lib/scripts/local_atp.pl"
+    fun cmd_line probfile = perl_script ^ " '" ^ space_implode " "
+      [File.shell_path cmd, args, File.platform_path probfile] ^ "'"
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n")
         val (proof, t) = s |> split |> split_last |> apfst cat_lines
-        val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
-        val time = num --| Scan.$$ "." -- num >> (fn (a, b) => a * 1000 + b)
+        val time = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode
       in (proof, as_time t) end
     fun run_on probfile =
diff -r 076da2bd61f4 -r 719426c9e1eb src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl	Tue Sep 15 15:29:11 2009 +0200
@@ -0,0 +1,15 @@
+use POSIX qw(setsid);
+
+$SIG{'INT'} = "DEFAULT";
+
+defined (my $pid = fork) or die "$!";
+if (not $pid) {
+  POSIX::setsid or die $!;
+  exec @ARGV;
+}
+else {
+  wait;
+  my ($user, $system, $cuser, $csystem) = times;
+  my $time = ($user + $cuser) * 1000;
+  print "$time\n";
+}