# HG changeset patch # User blanchet # Date 1648212743 -3600 # Node ID 72cbbb4d98f3ae7deed7d052b1c880edf6b5b8e9 # Parent e1aa703c8cce1aa33150398090d820bfdda4510f cleaned up obsolete E setup and a bit of SPASS diff -r e1aa703c8cce -r 72cbbb4d98f3 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Mar 25 13:52:23 2022 +0100 +++ b/src/HOL/Sledgehammer.thy Fri Mar 25 13:52:23 2022 +0100 @@ -35,7 +35,4 @@ ML_file \Tools/Sledgehammer/sledgehammer_commands.ML\ ML_file \Tools/Sledgehammer/sledgehammer_tactics.ML\ -lemma "2 + 2 = 5" - sledgehammer[verbose, mepo, overlord] - end diff -r e1aa703c8cce -r 72cbbb4d98f3 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Fri Mar 25 13:52:23 2022 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Mar 25 13:52:23 2022 +0100 @@ -128,40 +128,31 @@ val bool_atype : (string * string) atp_type val individual_atype : (string * string) atp_type val mk_anot : ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula - val mk_aconn : - atp_connective -> ('a, 'b, 'c, 'd) atp_formula - -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula + val mk_aconn : atp_connective -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula -> + ('a, 'b, 'c, 'd) atp_formula val mk_app : (string, 'a) atp_term -> (string, 'a) atp_term -> (string, 'a) atp_term val mk_apps : (string, 'a) atp_term -> (string, 'a) atp_term list -> (string, 'a) atp_term val mk_simple_aterm: 'a -> ('a, 'b) atp_term - val aconn_fold : - bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list - -> 'b -> 'b - val aconn_map : - bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) atp_formula) - -> atp_connective * 'a list -> ('b, 'c, 'd, 'e) atp_formula - val formula_fold : - bool option -> (bool option -> 'c -> 'e -> 'e) - -> ('a, 'b, 'c, 'd) atp_formula -> 'e -> 'e - val formula_map : - ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula + val aconn_fold : bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list -> + 'b -> 'b + val aconn_map : bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) atp_formula) -> + atp_connective * 'a list -> ('b, 'c, 'd, 'e) atp_formula + val formula_fold : bool option -> (bool option -> 'c -> 'e -> 'e) -> + ('a, 'b, 'c, 'd) atp_formula -> 'e -> 'e + val formula_map : ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type) val is_format_higher_order : atp_format -> bool val tptp_string_of_format : atp_format -> string val tptp_string_of_role : atp_formula_role -> string val tptp_string_of_line : atp_format -> string atp_problem_line -> string - val lines_of_atp_problem : - atp_format -> term_order -> (unit -> (string * int) list) - -> string atp_problem -> string list - val ensure_cnf_problem : - (string * string) atp_problem -> (string * string) atp_problem - val filter_cnf_ueq_problem : - (string * string) atp_problem -> (string * string) atp_problem + val lines_of_atp_problem : atp_format -> (unit -> (string * int) list) -> string atp_problem -> + string list + val ensure_cnf_problem : (string * string) atp_problem -> (string * string) atp_problem + val filter_cnf_ueq_problem : (string * string) atp_problem -> (string * string) atp_problem val declared_in_atp_problem : 'a atp_problem -> ('a list * 'a list) * 'a list - val nice_atp_problem : - bool -> atp_format -> ('a * (string * string) atp_problem_line list) list - -> ('a * string atp_problem_line list) list - * (string Symtab.table * string Symtab.table) option + val nice_atp_problem : bool -> atp_format -> + ('a * (string * string) atp_problem_line list) list -> + ('a * string atp_problem_line list) list * (string Symtab.table * string Symtab.table) option end; structure ATP_Problem : ATP_PROBLEM = @@ -693,8 +684,14 @@ fun maybe_enclose bef aft "" = "% " ^ bef ^ aft | maybe_enclose bef aft s = bef ^ s ^ aft -fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem = +fun dfg_lines poly ord_info problem = let + (* hardcoded settings *) + val is_lpo = false + val gen_weights = true + val gen_prec = true + val gen_simp = false + val typ = string_of_type (DFG poly) val term = dfg_string_of_term fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")" @@ -801,11 +798,11 @@ ["end_problem.\n"] end -fun lines_of_atp_problem format ord ord_info problem = +fun lines_of_atp_problem format ord_info problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: (case format of - DFG poly => dfg_lines poly ord ord_info + DFG poly => dfg_lines poly ord_info | _ => tptp_lines format) problem diff -r e1aa703c8cce -r 72cbbb4d98f3 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Mar 25 13:52:23 2022 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Mar 25 13:52:23 2022 +0100 @@ -117,7 +117,6 @@ mode -> string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list -> string atp_problem * string Symtab.table * (string * term) list * int Symtab.table - val atp_problem_selection_weights : string atp_problem -> (string * real) list val atp_problem_term_order_info : string atp_problem -> (string * int) list end; @@ -2923,42 +2922,6 @@ val fact_max_weight = 1.0 val type_info_default_weight = 0.8 -(* Weights are from 0.0 (most important) to 1.0 (least important). *) -fun atp_problem_selection_weights problem = - let - fun add_term_weights weight (ATerm ((s, _), tms)) = - is_tptp_user_symbol s ? Symtab.default (s, weight) #> fold (add_term_weights weight) tms - | add_term_weights weight (AAbs ((_, tm), args)) = - add_term_weights weight tm #> fold (add_term_weights weight) args - fun add_line_weights weight (Formula (_, _, phi, _, _)) = - formula_fold NONE (K (add_term_weights weight)) phi - | add_line_weights _ _ = I - fun add_conjectures_weights [] = I - | add_conjectures_weights conjs = - let val (hyps, conj) = split_last conjs in - add_line_weights conj_weight conj - #> fold (add_line_weights hyp_weight) hyps - end - fun add_facts_weights facts = - let - val num_facts = length facts - fun weight_of j = - fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j - / Real.fromInt num_facts - in - fold_index (fn (i, fact) => add_line_weights (weight_of i) fact) facts - end - val get = these o AList.lookup (op =) problem - in - Symtab.empty - |> add_conjectures_weights (get free_typesN @ get conjsN) - |> add_facts_weights (get factsN) - |> fold (fold (add_line_weights type_info_default_weight) o get) - [explicit_declsN, subclassesN, tconsN] - |> Symtab.dest - |> sort (prod_ord Real.compare string_ord o apply2 swap) - end - (* Ugly hack: may make innocent victims (collateral damage) *) fun may_be_app s args = String.isPrefix app_op_name s andalso length args = 2 fun may_be_predicator s = diff -r e1aa703c8cce -r 72cbbb4d98f3 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Mar 25 13:52:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Mar 25 13:52:23 2022 +0100 @@ -7,7 +7,6 @@ signature SLEDGEHAMMER_ATP_SYSTEMS = sig - type term_order = ATP_Problem.term_order type atp_format = ATP_Problem.atp_format type atp_formula_role = ATP_Problem.atp_formula_role type atp_failure = ATP_Proof.atp_failure @@ -16,8 +15,7 @@ type atp_slice = atp_format * string * string * bool * string type atp_config = {exec : string list * string list, - arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> - term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list, + arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> string list, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, @@ -27,16 +25,6 @@ val default_max_mono_iters : int val default_max_new_mono_instances : int - val term_order : string Config.T - val e_autoscheduleN : string - val e_fun_weightN : string - val e_sym_offset_weightN : string - val e_default_fun_weight : real Config.T - val e_fun_weight_base : real Config.T - val e_fun_weight_span : real Config.T - val e_default_sym_offs_weight : real Config.T - val e_sym_offs_weight_base : real Config.T - val e_sym_offs_weight_span : real Config.T val spass_H1SOS : string val spass_H2 : string val spass_H2LR0LT0 : string @@ -51,7 +39,6 @@ val get_atp : theory -> string -> (unit -> atp_config) val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit - val effective_term_order : Proof.context -> string -> term_order val local_atps : string list val remote_atps : string list val atps : string list @@ -86,8 +73,7 @@ type atp_config = {exec : string list * string list, - arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> - term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list, + arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> string list, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, @@ -139,23 +125,12 @@ val sosN = "sos" val no_sosN = "no_sos" -val smartN = "smart" -(* val kboN = "kbo" *) -val lpoN = "lpo" -val xweightsN = "_weights" -val xprecN = "_prec" -val xsimpN = "_simp" (* SPASS-specific *) - -(* Possible values for "atp_term_order": - "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *) -val term_order = - Attrib.setup_config_string \<^binding>\atp_term_order\ (K smartN) (* agsyHOL *) val agsyhol_config : atp_config = {exec = (["AGSYHOL_HOME"], ["agsyHOL"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => ["--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem], proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, @@ -173,7 +148,7 @@ val alt_ergo_config : atp_config = {exec = (["WHY3_HOME"], ["why3"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => ["--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem], proof_delims = [], @@ -193,81 +168,11 @@ (* E *) -val e_autoscheduleN = "auto" -val e_fun_weightN = "fun_weight" -val e_sym_offset_weightN = "sym_offset_weight" - -(* FUDGE *) -val e_default_fun_weight = - Attrib.setup_config_real \<^binding>\atp_e_default_fun_weight\ (K 20.0) -val e_fun_weight_base = - Attrib.setup_config_real \<^binding>\atp_e_fun_weight_base\ (K 0.0) -val e_fun_weight_span = - Attrib.setup_config_real \<^binding>\atp_e_fun_weight_span\ (K 40.0) -val e_default_sym_offs_weight = - Attrib.setup_config_real \<^binding>\atp_e_default_sym_offs_weight\ (K 1.0) -val e_sym_offs_weight_base = - Attrib.setup_config_real \<^binding>\atp_e_sym_offs_weight_base\ (K ~20.0) -val e_sym_offs_weight_span = - Attrib.setup_config_real \<^binding>\atp_e_sym_offs_weight_span\ (K 60.0) - -fun e_selection_heuristic_case heuristic fw sow = - if heuristic = e_fun_weightN then fw - else if heuristic = e_sym_offset_weightN then sow - else raise Fail ("unexpected " ^ quote heuristic) - -fun scaled_e_selection_weight ctxt heuristic w = - w * Config.get ctxt (e_selection_heuristic_case heuristic - e_fun_weight_span e_sym_offs_weight_span) - + Config.get ctxt (e_selection_heuristic_case heuristic - e_fun_weight_base e_sym_offs_weight_base) - |> Real.ceil |> signed_string_of_int - -fun e_selection_weight_arguments ctxt heuristic sel_weights = - if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then - (* supplied by Stephan Schulz *) - "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ - \--destructive-er-aggressive --destructive-er --presat-simplify \ - \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ - \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^ - e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^ - "(SimulateSOS," ^ - (e_selection_heuristic_case heuristic - e_default_fun_weight e_default_sym_offs_weight - |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^ - ",20,1.5,1.5,1" ^ - (sel_weights () - |> map (fn (s, w) => "," ^ s ^ ":" ^ - scaled_e_selection_weight ctxt heuristic w) - |> implode) ^ - "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ - \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ - \FIFOWeight(PreferProcessed))' " - else - "--auto-schedule " - -val e_ord_weights = map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode "," -fun e_ord_precedence [_] = "" - | e_ord_precedence info = info |> map fst |> space_implode "<" - -fun e_term_order_info_arguments false false _ = "" - | e_term_order_info_arguments gen_weights gen_prec ord_info = - let val ord_info = ord_info () in - (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^ - (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "") - end - val e_config : atp_config = {exec = (["E_HOME"], ["eprover-ho", "eprover"]), - arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn problem => - fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => - ["--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 "KBO6") ^ " " ^ - "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ - " --proof-object=1 " ^ - File.bash_path problem], + arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => + ["--tstp-in --tstp-out --silent --auto-schedule --cpu-limit=" ^ + string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ File.bash_path problem], proof_delims = [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ tstp_proof_delims, @@ -287,12 +192,12 @@ (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN) in (* FUDGE *) - K [((1000 (* infinity *), 1024, meshN), (format, type_enc, lam_trans, false, e_autoscheduleN)), - ((1, 512, meshN), (format, type_enc, lam_trans, false, e_sym_offset_weightN)), - ((1, 128, mepoN), (format, type_enc, lam_trans, false, e_fun_weightN)), - ((1, 724, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)), - ((1, 256, mepoN), (format, type_enc, liftingN, false, e_fun_weightN)), - ((1, 64, mashN), (format, type_enc, combsN, false, e_fun_weightN))] + K [((1000 (* infinity *), 1024, meshN), (format, type_enc, lam_trans, false, "")), + ((1, 512, meshN), (format, type_enc, lam_trans, false, "")), + ((1, 128, mepoN), (format, type_enc, lam_trans, false, "")), + ((1, 724, meshN), (format, "poly_guards??", lam_trans, false, "")), + ((1, 256, mepoN), (format, type_enc, liftingN, false, "")), + ((1, 64, mashN), (format, type_enc, combsN, false, ""))] end, good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -304,7 +209,7 @@ val iprover_config : atp_config = {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^ "--clausifier_options \"--mode clausify\" " ^ "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem], @@ -330,7 +235,7 @@ val leo2_config : atp_config = {exec = (["LEO2_HOME"], ["leo.opt", "leo"]), - arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ => + arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => ["--foatp e --atp e=\"$E_HOME\"/eprover \ \--atp epclextract=\"$E_HOME\"/epclextract \ \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ @@ -356,7 +261,7 @@ (* Include choice? Disabled now since it's disabled for Satallax as well. *) val leo3_config : atp_config = {exec = (["LEO3_HOME"], ["leo3"]), - arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ => + arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \ \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ (if full_proofs then "--nleq --naeq " else "")], @@ -378,7 +283,7 @@ (* Choice is disabled until there is proper reconstruction for it. *) val satallax_config : atp_config = {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => [(case getenv "E_HOME" of "" => "" | home => "-E " ^ home ^ "/eprover ") ^ @@ -410,7 +315,7 @@ val format = DFG Monomorphic in {exec = (["SPASS_HOME"], ["SPASS"]), - arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => fn _ => + arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => ["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem |> extra_options <> "" ? prefix (extra_options ^ " ")], @@ -454,7 +359,7 @@ val vampire_config : atp_config = {exec = (["VAMPIRE_HOME"], ["vampire"]), - arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ => + arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^ " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem |> sos = sosN ? prefix "--sos on "], @@ -494,7 +399,7 @@ THF (Polymorphic, {with_ite = true, with_let = false}, THF_Without_Choice) in {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]), - arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ => + arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => ["--input tptp", "--output tptp", "--timeout " ^ Time.toString timeout, extra_options, File.bash_path problem], proof_delims = tstp_proof_delims, @@ -557,7 +462,7 @@ fun remote_config system_name system_versions proof_delims known_failures prem_role good_slice = {exec = isabelle_scala_function, - arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ => + arguments = fn _ => fn _ => fn command => fn timeout => fn problem => [the_remote_system system_name system_versions, Isabelle_System.absolute_path problem, command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)], @@ -615,7 +520,7 @@ fun dummy_config prem_role format type_enc uncurried_aliases : atp_config = {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]), - arguments = K (K (K (K (K (K []))))), + arguments = K (K (K (K (K [])))), proof_delims = [], known_failures = known_szs_status_failures, prem_role = prem_role, @@ -658,18 +563,6 @@ fun refresh_systems_on_tptp () = Synchronized.change remote_systems (fn _ => get_remote_systems ()) -fun effective_term_order ctxt atp = - let val ord = Config.get ctxt term_order in - if ord = smartN then - {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN), - gen_simp = false} - else - let val is_lpo = String.isSubstring lpoN ord in - {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord, - gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord} - end - end - val local_atps = [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, zipperposition] val remote_atps = diff -r e1aa703c8cce -r 72cbbb4d98f3 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 25 13:52:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 25 13:52:23 2022 +0100 @@ -204,12 +204,7 @@ (state, subgoal, name, "Generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) - fun sel_weights () = atp_problem_selection_weights atp_problem - fun ord_info () = atp_problem_term_order_info atp_problem - - val ord = effective_term_order ctxt name val args = arguments ctxt full_proofs extra run_timeout prob_path - (ord, ord_info, sel_weights) val command = space_implode " " (File.bash_path executable :: args) fun run_command () = @@ -220,9 +215,8 @@ let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) in (Process_Result.out res, Process_Result.timing_elapsed res) end - val _ = - atp_problem - |> lines_of_atp_problem good_format ord ord_info + val _ = atp_problem + |> lines_of_atp_problem good_format (fn () => atp_problem_term_order_info atp_problem) |> (exec <> isabelle_scala_function) ? cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path