# HG changeset patch
# User desharna
# Date 1751977629 -7200
# Node ID 81b61be3ca0aedb8bfa3be0c90685dbed161b078
# Parent  547335b410054f9a7dc82d91762fd9d79cd671e1
added basic support for persistent prover data to Sledgehammer

diff -r 547335b41005 -r 81b61be3ca0a src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Jul 03 13:53:14 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Jul 08 14:27:09 2025 +0200
@@ -98,6 +98,17 @@
   | suffix_of_mode MaSh = ""
   | suffix_of_mode Minimize = "_min"
 
+fun tptp_logic_of_atp_format CNF = "CNF"
+  | tptp_logic_of_atp_format CNF_UEQ = "CNF"
+  | tptp_logic_of_atp_format FOF = "FOF"
+  | tptp_logic_of_atp_format (TFF (Monomorphic, Without_FOOL)) = "TF0"
+  | tptp_logic_of_atp_format (TFF (Polymorphic, Without_FOOL)) = "TF1"
+  | tptp_logic_of_atp_format (TFF (Monomorphic, With_FOOL _)) = "TX0"
+  | tptp_logic_of_atp_format (TFF (Polymorphic, With_FOOL _)) = "TX1"
+  | tptp_logic_of_atp_format (THF (Monomorphic, _, _)) = "TH0"
+  | tptp_logic_of_atp_format (THF (Polymorphic, _, _)) = "TH1"
+  | tptp_logic_of_atp_format (DFG _) = "DFG"
+
 fun run_atp mode name
     ({debug, verbose, overlord, abduce = abduce_max_candidates, strict, max_mono_iters,
       max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout,
@@ -231,13 +242,32 @@
 
         fun run_command () =
           let
+            val sledgehammer_persistent_data_dir =
+              Options.default_string \<^system_option>\<open>sledgehammer_persistent_data_dir\<close>
+            val env =
+              if sledgehammer_persistent_data_dir = "" then
+                []
+              else
+                let
+                  val tptp_logic = tptp_logic_of_atp_format good_format
+                  val thy_long_name = Context.theory_long_name thy
+                  val session_name = Long_Name.qualifier thy_long_name
+                  val dir =
+                    Path.expand (Path.explode sledgehammer_persistent_data_dir +
+                      Path.explode (name ^ "-" ^ session_name) +
+                      Path.explode tptp_logic)
+                in [("SLH_PERSISTENT_DATA_DIR", Path.implode dir)] end
+
             val f = fn _ =>
               if exec = isabelle_scala_function then
                 let val {output, ...} = SystemOnTPTP.run_system_encoded args
                 in output end
               else
-                let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect)
-                in Process_Result.out res end
+                Bash.script command
+                  |> Bash.putenv env
+                  |> Bash.redirect
+                  |> Isabelle_System.bash_process
+                  |> Process_Result.out
             (* Hackish: The following lines try to make the TPTP problem and command line more
             deterministic and constant. *)
             val hackish_lines = drop 2 lines_of_atp_problem
diff -r 547335b41005 -r 81b61be3ca0a src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Thu Jul 03 13:53:14 2025 +0200
+++ b/src/HOL/Tools/etc/options	Tue Jul 08 14:27:09 2025 +0200
@@ -32,6 +32,9 @@
 public option sledgehammer_timeout : int = 30
   -- "provers will be interrupted after this time (in seconds)"
 
+public option sledgehammer_persistent_data_dir : string = ""
+  -- "Directory where the automatic provers called by Sledgehammer will save persistent data"
+
 public option SystemOnTPTP : string = "https://tptp.org/cgi-bin/SystemOnTPTPFormReply"
   -- "URL for SystemOnTPTP service"