merged
authorhaftmann
Thu Sep 24 19:14:18 2009 +0200 (2009-09-24)
changeset 32682304a47739407
parent 32681 adeac3cbb659
parent 32677 8854e892cf3e
child 32705 04ce6bb14d85
merged
     1.1 --- a/Admin/E/eproof	Thu Sep 24 18:29:29 2009 +0200
     1.2 +++ b/Admin/E/eproof	Thu Sep 24 19:14:18 2009 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  
     1.5  use File::Basename qw/ dirname /;
     1.6  use File::Temp qw/ tempfile /;
     1.7 +use English;
     1.8  
     1.9  
    1.10  # E executables
    1.11 @@ -44,7 +45,7 @@
    1.12  # run E, redirecting output into a temporary file
    1.13  
    1.14  my ($fh, $filename) = tempfile(UNLINK => 1);
    1.15 -my $r = system "$eprover_cmd > $filename";
    1.16 +my $r = system "$eprover_cmd > '$filename'";
    1.17  exit ($r >> 8) if $r != 0;
    1.18  
    1.19  
    1.20 @@ -55,7 +56,7 @@
    1.21    # Note: Like the original eproof, we only look at the last 60 lines.
    1.22  
    1.23  if ($content =~ m/Total time\s*:\s*([0-9]+\.[0-9]+)/) {
    1.24 -  $timelimit = $timelimit - $1 - 1;
    1.25 +  $timelimit = int($timelimit - $1 - 1);
    1.26  
    1.27    if ($content =~ m/No proof found!/) {
    1.28      print "# Problem is satisfiable (or invalid), " .
    1.29 @@ -85,7 +86,7 @@
    1.30    print if (m/# SZS status/ or m/"# Failure"/);
    1.31  }
    1.32  $r = system ("exec bash -c \"ulimit -S -t $timelimit; " .
    1.33 -  "'$epclextract' $format -f --competition-framing $filename\"");
    1.34 +  "'$epclextract' $format -f --competition-framing '$filename'\"");
    1.35    # Note: Setting the user time is not supported on Cygwin, i.e., ulimit fails
    1.36    # and prints and error message. How could we then limit the execution time?
    1.37  exit ($r >> 8);
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 24 18:29:29 2009 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 24 19:14:18 2009 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4    type done_args = {last: Toplevel.state, log: string -> unit}
     2.5    type done_action = int -> done_args -> unit
     2.6    type run_args = {pre: Proof.state, post: Toplevel.state option,
     2.7 -    timeout: Time.time, log: string -> unit, pos: Position.T}
     2.8 +    timeout: Time.time, log: string -> unit, pos: Position.T, name: string}
     2.9    type run_action = int -> run_args -> unit
    2.10    type action = init_action * run_action * done_action
    2.11    val catch : (int -> string) -> run_action -> run_action
    2.12 @@ -56,7 +56,7 @@
    2.13  type done_args = {last: Toplevel.state, log: string -> unit}
    2.14  type done_action = int -> done_args -> unit
    2.15  type run_args = {pre: Proof.state, post: Toplevel.state option,
    2.16 -  timeout: Time.time, log: string -> unit, pos: Position.T}
    2.17 +  timeout: Time.time, log: string -> unit, pos: Position.T, name: string}
    2.18  type run_action = int -> run_args -> unit
    2.19  type action = init_action * run_action * done_action
    2.20  
    2.21 @@ -95,9 +95,9 @@
    2.22  
    2.23  fun log_sep thy = log thy "------------------"
    2.24  
    2.25 -fun apply_actions thy pos info (pre, post, time) actions =
    2.26 +fun apply_actions thy pos name info (pre, post, time) actions =
    2.27    let
    2.28 -    fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos}
    2.29 +    fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name}
    2.30      fun run (id, run, _) = (apply (run id); log_sep thy)
    2.31    in (log thy info; log_sep thy; List.app run actions) end
    2.32  
    2.33 @@ -121,7 +121,7 @@
    2.34      val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
    2.35      val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
    2.36    in
    2.37 -    only_within_range thy pos (apply_actions thy pos info st) (Actions.get thy)
    2.38 +    only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy)
    2.39    end
    2.40  
    2.41  fun done_actions st =
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 24 18:29:29 2009 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 24 19:14:18 2009 +0200
     3.3 @@ -31,6 +31,7 @@
     3.4  datatype me_data = MeData of {
     3.5    calls: int,
     3.6    success: int,
     3.7 +  proofs: int,
     3.8    time: int,
     3.9    timeout: int,
    3.10    lemmas: int,
    3.11 @@ -55,14 +56,14 @@
    3.12  fun make_min_data (succs, ab_ratios, it_ratios) =
    3.13    MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
    3.14  
    3.15 -fun make_me_data (calls, success, time, timeout, lemmas, posns) =
    3.16 -  MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
    3.17 +fun make_me_data (calls, success, proofs, time, timeout, lemmas, posns) =
    3.18 +  MeData{calls=calls, success=success, proofs=proofs, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
    3.19  
    3.20  val empty_data =
    3.21    Data(make_sh_data (0, 0, 0, 0, 0, 0),
    3.22 -       make_me_data(0, 0, 0, 0, 0, []),
    3.23 +       make_me_data(0, 0, 0, 0, 0, 0, []),
    3.24         MinData{succs=0, ab_ratios=0, it_ratios=0},
    3.25 -       make_me_data(0, 0, 0, 0, 0, []))
    3.26 +       make_me_data(0, 0, 0, 0, 0, 0, []))
    3.27  
    3.28  fun map_sh_data f
    3.29    (Data (ShData{calls, success, lemmas, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) =
    3.30 @@ -73,11 +74,11 @@
    3.31    (Data(shda, meda0, MinData{succs,ab_ratios,it_ratios}, meda)) =
    3.32    Data(shda, meda0, make_min_data(f(succs,ab_ratios,it_ratios)), meda)
    3.33  
    3.34 -fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) =
    3.35 -  Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda)
    3.36 +fun map_me_data0 f (Data (shda, MeData{calls,success,proofs,time,timeout,lemmas,posns}, minda, meda)) =
    3.37 +  Data(shda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,posns)), minda, meda)
    3.38  
    3.39 -fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,time,timeout,lemmas,posns})) =
    3.40 -  Data(shda, meda0, minda, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
    3.41 +fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,proofs,time,timeout,lemmas,posns})) =
    3.42 +  Data(shda, meda0, minda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,posns)))
    3.43  
    3.44  val inc_sh_calls =
    3.45    map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
    3.46 @@ -113,52 +114,60 @@
    3.47    map_min_data (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
    3.48  
    3.49  val inc_metis_calls = map_me_data
    3.50 - (fn (calls, success, time, timeout, lemmas,posns)
    3.51 -  => (calls + 1, success, time, timeout, lemmas,posns))
    3.52 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    3.53 +  => (calls + 1, success, proofs, time, timeout, lemmas,posns))
    3.54  
    3.55  val inc_metis_success = map_me_data
    3.56 - (fn (calls,success,time,timeout,lemmas,posns)
    3.57 -  => (calls, success + 1, time, timeout, lemmas,posns))
    3.58 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    3.59 +  => (calls, success + 1, proofs, time, timeout, lemmas,posns))
    3.60 +
    3.61 +val inc_metis_proofs = map_me_data
    3.62 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    3.63 +  => (calls, success, proofs + 1, time, timeout, lemmas,posns))
    3.64  
    3.65  fun inc_metis_time t = map_me_data
    3.66 - (fn (calls,success,time,timeout,lemmas,posns)
    3.67 -  => (calls, success, time + t, timeout, lemmas,posns))
    3.68 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    3.69 +  => (calls, success, proofs, time + t, timeout, lemmas,posns))
    3.70  
    3.71  val inc_metis_timeout = map_me_data
    3.72 - (fn (calls,success,time,timeout,lemmas,posns)
    3.73 -  => (calls, success, time, timeout + 1, lemmas,posns))
    3.74 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    3.75 +  => (calls, success, proofs, time, timeout + 1, lemmas,posns))
    3.76  
    3.77  fun inc_metis_lemmas n = map_me_data
    3.78 - (fn (calls,success,time,timeout,lemmas,posns)
    3.79 -  => (calls, success, time, timeout, lemmas + n, posns))
    3.80 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    3.81 +  => (calls, success, proofs, time, timeout, lemmas + n, posns))
    3.82  
    3.83  fun inc_metis_posns pos = map_me_data
    3.84 - (fn (calls,success,time,timeout,lemmas,posns)
    3.85 -  => (calls, success, time, timeout, lemmas, pos::posns))
    3.86 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    3.87 +  => (calls, success, proofs, time, timeout, lemmas, pos::posns))
    3.88  
    3.89  val inc_metis_calls0 = map_me_data0 
    3.90 -(fn (calls, success, time, timeout, lemmas,posns)
    3.91 -  => (calls + 1, success, time, timeout, lemmas,posns))
    3.92 +(fn (calls,success,proofs,time,timeout,lemmas,posns)
    3.93 +  => (calls + 1, success, proofs, time, timeout, lemmas,posns))
    3.94  
    3.95  val inc_metis_success0 = map_me_data0
    3.96 - (fn (calls,success,time,timeout,lemmas,posns)
    3.97 -  => (calls, success + 1, time, timeout, lemmas,posns))
    3.98 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
    3.99 +  => (calls, success + 1, proofs, time, timeout, lemmas,posns))
   3.100 +
   3.101 +val inc_metis_proofs0 = map_me_data0
   3.102 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
   3.103 +  => (calls, success, proofs + 1, time, timeout, lemmas,posns))
   3.104  
   3.105  fun inc_metis_time0 t = map_me_data0
   3.106 - (fn (calls,success,time,timeout,lemmas,posns)
   3.107 -  => (calls, success, time + t, timeout, lemmas,posns))
   3.108 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
   3.109 +  => (calls, success, proofs, time + t, timeout, lemmas,posns))
   3.110  
   3.111  val inc_metis_timeout0 = map_me_data0
   3.112 - (fn (calls,success,time,timeout,lemmas,posns)
   3.113 -  => (calls, success, time, timeout + 1, lemmas,posns))
   3.114 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
   3.115 +  => (calls, success, proofs, time, timeout + 1, lemmas,posns))
   3.116  
   3.117  fun inc_metis_lemmas0 n = map_me_data0
   3.118 - (fn (calls,success,time,timeout,lemmas,posns)
   3.119 -  => (calls, success, time, timeout, lemmas + n, posns))
   3.120 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
   3.121 +  => (calls, success, proofs, time, timeout, lemmas + n, posns))
   3.122  
   3.123  fun inc_metis_posns0 pos = map_me_data0
   3.124 - (fn (calls,success,time,timeout,lemmas,posns)
   3.125 -  => (calls, success, time, timeout, lemmas, pos::posns))
   3.126 + (fn (calls,success,proofs,time,timeout,lemmas,posns)
   3.127 +  => (calls, success, proofs, time, timeout, lemmas, pos::posns))
   3.128  
   3.129  local
   3.130  
   3.131 @@ -190,10 +199,10 @@
   3.132    let val str0 = string_of_int o the_default 0
   3.133    in str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) end
   3.134  
   3.135 -fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_time
   3.136 +fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_proofs metis_time
   3.137      metis_timeout metis_lemmas metis_posns =
   3.138   (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
   3.139 -  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success);
   3.140 +  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^ " (proof: " ^ str metis_proofs ^ ")");
   3.141    log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
   3.142    log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
   3.143    log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
   3.144 @@ -216,11 +225,11 @@
   3.145  fun log_data id log (Data
   3.146     (ShData{calls=sh_calls, lemmas=sh_lemmas, success=sh_success,
   3.147        time_isa=sh_time_isa,time_atp=sh_time_atp,time_atp_fail=sh_time_atp_fail},
   3.148 -    MeData{calls=metis_calls0,
   3.149 +    MeData{calls=metis_calls0, proofs=metis_proofs0,
   3.150        success=metis_success0, time=metis_time0, timeout=metis_timeout0,
   3.151        lemmas=metis_lemmas0,posns=metis_posns0},
   3.152      MinData{succs=min_succs, ab_ratios=ab_ratios, it_ratios=it_ratios},
   3.153 -    MeData{calls=metis_calls,
   3.154 +    MeData{calls=metis_calls, proofs=metis_proofs,
   3.155        success=metis_success, time=metis_time, timeout=metis_timeout,
   3.156        lemmas=metis_lemmas,posns=metis_posns})) =
   3.157    if sh_calls > 0
   3.158 @@ -229,12 +238,12 @@
   3.159      log_sh_data log sh_calls sh_success sh_lemmas sh_time_isa sh_time_atp sh_time_atp_fail;
   3.160      log "";
   3.161      if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls
   3.162 -      metis_success metis_time metis_timeout metis_lemmas  metis_posns else ();
   3.163 +      metis_success metis_proofs metis_time metis_timeout metis_lemmas  metis_posns else ();
   3.164      log "";
   3.165      if metis_calls0 > 0
   3.166        then (log_min_data log min_succs ab_ratios it_ratios; log "";
   3.167              log_metis_data log "unminimized " sh_calls sh_success metis_calls0
   3.168 -              metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
   3.169 +              metis_success0 metis_proofs0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
   3.170        else ()
   3.171     )
   3.172    else ()
   3.173 @@ -376,8 +385,8 @@
   3.174    end
   3.175  
   3.176  
   3.177 -fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout,
   3.178 -    inc_metis_lemmas, inc_metis_posns) args named_thms id
   3.179 +fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time, inc_metis_timeout,
   3.180 +    inc_metis_lemmas, inc_metis_posns) args name named_thms id
   3.181      ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   3.182    let
   3.183      fun metis thms ctxt = MetisTools.metis_tac ctxt thms
   3.184 @@ -388,6 +397,7 @@
   3.185            change_data id (inc_metis_lemmas (length named_thms));
   3.186            change_data id (inc_metis_time t);
   3.187            change_data id (inc_metis_posns pos);
   3.188 +          if name = "proof" then change_data id inc_metis_proofs else ();
   3.189            "succeeded (" ^ string_of_int t ^ ")")
   3.190      fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
   3.191        handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout")
   3.192 @@ -401,13 +411,13 @@
   3.193      |> log o prefix (metis_tag id) 
   3.194    end
   3.195  
   3.196 -fun sledgehammer_action args id (st as {log, pre, ...}: Mirabelle.run_args) =
   3.197 +fun sledgehammer_action args id (st as {log, pre, name, ...}: Mirabelle.run_args) =
   3.198    if can Logic.dest_conjunction (Thm.major_prem_of(snd(snd(Proof.get_goal pre))))
   3.199    then () else
   3.200    let
   3.201 -    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time,
   3.202 +    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time,
   3.203          inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
   3.204 -    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0,
   3.205 +    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_proofs0, inc_metis_time0,
   3.206          inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
   3.207      val named_thms = ref (NONE : (string * thm list) list option)
   3.208      val minimize = AList.defined (op =) args minimizeK
   3.209 @@ -416,12 +426,12 @@
   3.210      if is_some (!named_thms)
   3.211        then
   3.212         (if minimize
   3.213 -          then Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))) id st
   3.214 +          then Mirabelle.catch metis_tag (run_metis metis0_fns args name (these (!named_thms))) id st
   3.215            else ();
   3.216         if minimize andalso not(null(these(!named_thms)))
   3.217           then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st
   3.218           else ();
   3.219 -       Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st)
   3.220 +       Mirabelle.catch metis_tag (run_metis metis_fns args name (these (!named_thms))) id st)
   3.221      else ()
   3.222    end
   3.223