# HG changeset patch
# User wenzelm
# Date 1738840067 -3600
# Node ID 023845c29d48fb69198bc13a783ddf7ca4e28f12
# Parent  cbcc3ee0b98916b811001260fefbdad431e02b07
avoid tmp files to improve robustness on Windows, where ERROR_PATH_NOT_FOUND has been seen (see also 569135d7352a);

diff -r cbcc3ee0b989 -r 023845c29d48 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Feb 05 23:11:07 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Feb 06 12:07:47 2025 +0100
@@ -60,35 +60,33 @@
 
 local
 
-fun make_command command options problem_path proof_path =
-  Bash.strings (command () @ options) ^ " " ^
-    File.bash_platform_path problem_path ^
-    " > " ^ File.bash_path proof_path ^ " 2>&1"
-
 fun with_trace ctxt msg f x =
   let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()
   in f x end
 
-fun run ctxt name mk_cmd input =
+fun run ctxt name cmd input =
   (case SMT_Config.certificates_of ctxt of
     NONE =>
       if not (SMT_Config.is_available ctxt name) then
         error ("The SMT solver " ^ quote name ^ " is not installed")
       else if Config.get ctxt SMT_Config.debug_files = "" then
-        with_trace ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run mk_cmd) input
+        with_trace ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run cmd) input
       else
         let
           val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files)
           val in_path = Path.ext "smt_in" base_path
           val out_path = Path.ext "smt_out" base_path
-        in Cache_IO.raw_run mk_cmd input in_path out_path end
+          val _ = File.write in_path input
+          val result = Cache_IO.run cmd input
+          val _ = Bytes.write out_path (Bytes.terminate_lines (Process_Result.out_lines result))
+        in result end
   | SOME certs =>
       (case Cache_IO.lookup certs input of
         (NONE, key) =>
           if Config.get ctxt SMT_Config.read_only_certificates then
             error ("Bad certificate cache: missing certificate")
           else
-            Cache_IO.run_and_cache certs key mk_cmd input
+            Cache_IO.run_and_cache certs key cmd input
       | (SOME output, _) =>
           with_trace ctxt ("Using cached certificate from " ^
             Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output))
@@ -99,14 +97,14 @@
   | normal_return_codes "verit" = [0, 14, 255]
   | normal_return_codes _ = [0, 1]
 
-fun run_solver ctxt name mk_cmd input =
+fun run_solver ctxt name cmd input =
   let
     fun pretty tag lines = Pretty.string_of (Pretty.big_list tag (map Pretty.str lines))
 
     val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input
 
     val ({elapsed, ...}, result) =
-      Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input
+      Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name cmd)) input
     val res = Process_Result.out_lines result
     val err = Process_Result.err_lines result
     val return_code = Process_Result.rc result
@@ -150,12 +148,13 @@
       |> SMT_Translate.translate ctxt name smt_options comments
       ||> tap trace_replay_data
 
-    val run_solver = run_solver ctxt' name (make_command command options)
+    val cmd = Bash.script (Bash.strings (command () @ options))
+    val run_cmd = run_solver ctxt' name cmd
 
     val output_lines =
       (case memoize_fun_call of
-        NONE => run_solver str
-      | SOME memoize => split_lines (memoize (cat_lines o run_solver) str))
+        NONE => run_cmd str
+      | SOME memoize => split_lines (memoize (cat_lines o run_cmd) str))
   in (output_lines, replay_data) end
 
 end
diff -r cbcc3ee0b989 -r 023845c29d48 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Wed Feb 05 23:11:07 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Thu Feb 06 12:07:47 2025 +0100
@@ -229,7 +229,7 @@
   name = "z3",
   class = select_class,
   avail = make_avail "Z3",
-  command = make_command "Z3",
+  command = fn () => [getenv "Z3_SOLVER", "-in"],
   options = z3_options,
   smt_options = [(":produce-proofs", "true")],
   good_slices =
diff -r cbcc3ee0b989 -r 023845c29d48 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Wed Feb 05 23:11:07 2025 +0100
+++ b/src/Tools/cache_io.ML	Thu Feb 06 12:07:47 2025 +0100
@@ -6,52 +6,18 @@
 
 signature CACHE_IO =
 sig
-  (*IO wrapper*)
-  val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> Process_Result.T
-  val run: (Path.T -> Path.T -> string) -> string -> Process_Result.T
-
-  (*cache*)
   type cache
   val unsynchronized_init: Path.T -> cache
   val cache_path_of: cache -> Path.T
   val lookup: cache -> string -> Process_Result.T option * string
-  val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> Process_Result.T
-  val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> Process_Result.T
+  val run: Bash.params -> string -> Process_Result.T
+  val run_and_cache: cache -> string -> Bash.params -> string -> Process_Result.T
+  val run_cached: cache -> Bash.params -> string -> Process_Result.T
 end
 
 structure Cache_IO : CACHE_IO =
 struct
 
-(* IO wrapper *)
-
-val cache_io_prefix = "cache-io-"
-
-fun try_read_lines path =
-  let
-    fun loop n =
-      (case try File.read_lines path of
-        SOME lines => lines
-      | NONE => if n > 0 then (OS.Process.sleep (seconds 0.05); loop (n - 1)) else [])
-  in if File.exists path then loop (if ML_System.platform_is_windows then 20 else 0) else [] end
-
-fun raw_run make_cmd str in_path out_path =
-  let
-    val _ = File.write in_path str
-    val (err, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
-    val out_lines = try_read_lines out_path
-  in
-    Process_Result.make
-      {rc = rc, out_lines = out_lines, err_lines = split_lines err, timing = Timing.zero}
-  end
-
-fun run make_cmd str =
-  Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path =>
-    Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path =>
-      raw_run make_cmd str in_path out_path))
-
-
-(* cache *)
-
 abstype cache = Cache of {
   path: Path.T,
   table: (int * (int * int * int) Symtab.table) Synchronized.var }
@@ -106,9 +72,26 @@
           in ((SOME result, key), tab) end))
   end
 
-fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str =
+fun run cmd input =
   let
-    val result = run make_cmd str
+    val result = cmd
+      |> Bash.input (Bytes.string input)
+      |> Bash.redirect
+      |> Isabelle_System.bash_process
+    val rc = Process_Result.rc result
+  in
+    if rc = Process_Result.startup_failure_rc then
+      Process_Result.make
+       {rc = rc,
+        err_lines = Process_Result.out_lines result,
+        out_lines = [],
+        timing = Process_Result.timing result}
+    else result
+  end
+
+fun run_and_cache (Cache {path = cache_path, table}) key cmd input =
+  let
+    val result = run cmd input
     val out_lines = Process_Result.out_lines result
     val err_lines = Process_Result.err_lines result
     val (l1, l2) = apply2 length (out_lines, err_lines)
@@ -122,9 +105,9 @@
         in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
   in result end
 
-fun run_cached cache make_cmd str =
-  (case lookup cache str of
-    (NONE, key) => run_and_cache cache key make_cmd str
+fun run_cached cache cmd input =
+  (case lookup cache input of
+    (NONE, key) => run_and_cache cache key cmd input
   | (SOME output, _) => output)
 
 end