# HG changeset patch
# User wenzelm
# Date 1738856690 -3600
# Node ID 06dce439a4f0ba53443167ca670463884cda4b2a
# Parent  50dd4fc40fcbdc6f0139f73c80113beed081035f# Parent  090bd4ce91429452cf395a44194de31069d47241
merged

diff -r 50dd4fc40fcb -r 06dce439a4f0 src/HOL/TPTP/TPTP_Interpret_Test.thy
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Feb 06 16:44:50 2025 +0100
@@ -133,7 +133,7 @@
           else
             (warning (" test: file " ^ Path.print file ^
              " raised exception: " ^ Runtime.exn_message exn);
-             {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
+             Timing.zero)
       val to_real = Time.toReal
       val diff_elapsed =
         #elapsed t2 - #elapsed t1
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -63,7 +63,7 @@
 
   (*setup*)
   val print_setup: Proof.context -> unit
-end;
+end
 
 structure SMT_Config: SMT_CONFIG =
 struct
@@ -74,7 +74,7 @@
   name: string,
   class: Proof.context -> SMT_Util.class,
   avail: unit -> bool,
-  options: Proof.context -> string list}
+  options: Proof.context -> string list};
 
 structure Data = Generic_Data
 (
@@ -100,7 +100,7 @@
 
 fun set_solver_options (name, options) =
   let val opts = String.tokens (Symbol.is_ascii_blank o str) options
-  in map_solvers (Symtab.map_entry name (apsnd (K opts))) end
+  in map_solvers (Symtab.map_entry name (apsnd (K opts))) end;
 
 fun add_solver (info as {name, ...} : solver_info) context =
   if defined_solvers context name then
@@ -111,7 +111,7 @@
     |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
         (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
           (Thm.declaration_attribute o K o set_solver_options o pair name))
-        ("additional command-line options for SMT solver " ^ quote name))
+        ("additional command-line options for SMT solver " ^ quote name));
 
 val all_solvers_of' = Symtab.keys o get_solvers';
 val all_solvers_of = all_solvers_of' o Context.Proof;
@@ -130,7 +130,7 @@
       if Context_Position.is_visible ctxt then
         warning ("The SMT solver " ^ quote name ^ " is not installed")
       else ()
-  | warn_solver _ _ = ()
+  | warn_solver _ _ = ();
 
 fun select_solver name context =
   if not (defined_solvers context name) then
@@ -139,79 +139,79 @@
     (warn_solver context name; put_solver name context)
   else put_solver name context;
 
-fun no_solver_err () = error "No SMT solver selected"
+fun no_solver_err () = error "No SMT solver selected";
 
 fun solver_of ctxt =
   (case get_solver ctxt of
     SOME name => name
-  | NONE => no_solver_err ())
+  | NONE => no_solver_err ());
 
 fun solver_info_of default select ctxt =
   (case get_solver ctxt of
     NONE => default ()
-  | SOME name => select (Symtab.lookup (get_solvers ctxt) name))
+  | SOME name => select (Symtab.lookup (get_solvers ctxt) name));
 
 fun solver_class_of ctxt =
   let fun class_of ({class, ...}: solver_info, _) = class ctxt
-  in solver_info_of no_solver_err (class_of o the) ctxt end
+  in solver_info_of no_solver_err (class_of o the) ctxt end;
 
 fun solver_options_of ctxt =
   let
     fun all_options NONE = []
       | all_options (SOME ({options, ...} : solver_info, opts)) =
           opts @ options ctxt
-  in solver_info_of (K []) all_options ctxt end
+  in solver_info_of (K []) all_options ctxt end;
 
-val setup_solver =
-  Attrib.setup \<^binding>\<open>smt_solver\<close>
+val _ =
+  Theory.setup (Attrib.setup \<^binding>\<open>smt_solver\<close>
     (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
       (Thm.declaration_attribute o K o select_solver))
-    "SMT solver configuration"
+    "SMT solver configuration");
 
 
 (* options *)
 
-val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true)
-val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 0.0)
-val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0)
-val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1)
-val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false)
-val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true)
-val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false)
-val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false)
-val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false)
-val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false)
-val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false)
-val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true)
-val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false)
-val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10)
-val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500)
-val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1)
-val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false)
-val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true)
-val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false)
-val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false)
-val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "")
-val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite")
-val cvc_experimental_lethe = Attrib.setup_config_bool \<^binding>\<open>smt_cvc_lethe\<close> (K false)
+val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true);
+val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 0.0);
+val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0);
+val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1);
+val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false);
+val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true);
+val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false);
+val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false);
+val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false);
+val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false);
+val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false);
+val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true);
+val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false);
+val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10);
+val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500);
+val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1);
+val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false);
+val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true);
+val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false);
+val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false);
+val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "");
+val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite");
+val cvc_experimental_lethe = Attrib.setup_config_bool \<^binding>\<open>smt_cvc_lethe\<close> (K false);
 
 
 (* diagnostics *)
 
-fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
+fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ();
 
-fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
-fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
-fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics)
+fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose);
+fun trace_msg ctxt = cond_trace (Config.get ctxt trace);
+fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics);
 
-fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else ()
-fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else ()
+fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else ();
+fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else ();
 
-fun spy_verit ctxt  = Config.get ctxt spy_verit_attr
-fun spy_Z3 ctxt  = Config.get ctxt spy_z3
-fun compress_verit_proofs ctxt  = Config.get ctxt trace_verit_compression
+fun spy_verit ctxt  = Config.get ctxt spy_verit_attr;
+fun spy_Z3 ctxt  = Config.get ctxt spy_z3;
+fun compress_verit_proofs ctxt  = Config.get ctxt trace_verit_compression;
 
-fun use_lethe_proof_from_cvc ctxt  = Config.get ctxt cvc_experimental_lethe
+fun use_lethe_proof_from_cvc ctxt  = Config.get ctxt cvc_experimental_lethe;
 
 
 (* tools *)
@@ -222,9 +222,9 @@
 
 fun with_time_limit ctxt timeout_config f x =
   Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
-    handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
+    handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out;
 
-fun with_timeout ctxt = with_time_limit ctxt timeout
+fun with_timeout ctxt = with_time_limit ctxt timeout;
 
 
 (* certificates *)
@@ -237,46 +237,37 @@
     let val dir = Resources.master_directory (Context.theory_of context) + Path.explode name
     in SOME (Cache_IO.unsynchronized_init dir) end);
 
-val setup_certificates =
-  Attrib.setup \<^binding>\<open>smt_certificates\<close>
+val _ =
+  Theory.setup (Attrib.setup \<^binding>\<open>smt_certificates\<close>
     (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))
-    "SMT certificates configuration"
+    "SMT certificates configuration");
 
 
-(* setup *)
-
-val _ = Theory.setup (
-  setup_solver #>
-  setup_certificates)
+(* print_setup *)
 
 fun print_setup ctxt =
   let
-    fun string_of_bool b = if b then "true" else "false"
-
-    val names = available_solvers_of ctxt
-    val ns = if null names then ["(none)"] else sort_strings names
-    val n = the_default "(none)" (get_solver ctxt)
-    val opts = solver_options_of ctxt
-
-    val t = string_of_real (Config.get ctxt timeout)
+    val names = available_solvers_of ctxt;
+    val ns = if null names then ["(none)"] else sort_strings names;
+    val n = the_default "(none)" (get_solver ctxt);
+    val opts = solver_options_of ctxt;
+    val t = seconds (Config.get ctxt timeout)
 
     val certs_filename =
       (case get_certificates_path ctxt of
         SOME path => Path.print path
-      | NONE => "(disabled)")
-  in
-    Pretty.writeln (Pretty.big_list "SMT setup:" [
-      Pretty.str ("Current SMT solver: " ^ n),
+      | NONE => "(disabled)");
+
+    val items =
+     [Pretty.str ("Current SMT solver: " ^ n),
       Pretty.str ("Current SMT solver options: " ^ implode_space opts),
       Pretty.str_list "Available SMT solvers: "  "" ns,
-      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
-      Pretty.str ("With proofs: " ^
-        string_of_bool (not (Config.get ctxt oracle))),
+      Pretty.str ("Current timeout: " ^ (if Timeout.ignored t then "(none)" else Time.message t)),
+      Pretty.str ("With proofs: " ^ Value.print_bool (not (Config.get ctxt oracle))),
       Pretty.str ("Certificates cache: " ^ certs_filename),
-      Pretty.str ("Fixed certificates: " ^
-        string_of_bool (Config.get ctxt read_only_certificates))])
-  end
+      Pretty.str ("Fixed certificates: " ^ Value.print_bool (Config.get ctxt read_only_certificates))];
+  in Pretty.writeln (Pretty.big_list "SMT setup:" (map (Pretty.item o single) items)) end;
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>smt_status\<close>
@@ -284,4 +275,4 @@
     \and the values of SMT configuration options"
     (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
 
-end;
+end
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Feb 06 16:44:50 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,20 +97,23 @@
   | 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, ...}, {redirected_output = res, output = err, return_code}) =
-      Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input
+    val ({elapsed, ...}, result) =
+      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
     val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
 
     val output = drop_suffix (equal "") res
     val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
-    val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
-    val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
+    val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Time.message elapsed]
+    val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Time.message elapsed]
 
     val _ = member (op =) (normal_return_codes name) return_code orelse
       raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
@@ -136,23 +137,24 @@
 
 in
 
-fun invoke memoize_fun_call name command options smt_options ithms ctxt =
+fun invoke memoize_fun_call name command cmd_options smt_options ithms ctxt =
   let
-    val options = options @ SMT_Config.solver_options_of ctxt
+    val options = cmd_options @ SMT_Config.solver_options_of ctxt
     val comments = [implode_space options]
 
-    val (str, replay_data as {context = ctxt', ...}) =
+    val (input, replay_data as {context = ctxt', ...}) =
       ithms
       |> tap (trace_assms ctxt)
       |> 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 input
+      | SOME memoize => split_lines (memoize (cat_lines o run_cmd) input))
   in (output_lines, replay_data) end
 
 end
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Thu Feb 06 16:44:50 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 50dd4fc40fcb -r 06dce439a4f0 src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/Concurrent/timeout.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -15,7 +15,7 @@
   val end_time: Time.time -> Time.time
   val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
   val apply_physical: Time.time -> ('a -> 'b) -> 'a -> 'b
-  val print: Time.time -> string
+  val message: Time.time -> string
 end;
 
 structure Timeout: TIMEOUT =
@@ -59,6 +59,6 @@
 fun apply timeout f x = apply' {physical = false, timeout = timeout} f x;
 fun apply_physical timeout f x = apply' {physical = true, timeout = timeout} f x;
 
-fun print t = "Timeout after " ^ Value.print_time t ^ "s";
+fun message t = "Timeout after " ^ Time.message t;
 
 end;
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/General/bytes.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -36,6 +36,7 @@
   val split_lines: T -> string list
   val trim_split_lines: T -> string list
   val cat_lines: string list -> T
+  val terminate_lines: string list -> T
   val read_block: int -> BinIO.instream -> string
   val read_stream: int -> BinIO.instream -> T
   val write_stream: BinIO.outstream -> T -> unit
@@ -190,6 +191,8 @@
 
 fun cat_lines lines = build (fold add (separate "\n" lines));
 
+fun terminate_lines lines = build (fold (fn line => add line #> add "\n") lines);
+
 
 (* IO *)
 
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Pure/General/time.ML
--- a/src/Pure/General/time.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/General/time.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/time.scala
     Author:     Makarius
 
-Time based on nanoseconds (idealized).
+Time based on nanoseconds (idealized), printed as milliseconds.
 *)
 
 signature TIME =
@@ -10,6 +10,9 @@
   val min: time * time -> time
   val max: time * time -> time
   val scale: real -> time -> time
+  val parse: string -> time
+  val print: time -> string
+  val message: time -> string
 end;
 
 structure Time: TIME =
@@ -22,4 +25,15 @@
 
 fun scale s t = Time.fromNanoseconds (Real.ceil (s * Real.fromInt (Time.toNanoseconds t)));
 
+fun parse s =
+  (case Time.fromString s of
+    SOME t => t
+  | NONE => raise Fail ("Bad time " ^ quote s));
+
+fun print t =
+  if t < Time.zeroTime then "-" ^ Time.toString (Time.zeroTime - t)
+  else Time.toString t;
+
+fun message t = print t ^ "s";
+
 end;
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/General/timing.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -16,6 +16,7 @@
 sig
   include BASIC_TIMING
   type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
+  val zero: timing
   type start
   val start: unit -> start
   val result: start -> timing
@@ -34,6 +35,8 @@
 
 type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
 
+val zero: timing = {elapsed = Time.zeroTime, cpu = Time.zeroTime, gc = Time.zeroTime};
+
 
 (* timer control *)
 
@@ -83,9 +86,9 @@
   is_relevant_time gc;
 
 fun message {elapsed, cpu, gc} =
-  Value.print_time elapsed ^ "s elapsed time, " ^
-  Value.print_time cpu ^ "s cpu time, " ^
-  Value.print_time gc ^ "s GC time" handle Time.Time => "";
+  Time.message elapsed ^ " elapsed time, " ^
+  Time.message cpu ^ " cpu time, " ^
+  Time.message gc ^ " GC time" handle Time.Time => "";
 
 fun cond_timeit enabled msg e =
   if enabled then
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Pure/General/value.ML
--- a/src/Pure/General/value.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/General/value.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -13,8 +13,6 @@
   val print_int: int -> string
   val parse_real: string -> real
   val print_real: real -> string
-  val parse_time: string -> Time.time
-  val print_time: Time.time -> string
 end;
 
 structure Value: VALUE =
@@ -82,16 +80,4 @@
     | _ => s)
   end;
 
-
-(* time *)
-
-fun parse_time s =
-  (case Time.fromString s of
-    SOME x => x
-  | NONE => raise Fail ("Bad time " ^ quote s));
-
-fun print_time x =
-  if x < Time.zeroTime then "-" ^ Time.toString (Time.zeroTime - x)
-  else Time.toString x;
-
 end;
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/Isar/runtime.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -113,7 +113,7 @@
         let
           val msg =
             (case exn of
-              Timeout.TIMEOUT t => Timeout.print t
+              Timeout.TIMEOUT t => Timeout.message t
             | TOPLEVEL_ERROR => "Error"
             | ERROR "" => "Error"
             | ERROR msg => msg
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -703,9 +703,9 @@
 val gcN = "gc";
 
 fun timing_properties {elapsed, cpu, gc} =
- [(elapsedN, Value.print_time elapsed),
-  (cpuN, Value.print_time cpu),
-  (gcN, Value.print_time gc)];
+ [(elapsedN, Time.print elapsed),
+  (cpuN, Time.print cpu),
+  (gcN, Time.print gc)];
 
 val timingN = "timing";
 fun timing t = (timingN, timing_properties t);
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/ROOT.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -54,6 +54,7 @@
 ML_file "General/value.ML";
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
+ML_file "General/time.ML";
 ML_file "PIDE/markup.ML";
 ML_file "General/utf8.ML";
 ML_file "General/scan.ML";
@@ -94,7 +95,6 @@
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
 ML_file "General/seq.ML";
-ML_file "General/time.ML";
 ML_file "General/timing.ML";
 ML_file "General/sha1.ML";
 
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Pure/System/bash.ML
--- a/src/Pure/System/bash.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/System/bash.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -10,10 +10,10 @@
   val strings: string list -> string
   type params
   val dest_params: params ->
-   {script: string, input: string, cwd: Path.T option, putenv: (string * string) list,
+   {script: string, input: Bytes.T, cwd: Path.T option, putenv: (string * string) list,
     redirect: bool, timeout: Time.time, description: string}
   val script: string -> params
-  val input: string -> params -> params
+  val input: Bytes.T -> params -> params
   val cwd: Path.T -> params -> params
   val putenv: (string * string) list -> params -> params
   val redirect: params -> params
@@ -56,7 +56,7 @@
 
 abstype params =
   Params of
-   {script: string, input: string, cwd: Path.T option, putenv: (string * string) list,
+   {script: string, input: Bytes.T, cwd: Path.T option, putenv: (string * string) list,
     redirect: bool, timeout: Time.time, description: string}
 with
 
@@ -69,7 +69,7 @@
 fun map_params f (Params {script, input, cwd, putenv, redirect, timeout, description}) =
   make_params (f (script, input, cwd, putenv, redirect, timeout, description));
 
-fun script script = make_params (script, "", NONE, [], false, Time.zeroTime, "");
+fun script script = make_params (script, Bytes.empty, NONE, [], false, Time.zeroTime, "");
 
 fun input input =
   map_params (fn (script, _, cwd, putenv, redirect, timeout, description) =>
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/System/isabelle_system.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -41,13 +41,15 @@
     val {script, input, cwd, putenv, redirect, timeout, description} =
       Bash.dest_params params;
     val server_run =
-      [Bash.server_run, script, input,
-        let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end,
-        let open XML.Encode in YXML.string_of_body o list (pair string string) end
-          (("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv),
-        Value.print_bool redirect,
-        Value.print_real (Time.toReal timeout),
-        description];
+     [Bytes.string Bash.server_run,
+      Bytes.string script,
+      input,
+      let open XML.Encode in YXML.bytes_of_body (option (string o absolute_path) cwd) end,
+      let open XML.Encode in YXML.bytes_of_body o list (pair string string) end
+        (("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv),
+      Bytes.string (Value.print_bool redirect),
+      Bytes.string (Value.print_real (Time.toReal timeout)),
+      Bytes.string description];
 
     val address = Options.default_string \<^system_option>\<open>bash_process_address\<close>;
     val password = Options.default_string \<^system_option>\<open>bash_process_password\<close>;
@@ -93,7 +95,7 @@
             Exn.Res res => res
           | Exn.Exn exn => (kill maybe_uuid; Exn.reraise exn));
       in
-        with_streams (fn s => (Byte_Message.write_message_string (#2 s) server_run; loop NONE s))
+        with_streams (fn s => (Byte_Message.write_message (#2 s) server_run; loop NONE s))
       end)
   end;
 
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Pure/System/process_result.ML
--- a/src/Pure/System/process_result.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Pure/System/process_result.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -6,6 +6,7 @@
 
 signature PROCESS_RESULT =
 sig
+  val startup_failure_rc: int
   val interrupt_rc: int
   val timeout_rc: int
   type T
@@ -29,6 +30,7 @@
 structure Process_Result: PROCESS_RESULT =
 struct
 
+val startup_failure_rc = 127
 val interrupt_rc = 130
 val timeout_rc = 142
 
diff -r 50dd4fc40fcb -r 06dce439a4f0 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Thu Feb 06 14:46:49 2025 +0100
+++ b/src/Tools/cache_io.ML	Thu Feb 06 16:44:50 2025 +0100
@@ -6,58 +6,18 @@
 
 signature CACHE_IO =
 sig
-  (*IO wrapper*)
-  type result = {
-    output: string list,
-    redirected_output: string list,
-    return_code: int}
-  val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> result
-  val run: (Path.T -> Path.T -> string) -> string -> result
-
-  (*cache*)
   type cache
   val unsynchronized_init: Path.T -> cache
   val cache_path_of: cache -> Path.T
-  val lookup: cache -> string -> result option * string
-  val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> result
-  val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
+  val lookup: cache -> string -> Process_Result.T option * string
+  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-"
-
-type result = {
-  output: string list,
-  redirected_output: string list,
-  return_code: int}
-
-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 (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
-    val out1 = try_read_lines out_path
-  in {output = split_lines out2, redirected_output = out1, return_code = rc} 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 }
@@ -107,26 +67,47 @@
               else (i, xsp)
             val (out, err) =
               apply2 rev (snd (fold load (File.read_lines cache_path) (1, ([], []))))
-          in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
+            val result =
+              Process_Result.make {rc = 0, out_lines = out, err_lines = err, timing = Timing.zero}
+          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 {output = err, redirected_output=out, return_code} = run make_cmd str
-    val (l1, l2) = apply2 length (out, err)
+    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)
     val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
-    val lines = map (suffix "\n") (header :: out @ err)
+    val lines = map (suffix "\n") (header :: out_lines @ err_lines)
 
     val _ = Synchronized.change table (fn (p, tab) =>
       if Symtab.defined tab key then (p, tab)
       else
         let val _ = File.append_list cache_path lines
         in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
-  in {output = err, redirected_output = out, return_code = return_code} 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