--- 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
--- 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
--- 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
--- 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 =
--- 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;
--- 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 *)
--- 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;
--- 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
--- 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;
--- 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
--- 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);
--- 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";
--- 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) =>
--- 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;
--- 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
--- 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