# HG changeset patch
# User desharna
# Date 1614849044 -3600
# Node ID 316e121476985087cd5f68323867d04c8ee88ad8
# Parent  78aa7846e91fe11fd90c7990112922d9e44d3ffb
tuned exec field in atp_config

diff -r 78aa7846e91f -r 316e12147698 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu Mar 04 10:10:44 2021 +0100
@@ -56,7 +56,6 @@
     val _ = problem
       |> lines_of_atp_problem format ord (K [])
       |> File.write_list prob_file
-    val exec = exec false
     val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
     val command =
       File.bash_path (Path.explode path) ^ " " ^
diff -r 78aa7846e91f -r 316e12147698 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Mar 04 10:10:44 2021 +0100
@@ -14,7 +14,7 @@
 
   type slice_spec = (int * string) * atp_format * string * string * bool
   type atp_config =
-    {exec : bool -> string list * string list,
+    {exec : string list * string list,
      arguments : Proof.context -> bool -> string -> Time.time -> string ->
        term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
      proof_delims : (string * string) list,
@@ -73,7 +73,7 @@
 type slice_spec = (int * string) * atp_format * string * string * bool
 
 type atp_config =
-  {exec : bool -> string list * string list,
+  {exec : string list * string list,
    arguments : Proof.context -> bool -> string -> Time.time -> string ->
      term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
    proof_delims : (string * string) list,
@@ -165,7 +165,7 @@
 (* agsyHOL *)
 
 val agsyhol_config : atp_config =
-  {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
+  {exec = (["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,
    proof_delims = tstp_proof_delims,
@@ -183,7 +183,7 @@
 (* Alt-Ergo *)
 
 val alt_ergo_config : atp_config =
-  {exec = K (["WHY3_HOME"], ["why3"]),
+  {exec = (["WHY3_HOME"], ["why3"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
      "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^
      " " ^ file_name,
@@ -272,7 +272,7 @@
     end
 
 val e_config : atp_config =
-  {exec = fn _ => (["E_HOME"], ["eprover"]),
+  {exec = (["E_HOME"], ["eprover"]),
    arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn file_name =>
      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
        "--auto-schedule --tstp-in --tstp-out --silent " ^
@@ -320,7 +320,7 @@
 (* iProver *)
 
 val iprover_config : atp_config =
-  {exec = K (["IPROVER_HOME"], ["iproveropt", "iprover"]),
+  {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
      "--clausifier \"$E_HOME\"/eprover " ^
      "--clausifier_options \"--tstp-format --silent --cnf\" " ^
@@ -342,7 +342,7 @@
 (* LEO-II *)
 
 val leo2_config : atp_config =
-  {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
+  {exec = (["LEO2_HOME"], ["leo.opt", "leo"]),
    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
      "--foatp e --atp e=\"$E_HOME\"/eprover \
      \--atp epclextract=\"$E_HOME\"/epclextract \
@@ -368,7 +368,7 @@
 
 (* Include choice? Disabled now since it's disabled for Satallax as well. *)
 val leo3_config : atp_config =
-  {exec = K (["LEO3_HOME"], ["leo3"]),
+  {exec = (["LEO3_HOME"], ["leo3"]),
    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
      file_name ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \
      \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
@@ -389,7 +389,7 @@
 
 (* Choice is disabled until there is proper reconstruction for it. *)
 val satallax_config : atp_config =
-  {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
+  {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
      (case getenv "E_HOME" of
        "" => ""
@@ -418,7 +418,7 @@
 val spass_H2SOS = "-Heuristic=2 -SOS"
 
 val spass_config : atp_config =
-  {exec = K (["SPASS_HOME"], ["SPASS"]),
+  {exec = (["SPASS_HOME"], ["SPASS"]),
    arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ =>
      "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
      "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
@@ -486,7 +486,7 @@
   "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"
 
 val vampire_config : atp_config =
-  {exec = K (["VAMPIRE_HOME"], ["vampire"]),
+  {exec = (["VAMPIRE_HOME"], ["vampire"]),
    arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ =>
      (check_vampire_noncommercial ();
       vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
@@ -519,7 +519,7 @@
 (* Z3 with TPTP syntax (half experimental, half legacy) *)
 
 val z3_tptp_config : atp_config =
-  {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
+  {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
      "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
    proof_delims = [("SZS status Theorem", "")],
@@ -544,7 +544,7 @@
 val zipperposition_cdots = "--mode ho-competitive --boolean-reasoning cases-simpl --ext-rules ext-family --ext-rules-max-depth 1 --ho-prim-enum pragmatic --ho-prim-max 1 --bool-subterm-selection A --avatar off --recognize-injectivity true --ho-elim-leibniz 1 --ho-unif-level full-framework --no-max-vars -q '6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)' -q '6|const|conjecture-relative-var(1.02,l,f)' -q '1|prefer-processed|fifo' -q '1|prefer-non-goals|conjecture-relative-var(1,l,f)' -q '4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)' --select e-selection7 --ho-choice-inst true --sine 50 --sine-tolerance 2 --sine-depth-max 4 --sine-depth-min 1 --scan-clause-ac true --lambdasup 0 --kbo-weight-fun invfreqrank"
 
 val zipperposition_config : atp_config =
-  {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
+  {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
    arguments = fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ =>
      "--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
      |> extra_options <> "" ? prefix (extra_options ^ " "),
@@ -604,7 +604,7 @@
 val max_remote_secs = 1000   (* give Geoff Sutcliffe's servers a break *)
 
 fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice =
-  {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
+  {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
    arguments = fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
      (if command <> "" then "-c " ^ quote command ^ " " else "") ^
      "-s " ^ the_remote_system system_name system_versions ^ " " ^
@@ -666,7 +666,7 @@
 (* Dummy prover *)
 
 fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
-  {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
+  {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
    arguments = K (K (K (K (K (K ""))))),
    proof_delims = [],
    known_failures = known_szs_status_failures,
@@ -698,7 +698,7 @@
 
 fun is_atp_installed thy name =
   let val {exec, ...} = get_atp thy name () in
-    exists (fn var => getenv var <> "") (fst (exec false))
+    exists (fn var => getenv var <> "") (fst exec)
   end
 
 fun refresh_systems_on_tptp () =
diff -r 78aa7846e91f -r 316e12147698 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Mar 04 10:10:44 2021 +0100
@@ -158,7 +158,6 @@
         Path.explode dest_dir + problem_file_name
       else
         error ("No such directory: " ^ quote dest_dir)
-    val exec = exec full_proofs
     val command0 =
       (case find_first (fn var => getenv var <> "") (fst exec) of
         SOME var =>