# HG changeset patch # User desharna # Date 1642001587 -3600 # Node ID a10873b3c7d45bb3fddbe5fe45838177bc0b707d # Parent 10df7a627ab6e96fa2f54be37b195fdef8530ab2# Parent 4d77dd3019d1237345e8b5ca9f2324a01babc2c9 merged diff -r 4d77dd3019d1 -r a10873b3c7d4 NEWS --- a/NEWS Tue Jan 11 06:48:02 2022 +0000 +++ b/NEWS Wed Jan 12 16:33:07 2022 +0100 @@ -43,6 +43,15 @@ INCOMPATIBILITY. - Added support for TX0 and TX1 TPTP formats and $ite/$let expressions in TH0 and TH1. + - Replaced option "sledgehammer_atp_dest_dir" by + "sledgehammer_atp_problem_dest_dir", for problem files, and + "sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY. + +* Mirabelle: + - Replaced sledgehammer option "keep" by + "keep_probs", for problems files, and + "keep_proofs" for proof files. Minor INCOMPATIBILITY. + *** System *** diff -r 4d77dd3019d1 -r a10873b3c7d4 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Tue Jan 11 06:48:02 2022 +0000 +++ b/src/Doc/Sledgehammer/document/root.tex Wed Jan 12 16:33:07 2022 +0100 @@ -1328,7 +1328,7 @@ \begin{verbatim} isabelle mirabelle -d $AFP -O output \ - -A "sledgehammer[provers = e, timeout = 5, keep = true]" \ + -A "sledgehammer[provers = e, timeout = 5, keep_probs = true]" \ VeriComp \end{verbatim} diff -r 4d77dd3019d1 -r a10873b3c7d4 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Tue Jan 11 06:48:02 2022 +0000 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jan 12 16:33:07 2022 +0100 @@ -106,7 +106,7 @@ let val prob_prefix = "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ method in - Config.put atp_dest_dir dir + Config.put atp_problem_dest_dir dir #> Config.put atp_problem_prefix (prob_prefix ^ "__") #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) end diff -r 4d77dd3019d1 -r a10873b3c7d4 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jan 11 06:48:02 2022 +0000 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jan 12 16:33:07 2022 +0100 @@ -2377,13 +2377,14 @@ else fold (ifact_lift add_formula_var_types) (conjs @ facts) [] fun add_undefined_const T = let - (* FIXME: make sure type arguments are filtered / clean up code *) - val (s, s') = - `(make_fixed_const NONE) \<^const_name>\undefined\ - |> (is_type_enc_mangling type_enc ? mangled_const_name type_enc [T]) + val name = `(make_fixed_const NONE) \<^const_name>\undefined\ + val ((s, s'), Ts) = + if is_type_enc_mangling type_enc then + (mangled_const_name type_enc [T] name, []) + else + (name, [T]) in - Symtab.map_default (s, []) - (insert_type thy #3 (s', [T], T, false, 0, false)) + Symtab.map_default (s, []) (insert_type thy #3 (s', Ts, T, false, 0, false)) end fun add_TYPE_const () = let val (s, s') = TYPE_name in @@ -2400,7 +2401,9 @@ Native (_, _, Raw_Polymorphic phantoms, _) => phantoms = Without_Phantom_Type_Vars ? add_TYPE_const () | Native _ => I - | _ => fold add_undefined_const (var_types ()))) + | _ => + (* Add constants "undefined" as witnesses that the types are inhabited. *) + fold add_undefined_const (var_types ()))) end (* We add "bool" in case the helper "True_or_False" is included later. *) diff -r 4d77dd3019d1 -r a10873b3c7d4 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Tue Jan 11 06:48:02 2022 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Wed Jan 12 16:33:07 2022 +0100 @@ -22,13 +22,15 @@ val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) -val keepK = "keep" (*=BOOL: keep temporary files created by sledgehammer*) +val keep_probsK = "keep_probs" (*=BOOL: keep temporary problem files created by sledgehammer*) +val keep_proofsK = "keep_proofs" (*=BOOL: keep temporary proof files created by ATPs*) val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*) val term_orderK = "term_order" (*=STRING: term order (in E)*) (*defaults used in this Mirabelle action*) val check_trivial_default = false -val keep_default = false +val keep_probs_default = false +val keep_proofs_default = false datatype sh_data = ShData of { calls: int, @@ -271,23 +273,24 @@ local -fun run_sh params e_selection_heuristic term_order force_sos dir pos state = +fun run_sh params e_selection_heuristic term_order force_sos keep pos state = let - fun set_file_name (SOME dir) = + fun set_file_name (SOME (dir, keep_probs, keep_proofs)) = let val filename = "prob_" ^ StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^ StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos)) in - Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir - #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__") + Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__") + #> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir) + #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir) #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ()) end | set_file_name NONE = I val state' = state |> Proof.map_context - (set_file_name dir + (set_file_name keep #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) e_selection_heuristic |> the_default I) #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) @@ -308,27 +311,27 @@ in fun run_sledgehammer change_data (params as {provers, ...}) output_dir - e_selection_heuristic term_order force_sos keep proof_method_from_msg thy_index trivial - proof_method named_thms pos st = + e_selection_heuristic term_order force_sos keep_probs keep_proofs proof_method_from_msg thy_index + trivial proof_method named_thms pos st = let val thy = Proof.theory_of st val thy_name = Context.theory_name thy val triv_str = if trivial then "[T] " else "" val _ = change_data inc_sh_calls val _ = if trivial then () else change_data inc_sh_nontriv_calls - val keep_dir = - if keep then + val keep = + if keep_probs orelse keep_proofs then let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in Path.append output_dir (Path.basic subdir) |> Isabelle_System.make_directory |> Path.implode - |> SOME + |> (fn dir => SOME (dir, keep_probs, keep_proofs)) end else NONE val prover_name = hd provers val (sledgehamer_outcome, msg, cpu_time) = - run_sh params e_selection_heuristic term_order force_sos keep_dir pos st + run_sh params e_selection_heuristic term_order force_sos keep pos st val outcome_msg = (case sledgehamer_outcome of Sledgehammer.SH_Some {used_facts, run_time, ...} => @@ -440,7 +443,8 @@ (* Parse Mirabelle-specific parameters *) val check_trivial = Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default) - val keep = Mirabelle.get_bool_argument arguments (keepK, keep_default) + val keep_probs = Mirabelle.get_bool_argument arguments (keep_probsK, keep_probs_default) + val keep_proofs = Mirabelle.get_bool_argument arguments (keep_proofsK, keep_proofs_default) val e_selection_heuristic = AList.lookup (op =) arguments e_selection_heuristicK val term_order = AList.lookup (op =) arguments term_orderK val force_sos = AList.lookup (op =) arguments force_sosK @@ -473,7 +477,8 @@ handle Timeout.TIMEOUT _ => false val (outcome, log1) = run_sledgehammer change_data params output_dir e_selection_heuristic term_order - force_sos keep proof_method_from_msg theory_index trivial meth named_thms pos pre + force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial meth + named_thms pos pre val log2 = (case !named_thms of SOME thms => diff -r 4d77dd3019d1 -r a10873b3c7d4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Jan 11 06:48:02 2022 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Jan 12 16:33:07 2022 +0100 @@ -11,7 +11,8 @@ type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover - val atp_dest_dir : string Config.T + val atp_problem_dest_dir : string Config.T + val atp_proof_dest_dir : string Config.T val atp_problem_prefix : string Config.T val atp_completish : int Config.T val atp_full_names : bool Config.T @@ -36,7 +37,10 @@ open Sledgehammer_Prover (* Empty string means create files in Isabelle's temporary files directory. *) -val atp_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_dest_dir\ (K "") +val atp_problem_dest_dir = + Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_dest_dir\ (K "") +val atp_proof_dest_dir = + Attrib.setup_config_string \<^binding>\sledgehammer_atp_proof_dest_dir\ (K "") val atp_problem_prefix = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_prefix\ (K "prob") val atp_completish = Attrib.setup_config_int \<^binding>\sledgehammer_atp_completish\ (K 0) @@ -144,20 +148,25 @@ val completish = Config.get ctxt atp_completish val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt - val (dest_dir, problem_prefix) = - if overlord then overlord_file_location_of_prover name - else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix) + val (problem_dest_dir, proof_dest_dir, problem_prefix) = + if overlord then + overlord_file_location_of_prover name + |> (fn (dir, prefix) => (dir, dir, prefix)) + else + (Config.get ctxt atp_problem_dest_dir, + Config.get ctxt atp_proof_dest_dir, + Config.get ctxt atp_problem_prefix) val problem_file_name = Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ suffix_of_mode mode ^ "_" ^ string_of_int subgoal) |> Path.ext "p" val prob_path = - if dest_dir = "" then + if problem_dest_dir = "" then File.tmp_path problem_file_name - else if File.exists (Path.explode dest_dir) then - Path.explode dest_dir + problem_file_name + else if File.exists (Path.explode problem_dest_dir) then + Path.explode problem_dest_dir + problem_file_name else - error ("No such directory: " ^ quote dest_dir) + error ("No such directory: " ^ quote problem_dest_dir) val executable = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => @@ -340,17 +349,21 @@ (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) - fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else () + fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () fun export (_, (output, _, _, _, _), _) = let - val make_export_path = + val proof_dest_dir_path = Path.explode proof_dest_dir + val make_export_file_name = Path.split_ext #> apfst (Path.explode o suffix "_proof" o Path.implode) #> swap #> uncurry Path.ext in - if dest_dir = "" then () - else File.write (make_export_path prob_path) output + if proof_dest_dir = "" then Output.system_message "don't export proof" + else if File.exists proof_dest_dir_path then + File.write (proof_dest_dir_path + make_export_file_name problem_file_name) output + else + error ("No such directory: " ^ quote proof_dest_dir) end val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome),