# 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 =>