--- a/etc/options Sun Jun 06 15:49:39 2021 +0000
+++ b/etc/options Sun Jun 06 21:39:26 2021 +0200
@@ -91,8 +91,6 @@
-- "level of parallel proof checking: 0, 1, 2"
option parallel_subproofs_threshold : real = 0.01
-- "lower bound of timing estimate for forked nested proofs (seconds)"
-option parallel_presentation : bool = true
- -- "parallel theory presentation"
option command_timing_threshold : real = 0.1
-- "default threshold for persistent command timing (seconds)"
--- a/src/HOL/ROOT Sun Jun 06 15:49:39 2021 +0000
+++ b/src/HOL/ROOT Sun Jun 06 21:39:26 2021 +0200
@@ -939,7 +939,8 @@
session "HOL-Mirabelle-ex" in "Tools/Mirabelle" = HOL +
description "Some arbitrary small test case for Mirabelle."
- options [timeout = 60, mirabelle_actions = "arith"]
+ options [timeout = 60,
+ mirabelle_theories = "HOL-Analysis.Inner_Product", mirabelle_actions = "arith"]
sessions
"HOL-Analysis"
theories
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Jun 06 15:49:39 2021 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Jun 06 21:39:26 2021 +0200
@@ -147,45 +147,56 @@
fun check_pos range = check_line range o Position.line_of;
in check_pos o get_theory end;
+fun check_session qualifier thy_name (_: Position.T) =
+ Resources.theory_qualifier thy_name = qualifier;
+
(* presentation hook *)
val whitelist = ["apply", "by", "proof"];
val _ =
- Theory.setup (Thy_Info.add_presentation (fn context => fn thy =>
+ Build.add_hook (fn qualifier => fn loaded_theories =>
let
- val {options, adjust_pos, segments, ...} = context;
- val mirabelle_timeout = Options.seconds options \<^system_option>\<open>mirabelle_timeout\<close>;
- val mirabelle_stride = Options.int options \<^system_option>\<open>mirabelle_stride\<close>;
- val mirabelle_actions = Options.string options \<^system_option>\<open>mirabelle_actions\<close>;
- val mirabelle_theories = Options.string options \<^system_option>\<open>mirabelle_theories\<close>;
+ val mirabelle_timeout = Options.default_seconds \<^system_option>\<open>mirabelle_timeout\<close>;
+ val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>;
+ val mirabelle_actions = Options.default_string \<^system_option>\<open>mirabelle_actions\<close>;
+ val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>;
val actions =
(case read_actions mirabelle_actions of
SOME actions => actions
| NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions));
- val check = check_theories (space_explode "," mirabelle_theories);
- val commands =
- segments
- |> map_index (fn (n, {command = tr, prev_state = st, state = st', ...}) =>
- if n mod mirabelle_stride = 0 then
- let
- val name = Toplevel.name_of tr;
- val pos = adjust_pos (Toplevel.pos_of tr);
- in
- if can (Proof.assert_backward o Toplevel.proof_of) st andalso
- member (op =) whitelist name andalso
- check (Context.theory_long_name thy) pos
- then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'}
- else NONE
- end
- else NONE)
- |> map_filter I;
+ val check =
+ if mirabelle_theories = "" then check_session qualifier
+ else check_theories (space_explode "," mirabelle_theories);
- fun apply (i, (name, arguments)) () =
- apply_action (i + 1) name arguments mirabelle_timeout commands thy;
- in if null commands then () else fold_index apply actions () end));
+ fun theory_commands (thy, segments) =
+ let
+ val commands = segments
+ |> map_index (fn (n, {command = tr, prev_state = st, state = st', ...}) =>
+ if n mod mirabelle_stride = 0 then
+ let
+ val name = Toplevel.name_of tr;
+ val pos = Toplevel.pos_of tr;
+ in
+ if can (Proof.assert_backward o Toplevel.proof_of) st andalso
+ member (op =) whitelist name andalso
+ check (Context.theory_long_name thy) pos
+ then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'}
+ else NONE
+ end
+ else NONE)
+ |> map_filter I;
+ in if null commands then NONE else SOME (thy, commands) end;
+
+ fun app_actions (thy, commands) =
+ (actions, ()) |-> fold_index (fn (index, (name, arguments)) => fn () =>
+ apply_action (index + 1) name arguments mirabelle_timeout commands thy);
+ in
+ if null actions then ()
+ else List.app app_actions (map_filter theory_commands loaded_theories)
+ end);
(* Mirabelle utility functions *)
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Sun Jun 06 15:49:39 2021 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Sun Jun 06 21:39:26 2021 +0200
@@ -102,7 +102,7 @@
if (build_results0.ok) {
val build_options =
- options + "timeout_build=false" + "parallel_presentation=false" +
+ options + "timeout_build=false" +
("mirabelle_actions=" + actions.mkString(";")) +
("mirabelle_theories=" + theories.mkString(","))
--- a/src/Pure/Thy/thy_info.ML Sun Jun 06 15:49:39 2021 +0000
+++ b/src/Pure/Thy/thy_info.ML Sun Jun 06 21:39:26 2021 +0200
@@ -18,7 +18,8 @@
val get_theory: string -> theory
val master_directory: string -> Path.T
val remove_thy: string -> unit
- val use_theories: Options.T -> string -> (string * Position.T) list -> unit
+ val use_theories: Options.T -> string -> (string * Position.T) list ->
+ (theory * Document_Output.segment list) list
val use_thy: string -> unit
val script_thy: Position.T -> string -> theory -> theory
val register_thy: theory -> unit
@@ -47,19 +48,13 @@
fun merge data : T = Library.merge (eq_snd op =) data;
);
-fun sequential_presentation options =
- not (Options.bool options \<^system_option>\<open>parallel_presentation\<close>);
-
fun apply_presentation (context: presentation_context) thy =
- Par_List.map'
- {name = "apply_presentation", sequential = sequential_presentation (#options context)}
- (fn (f, _) => f context thy) (Presentation.get thy)
- |> ignore;
+ ignore (Par_List.map (fn (f, _) => f context thy) (Presentation.get thy));
fun add_presentation f = Presentation.map (cons (f, stamp ()));
val _ =
- Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
+ Theory.setup (add_presentation (fn {options, segments, ...} => fn thy =>
if exists (Toplevel.is_skipped_proof o #state) segments then ()
else
let
@@ -186,82 +181,75 @@
(* scheduling loader tasks *)
datatype result =
- Result of {theory: theory, exec_id: Document_ID.exec,
- present: (unit -> unit) option, commit: unit -> unit};
+ Result of
+ {theory: theory,
+ exec_id: Document_ID.exec,
+ present: unit -> presentation_context option,
+ commit: unit -> unit};
fun theory_result theory =
- Result {theory = theory, exec_id = Document_ID.none, present = NONE, commit = I};
+ Result
+ {theory = theory,
+ exec_id = Document_ID.none,
+ present = K NONE,
+ commit = I};
fun result_theory (Result {theory, ...}) = theory;
-fun result_present (Result {present, ...}) = present;
fun result_commit (Result {commit, ...}) = commit;
-fun join_theory (Result {theory, exec_id, ...}) =
- let
- val _ = Execution.join [exec_id];
- val res = Exn.capture Thm.consolidate_theory theory;
- val exns = maps Task_Queue.group_status (Execution.peek exec_id);
- in res :: map Exn.Exn exns end;
+fun consolidate_theory (Exn.Exn exn) = [Exn.Exn exn]
+ | consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) =
+ let
+ val _ = Execution.join [exec_id];
+ val res = Exn.capture Thm.consolidate_theory theory;
+ val exns = maps Task_Queue.group_status (Execution.peek exec_id);
+ in res :: map Exn.Exn exns end;
+
+fun present_theory (Exn.Exn exn) = [Exn.Exn exn]
+ | present_theory (Exn.Res (Result {theory, present, ...})) =
+ (case present () of
+ NONE => []
+ | SOME (context as {segments, ...}) =>
+ [Exn.capture (fn () => (apply_presentation context theory; (theory, segments))) ()]);
+
datatype task =
Task of string list * (theory list -> result) |
Finished of theory;
-fun task_finished (Task _) = false
- | task_finished (Finished _) = true;
-
-fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
+val schedule_theories = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
+ let
+ fun join_parents deps name parents =
+ (case map #1 (filter (not o can Future.join o #2) deps) of
+ [] => map (result_theory o Future.join o the o AList.lookup (op =) deps) parents
+ | bad =>
+ error ("Failed to load theory " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")"));
-val schedule_seq =
- String_Graph.schedule (fn deps => fn (_, task) =>
- (case task of
- Task (parents, body) =>
- let
- val result = body (task_parents deps parents);
- val _ = Par_Exn.release_all (join_theory result);
- val _ = (case result_present result of NONE => () | SOME present => present ());
- val _ = result_commit result ();
- in result_theory result end
- | Finished thy => thy)) #> ignore;
-
-val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
- let
val futures = tasks
|> String_Graph.schedule (fn deps => fn (name, task) =>
(case task of
Task (parents, body) =>
- (singleton o Future.forks)
- {name = "theory:" ^ name, group = NONE,
- deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
- (fn () =>
- (case filter (not o can Future.join o #2) deps of
- [] => body (map (result_theory o Future.join) (task_parents deps parents))
- | bad =>
- error
- ("Failed to load theory " ^ quote name ^
- " (unresolved " ^ commas_quote (map #1 bad) ^ ")")))
+ if Multithreading.max_threads () > 1 then
+ (singleton o Future.forks)
+ {name = "theory:" ^ name, group = NONE,
+ deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
+ (fn () => body (join_parents deps name parents))
+ else
+ Future.value_result (Exn.capture (fn () => body (join_parents deps name parents)) ())
| Finished theory => Future.value (theory_result theory)));
- val results1 = futures
- |> maps (fn future =>
- (case Future.join_result future of
- Exn.Res result => join_theory result
- | Exn.Exn exn => [Exn.Exn exn]));
+ val results1 = futures |> maps (consolidate_theory o Future.join_result);
- val results2 = futures
- |> map_filter (Option.mapPartial result_present o Exn.get_res o Future.join_result)
- |> Par_List.map'
- {name = "present", sequential = sequential_presentation (Options.default ())}
- (fn present => Exn.capture present ());
+ val present_results = futures |> maps (present_theory o Future.join_result);
+ val results2 = (map o Exn.map_res) (K ()) present_results;
val results3 = futures
|> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
- (* FIXME avoid global Execution.reset (!??) *)
val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
- in () end);
+ in Par_Exn.release_all present_results end);
(* eval theory *)
@@ -303,14 +291,12 @@
val (results, thy) = cond_timeit true ("theory " ^ quote name) excursion;
- fun present () =
+ fun present () : presentation_context =
let
val segments =
(spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) =>
{span = span, prev_state = st, command = tr, state = st'});
- val context: presentation_context =
- {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
- in apply_presentation context thy end;
+ in {options = options, file_pos = text_pos, adjust_pos = I, segments = segments} end;
in (thy, present) end;
@@ -358,7 +344,7 @@
val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
fun commit () = update_thy deps theory;
- in Result {theory = theory, exec_id = exec_id, present = SOME present, commit = commit} end;
+ in Result {theory = theory, exec_id = exec_id, present = SOME o present, commit = commit} end;
fun check_thy_deps dir name =
(case lookup_deps name of
@@ -378,6 +364,9 @@
| SOME theory => Resources.loaded_files_current theory);
in (current, deps', theory_pos', imports', keywords') end);
+fun task_finished (Task _) = false
+ | task_finished (Finished _) = true;
+
in
fun require_thys options initiators qualifier dir strs tasks =
@@ -425,11 +414,10 @@
(* use theories *)
fun use_theories options qualifier imports =
- let val (_, tasks) = require_thys options [] qualifier Path.current imports String_Graph.empty
- in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
+ schedule_theories (#2 (require_thys options [] qualifier Path.current imports String_Graph.empty));
fun use_thy name =
- use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)];
+ ignore (use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)]);
(* toplevel scripting -- without maintaining database *)
--- a/src/Pure/Tools/build.ML Sun Jun 06 15:49:39 2021 +0000
+++ b/src/Pure/Tools/build.ML Sun Jun 06 21:39:26 2021 +0200
@@ -4,7 +4,13 @@
Build Isabelle sessions.
*)
-structure Build: sig end =
+signature BUILD =
+sig
+ type hook = string -> (theory * Document_Output.segment list) list -> unit
+ val add_hook: hook -> unit
+end;
+
+structure Build: BUILD =
struct
(* session timing *)
@@ -23,28 +29,43 @@
(* build theories *)
+type hook = string -> (theory * Document_Output.segment list) list -> unit;
+
+local
+ val hooks = Synchronized.var "Build.hooks" ([]: hook list);
+in
+
+fun add_hook hook = Synchronized.change hooks (cons hook);
+
+fun apply_hooks qualifier loaded_theories =
+ Synchronized.value hooks
+ |> List.app (fn hook => hook qualifier loaded_theories);
+
+end;
+
+
fun build_theories qualifier (options, thys) =
let
val condition = space_explode "," (Options.string options "condition");
val conds = filter_out (can getenv_strict) condition;
- in
- if null conds then
- (Options.set_default options;
- Isabelle_Process.init_options ();
- Future.fork I;
- (Thy_Info.use_theories options qualifier
- |>
- (case Options.string options "profiling" of
- "" => I
- | "time" => profile_time
- | "allocations" => profile_allocations
- | bad => error ("Bad profiling option: " ^ quote bad))
- |> Unsynchronized.setmp print_mode
- (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
- else
- Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
- " (undefined " ^ commas conds ^ ")\n")
- end;
+ val loaded_theories =
+ if null conds then
+ (Options.set_default options;
+ Isabelle_Process.init_options ();
+ Future.fork I;
+ (Thy_Info.use_theories options qualifier
+ |>
+ (case Options.string options "profiling" of
+ "" => I
+ | "time" => profile_time
+ | "allocations" => profile_allocations
+ | bad => error ("Bad profiling option: " ^ quote bad))
+ |> Unsynchronized.setmp print_mode
+ (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
+ else
+ (Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
+ " (undefined " ^ commas conds ^ ")\n"); [])
+ in apply_hooks qualifier loaded_theories end;
(* build session *)