1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Sep 02 16:29:50 2009 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Sep 02 21:31:58 2009 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4    val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
     1.5    val get_setting : (string * string) list -> string * string -> string
     1.6    val get_int_setting : (string * string) list -> string * int -> int
     1.7 +  val cpu_time : ('a -> 'b) -> 'a -> 'b * int
     1.8  end
     1.9  
    1.10  
    1.11 @@ -67,23 +68,22 @@
    1.12    (* FIXME: with multithreading and parallel proofs enabled, we might need to
    1.13       encapsulate this inside a critical section *)
    1.14  
    1.15 -fun log_block thy msg = log thy (msg ^ "\n------------------")
    1.16 -fun log_action thy name msg = log_block thy (name ^ ": " ^ msg)
    1.17 +fun log_sep thy = log thy "------------------"
    1.18  
    1.19 -fun capture_exns logf f x =
    1.20 -  let
    1.21 -    fun f' x = f x
    1.22 -      handle TimeLimit.TimeOut => logf "time out"
    1.23 -           | ERROR msg => logf ("error: " ^ msg)
    1.24 -  in (case try f' x of NONE => logf "exception" | _ => ()) end
    1.25 +fun try_with f NONE = SOME ()
    1.26 +  | try_with f (SOME e) = (f e; try (fn () => reraise e) ())
    1.27 +
    1.28 +fun capture_exns thy name f x =
    1.29 +  (case try_with I (Exn.get_exn (Exn.capture f x)) of
    1.30 +    NONE => (log thy ("Unhandled exception in " ^ quote name); log_sep thy)
    1.31 +  | SOME _ => log_sep thy)
    1.32  
    1.33  fun apply_actions thy info (pre, post, time) actions =
    1.34    let
    1.35 -    val _ = log_block thy info
    1.36      fun apply (name, action) =
    1.37 -      let val st = {pre=pre, post=post, timeout=time, log=log_action thy name}
    1.38 -      in capture_exns (log_action thy name) action st end
    1.39 -  in List.app apply actions end
    1.40 +      {pre=pre, post=post, timeout=time, log=log thy}
    1.41 +      |> capture_exns thy name action
    1.42 +  in (log thy info; log_sep thy; List.app apply actions) end
    1.43  
    1.44  fun in_range _ _ NONE = true
    1.45    | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
    1.46 @@ -182,4 +182,11 @@
    1.47    | SOME NONE => error ("bad option: " ^ key)
    1.48    | NONE => default)
    1.49  
    1.50 +fun cpu_time f x =
    1.51 +  let
    1.52 +    val start = start_timing ()
    1.53 +    val result = Exn.capture (fn () => f x) ()
    1.54 +    val time = Time.toMilliseconds (#cpu (end_timing start))
    1.55 +  in (Exn.release result, time) end
    1.56 +
    1.57  end

     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Wed Sep 02 16:29:50 2009 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Wed Sep 02 21:31:58 2009 +0200
     2.3 @@ -7,8 +7,9 @@
     2.4  
     2.5  fun arith_action {pre, timeout, log, ...} =
     2.6    if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
     2.7 -  then log "succeeded"
     2.8 +  then log "arith: succeeded"
     2.9    else ()
    2.10 +  handle TimeLimit.TimeOut => log "arith: time out"
    2.11  
    2.12  fun invoke _ = Mirabelle.register ("arith", arith_action)
    2.13  

     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Wed Sep 02 16:29:50 2009 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Wed Sep 02 21:31:58 2009 +0200
     3.3 @@ -16,9 +16,11 @@
     3.4      fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
     3.5    in
     3.6      (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
     3.7 +    |> prefix "metis: "
     3.8      |> add_info
     3.9      |> log
    3.10    end
    3.11 +  handle TimeLimit.TimeOut => log "metis: time out"
    3.12  
    3.13  fun invoke _ = Mirabelle.register ("metis", metis_action)
    3.14  

     4.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Wed Sep 02 16:29:50 2009 +0200
     4.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Wed Sep 02 21:31:58 2009 +0200
     4.3 @@ -11,9 +11,10 @@
     4.4      val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
     4.5    in
     4.6      (case TimeLimit.timeLimit timeout quickcheck pre of
     4.7 -      NONE => log "no counterexample"
     4.8 -    | SOME _ => log "counterexample found")
     4.9 +      NONE => log "quickcheck: no counterexample"
    4.10 +    | SOME _ => log "quickcheck: counterexample found")
    4.11    end
    4.12 +  handle TimeLimit.TimeOut => log "quickcheck: time out"
    4.13  
    4.14  fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
    4.15  

     5.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 02 16:29:50 2009 +0200
     5.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 02 21:31:58 2009 +0200
     5.3 @@ -25,60 +25,81 @@
     5.4      val _ = done y
     5.5    in Exn.release z end
     5.6  
     5.7 +fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
     5.8 +  | with_time false t = "failed (" ^ string_of_int t ^ ")"
     5.9 +
    5.10  val proverK = "prover"
    5.11  val keepK = "keep"
    5.12  val metisK = "metis"
    5.13  
    5.14 -fun sledgehammer_action args {pre=st, timeout, log, ...} =
    5.15 +
    5.16 +local
    5.17 +
    5.18 +fun init NONE = !AtpWrapper.destdir
    5.19 +  | init (SOME path) =
    5.20 +      let
    5.21 +        (* Warning: we implicitly assume single-threaded execution here! *)
    5.22 +        val old = !AtpWrapper.destdir
    5.23 +        val _ = AtpWrapper.destdir := path
    5.24 +      in old end
    5.25 +
    5.26 +fun done path = AtpWrapper.destdir := path
    5.27 +
    5.28 +fun run prover_name timeout st _ =
    5.29 +  let
    5.30 +    val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st))
    5.31 +    val atp_timeout = AtpManager.get_timeout () 
    5.32 +    val atp = prover atp_timeout NONE NONE prover_name 1
    5.33 +    val (success, (message, thm_names), _, _, _) =
    5.34 +      TimeLimit.timeLimit timeout atp (Proof.get_goal st)
    5.35 +  in (success, message, SOME thm_names) end
    5.36 +  handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
    5.37 +       | TimeLimit.TimeOut => (false, "time out", NONE)
    5.38 +       | ERROR msg => (false, "error: " ^ msg, NONE)
    5.39 +
    5.40 +in
    5.41 +
    5.42 +fun run_sledgehammer (args, st, timeout, log) =
    5.43    let
    5.44      val prover_name =
    5.45        AList.lookup (op =) args proverK
    5.46        |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
    5.47 +    val dir = AList.lookup (op =) args keepK
    5.48 +    val ((success, msg, thm_names), time) =
    5.49 +      safe init done (Mirabelle.cpu_time (run prover_name timeout st)) dir
    5.50 +    fun sh_log s = log ("sledgehammer: " ^ with_time success time ^ " [" ^
    5.51 +      prover_name ^ "]" ^ s)
    5.52 +    val _ = if success then sh_log (":\n" ^ msg) else sh_log ""
    5.53 +  in if success then thm_names else NONE end
    5.54  
    5.55 -    val thy = Proof.theory_of st
    5.56 - 
    5.57 -    val prover = the (AtpManager.get_prover prover_name thy)
    5.58 -    val atp_timeout = AtpManager.get_timeout () 
    5.59 +end
    5.60  
    5.61 -    (* run sledgehammer *)
    5.62 -    fun init NONE = !AtpWrapper.destdir
    5.63 -      | init (SOME path) =
    5.64 -          let
    5.65 -            (* Warning: we implicitly assume single-threaded execution here! *)
    5.66 -            val old = !AtpWrapper.destdir
    5.67 -            val _ = AtpWrapper.destdir := path
    5.68 -          in old end
    5.69 -    fun done path = AtpWrapper.destdir := path
    5.70 -    fun sh _ =
    5.71 -      let
    5.72 -        val atp = prover atp_timeout NONE NONE prover_name 1
    5.73 -        val (success, (message, thm_names), _, _, _) =
    5.74 -          TimeLimit.timeLimit timeout atp (Proof.get_goal st)
    5.75 -      in (success, message, SOME thm_names) end
    5.76 -      handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
    5.77 -    val (success, message, thm_names) = safe init done sh
    5.78 -      (AList.lookup (op =) args keepK)
    5.79 -    val _ =
    5.80 -      if success then log (quote prover_name ^ " succeeded:\n" ^ message)
    5.81 -      else log (prover_name ^ " failed")
    5.82  
    5.83 -    (* try metis *)
    5.84 +fun run_metis (args, st, timeout, log) thm_names =
    5.85 +  let
    5.86      fun get_thms ctxt = maps (thms_of_name ctxt)
    5.87      fun metis thms ctxt = MetisTools.metis_tac ctxt thms
    5.88 -    fun log_metis s =
    5.89 -      log ("applying metis: " ^ s)
    5.90 -    fun apply_metis thms =
    5.91 -      if Mirabelle.can_apply timeout (metis thms) st
    5.92 -      then "succeeded" else "failed"
    5.93 -    val _ =
    5.94 -      if not (AList.defined (op =) args metisK) then ()
    5.95 -      else
    5.96 -        these thm_names
    5.97 -        |> get_thms (Proof.context_of st)
    5.98 -        |> apply_metis
    5.99 -        |> log_metis
   5.100 -  in () end
   5.101 +    fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
   5.102 +    fun timed_metis thms =
   5.103 +      uncurry with_time (Mirabelle.cpu_time apply_metis thms)
   5.104 +      handle TimeLimit.TimeOut => "time out"
   5.105 +    fun log_metis s = log ("-----\nmetis (sledgehammer): " ^ s)
   5.106 +  in
   5.107 +    if not (AList.defined (op =) args metisK) then ()
   5.108 +    else if is_none thm_names then ()
   5.109 +    else
   5.110 +      these thm_names
   5.111 +      |> get_thms (Proof.context_of st)
   5.112 +      |> timed_metis
   5.113 +      |> log_metis
   5.114 +  end
   5.115 +
   5.116 +
   5.117 +fun sledgehammer_action args {pre, timeout, log, ...} =
   5.118 +  run_sledgehammer (args, pre, timeout, log)
   5.119 +  |> run_metis (args, pre, timeout, log)
   5.120  
   5.121  fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)
   5.122  
   5.123  end
   5.124 +

     6.1 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Sep 02 16:29:50 2009 +0200
     6.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Sep 02 21:31:58 2009 +0200
     6.3 @@ -122,14 +122,20 @@
     6.4  }
     6.5  close(LOG_FILE);
     6.6  
     6.7 -my $r = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
     6.8 +my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
     6.9    "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
    6.10  
    6.11  
    6.12 +# produce report
    6.13 +
    6.14 +if ($result == 0) {
    6.15 +  system "perl -w \"$mirabelle_home/lib/scripts/report.pl\" \"$log_file\"";
    6.16 +}
    6.17 +
    6.18 +
    6.19  # cleanup
    6.20  
    6.21  unlink $root_file;
    6.22  unlink $setup_file;
    6.23  
    6.24 -exit $r;
    6.25 -
    6.26 +exit $result;