# HG changeset patch
# User blanchet
# Date 1375104631 -7200
# Node ID d9d90d29860e410fd9d73c4f954c719764aad8cf
# Parent  1165f78c16d8f07a4a7995155ea9d6ef2ddc75a2
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")

diff -r 1165f78c16d8 -r d9d90d29860e src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Sun Jul 28 20:51:15 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 29 15:30:31 2013 +0200
@@ -55,6 +55,7 @@
     val ord = effective_term_order ctxt atp
     val _ = problem |> lines_of_atp_problem format ord (K [])
                     |> File.write_list prob_file
+    val exec = exec ()
     val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
     val command =
       File.shell_path (Path.explode path) ^ " " ^
diff -r 1165f78c16d8 -r d9d90d29860e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun Jul 28 20:51:15 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jul 29 15:30:31 2013 +0200
@@ -14,7 +14,7 @@
 
   type slice_spec = (int * string) * atp_format * string * string * bool
   type atp_config =
-    {exec : string list * string list,
+    {exec : unit -> string list * string list,
      arguments :
        Proof.context -> bool -> string -> Time.time -> string
        -> term_order * (unit -> (string * int) list)
@@ -96,7 +96,7 @@
 type slice_spec = (int * string) * atp_format * string * string * bool
 
 type atp_config =
-  {exec : string list * string list,
+  {exec : unit -> string list * string list,
    arguments :
      Proof.context -> bool -> string -> Time.time -> string
      -> term_order * (unit -> (string * int) list)
@@ -215,7 +215,7 @@
   THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs)
 
 val agsyhol_config : atp_config =
-  {exec = (["AGSYHOL_HOME"], ["agsyHOL"]),
+  {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^
        file_name,
@@ -236,7 +236,7 @@
 val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
 
 val alt_ergo_config : atp_config =
-  {exec = (["WHY3_HOME"], ["why3"]),
+  {exec = K (["WHY3_HOME"], ["why3"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "--format tptp --prover 'Alt-Ergo,0.95,' --timelimit " ^
        string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
@@ -259,6 +259,7 @@
 
 fun is_e_at_least_1_3 () = string_ord (getenv "E_VERSION", "1.3") <> LESS
 fun is_e_at_least_1_6 () = string_ord (getenv "E_VERSION", "1.6") <> LESS
+fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
 
 val e_smartN = "smart"
 val e_autoN = "auto"
@@ -330,12 +331,6 @@
        else "")
     end
 
-fun e_shell_level_argument full_proof =
-  if is_e_at_least_1_6 () then
-    " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
-  else
-    ""
-
 fun effective_e_selection_heuristic ctxt =
   if is_e_at_least_1_3 () then Config.get ctxt e_selection_heuristic
   else e_autoN
@@ -343,16 +338,25 @@
 fun e_kbo () = if is_e_at_least_1_3 () then "KBO6" else "KBO"
 
 val e_config : atp_config =
-  {exec = (["E_HOME"], ["eproof_ram", "eproof"]),
+  {exec = (fn () => (["E_HOME"],
+       if is_e_at_least_1_8 () then ["eprover"] else ["eproof_ram", "eproof"])),
    arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout =>
        fn file_name =>
        fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
-       "--tstp-in --tstp-out --output-level=5 --silent " ^
+       "--tstp-in --tstp-out --silent " ^
        e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
        e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
        "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
-       e_shell_level_argument full_proof ^ " " ^ file_name,
+       (if is_e_at_least_1_8 () then
+          " --proof-object=1"
+        else
+          " --output-level=5" ^
+          (if is_e_at_least_1_6 () then
+             " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
+           else
+             "")) ^
+       " " ^ file_name,
    proof_delims =
      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
      tstp_proof_delims,
@@ -383,7 +387,7 @@
 (* E-MaLeS *)
 
 val e_males_config : atp_config =
-  {exec = (["E_MALES_HOME"], ["emales.py"]),
+  {exec = K (["E_MALES_HOME"], ["emales.py"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name,
    proof_delims = tstp_proof_delims,
@@ -404,7 +408,7 @@
 (* E-Par *)
 
 val e_par_config : atp_config =
-  {exec = (["E_HOME"], ["runepar.pl"]),
+  {exec = K (["E_HOME"], ["runepar.pl"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^
        " 2" (* proofs *),
@@ -421,7 +425,7 @@
 (* iProver *)
 
 val iprover_config : atp_config =
-  {exec = (["IPROVER_HOME"], ["iprover"]),
+  {exec = K (["IPROVER_HOME"], ["iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^
        string_of_real (Time.toReal timeout) ^ " " ^ file_name,
@@ -442,7 +446,7 @@
 (* iProver-Eq *)
 
 val iprover_eq_config : atp_config =
-  {exec = (["IPROVER_EQ_HOME"], ["iprover-eq"]),
+  {exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]),
    arguments = #arguments iprover_config,
    proof_delims = #proof_delims iprover_config,
    known_failures = #known_failures iprover_config,
@@ -462,7 +466,7 @@
   THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
 
 val leo2_config : atp_config =
-  {exec = (["LEO2_HOME"], ["leo.opt", "leo"]),
+  {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "--foatp e --atp e=\"$E_HOME\"/eprover \
        \--atp epclextract=\"$E_HOME\"/epclextract \
@@ -490,7 +494,7 @@
   THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs)
 
 val satallax_config : atp_config =
-  {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
+  {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
    proof_delims =
@@ -520,7 +524,7 @@
 
 (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
 val spass_config : atp_config =
-  {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
+  {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
    arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
        fn file_name => fn _ =>
        "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
@@ -567,7 +571,7 @@
 val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
 
 val vampire_config : atp_config =
-  {exec = (["VAMPIRE_HOME"], ["vampire"]),
+  {exec = K (["VAMPIRE_HOME"], ["vampire"]),
    arguments = fn _ => fn full_proof => fn sos => fn timeout => fn file_name =>
        fn _ =>
        "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
@@ -619,7 +623,7 @@
 val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
 
 val z3_tptp_config : atp_config =
-  {exec = (["Z3_HOME"], ["z3"]),
+  {exec = K (["Z3_HOME"], ["z3"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
        string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
@@ -641,7 +645,7 @@
 (* Not really a prover: Experimental Polymorphic THF and DFG output *)
 
 fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
-  {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
+  {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
    arguments = K (K (K (K (K (K ""))))),
    proof_delims = [],
    known_failures = known_szs_status_failures,
@@ -710,7 +714,7 @@
 
 fun remote_config system_name system_versions proof_delims known_failures
                   prem_role best_slice : atp_config =
-  {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
+  {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
    arguments = fn _ => fn _ => fn command => fn timeout => fn file_name =>
        fn _ =>
        (if command <> "" then "-c " ^ quote command ^ " " else "") ^
@@ -796,7 +800,7 @@
 
 fun is_atp_installed thy name =
   let val {exec, ...} = get_atp thy name () in
-    exists (fn var => getenv var <> "") (fst exec)
+    exists (fn var => getenv var <> "") (fst (exec ()))
   end
 
 fun refresh_systems_on_tptp () =
diff -r 1165f78c16d8 -r d9d90d29860e src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 28 20:51:15 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jul 29 15:30:31 2013 +0200
@@ -712,6 +712,7 @@
         Path.append (Path.explode dest_dir) problem_file_name
       else
         error ("No such directory: " ^ quote dest_dir ^ ".")
+    val exec = exec ()
     val command0 =
       case find_first (fn var => getenv var <> "") (fst exec) of
         SOME var =>
@@ -769,7 +770,8 @@
                     |> op @
                     |> cons (0, subgoal_th)
           in
-            Legacy_Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl
+            Legacy_Monomorph.monomorph atp_schematic_consts_of rths ctxt
+            |> fst |> tl
             |> curry ListPair.zip (map fst facts)
             |> maps (fn (name, rths) =>
                         map (pair name o zero_var_indexes o snd) rths)
@@ -962,8 +964,8 @@
                   else
                     ()
                 val isar_params =
-                  (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
-                   isar_compress_degree, merge_timeout_slack,
+                  (debug, verbose, preplay_timeout, preplay_trace,
+                   isar_compress, isar_compress_degree, merge_timeout_slack,
                    isar_try0,isar_minimize,
                    pool, fact_names, lifted, sym_tab, atp_proof, goal)
                 val one_line_params =
@@ -973,8 +975,8 @@
                    subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
-                proof_text ctxt (mode = Auto_Try) isar_proofs isar_params num_chained
-                           one_line_params
+                proof_text ctxt (mode = Auto_Try) isar_proofs isar_params
+                           num_chained one_line_params
               end,
            (if verbose then
               "\nATP real CPU time: " ^ string_of_time run_time ^ "."
@@ -1177,7 +1179,9 @@
                                          preplay,
                  subgoal, subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
-            in one_line_proof_text (mode = Auto_Try) num_chained one_line_params end,
+            in
+              one_line_proof_text (mode = Auto_Try) num_chained one_line_params
+            end,
          if verbose then
            "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
          else
@@ -1222,7 +1226,9 @@
                  minimize_command override_params name, subgoal,
                  subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
-            in one_line_proof_text (mode = Auto_Try) num_chained one_line_params end,
+            in
+              one_line_proof_text (mode = Auto_Try) num_chained one_line_params
+            end,
        message_tail = ""}
     | play =>
       let