split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"

--- a/NEWS	Tue Jan 11 12:08:03 2022 +0100
+++ b/NEWS	Tue Jan 11 22:07:04 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 ***

--- a/src/Doc/Sledgehammer/document/root.tex	Tue Jan 11 12:08:03 2022 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Tue Jan 11 22:07:04 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}
 

--- a/src/HOL/TPTP/mash_eval.ML	Tue Jan 11 12:08:03 2022 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Tue Jan 11 22:07:04 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

--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Tue Jan 11 12:08:03 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Tue Jan 11 22:07:04 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 =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Jan 11 12:08:03 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Jan 11 22:07:04 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>\<open>sledgehammer_atp_dest_dir\<close> (K "")
+val atp_problem_dest_dir =
+  Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_problem_dest_dir\<close> (K "")
+val atp_proof_dest_dir =
+  Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_proof_dest_dir\<close> (K "")
 val atp_problem_prefix =
   Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_problem_prefix\<close> (K "prob")
 val atp_completish = Attrib.setup_config_int \<^binding>\<open>sledgehammer_atp_completish\<close> (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),