# 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"; +}