# HG changeset patch # User wenzelm # Date 1623004192 -7200 # Node ID 9ead8d9be3ab30597535e01eed3f52e66f25c66b # Parent 745e2cd1f5f5db522c82bc623155b3ff8a5b4d2e clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT); diff -r 745e2cd1f5f5 -r 9ead8d9be3ab etc/options --- a/etc/options Sun Jun 06 16:34:57 2021 +0200 +++ b/etc/options Sun Jun 06 20:29:52 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)" diff -r 745e2cd1f5f5 -r 9ead8d9be3ab src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Jun 06 16:34:57 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Jun 06 20:29:52 2021 +0200 @@ -153,7 +153,7 @@ val whitelist = ["apply", "by", "proof"]; val _ = - Theory.setup (Thy_Info.add_presentation (fn {segments, ...} => fn thy => + Build.add_hook (fn loaded_theories => let val mirabelle_timeout = Options.default_seconds \<^system_option>\mirabelle_timeout\; val mirabelle_stride = Options.default_int \<^system_option>\mirabelle_stride\; @@ -165,26 +165,33 @@ 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 = 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; - 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 *) diff -r 745e2cd1f5f5 -r 9ead8d9be3ab src/HOL/Tools/Mirabelle/mirabelle.scala --- a/src/HOL/Tools/Mirabelle/mirabelle.scala Sun Jun 06 16:34:57 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Sun Jun 06 20:29:52 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(",")) diff -r 745e2cd1f5f5 -r 9ead8d9be3ab src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Jun 06 16:34:57 2021 +0200 +++ b/src/Pure/Thy/thy_info.ML Sun Jun 06 20:29:52 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,14 +48,8 @@ fun merge data : T = Library.merge (eq_snd op =) data; ); -fun sequential_presentation options = - not (Options.bool options \<^system_option>\parallel_presentation\); - 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 ())); @@ -186,14 +181,20 @@ (* 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 consolidate_theory (Exn.Exn exn) = [Exn.Exn exn] @@ -204,6 +205,14 @@ 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; @@ -231,18 +240,16 @@ 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) ()) ()); val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); - in ignore (Par_Exn.release_all (results1 @ results2 @ results3 @ results4)) end); + val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); + in Par_Exn.release_all present_results end); (* eval theory *) @@ -284,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; @@ -339,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 @@ -412,7 +417,7 @@ 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 *) diff -r 745e2cd1f5f5 -r 9ead8d9be3ab src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Sun Jun 06 16:34:57 2021 +0200 +++ b/src/Pure/Tools/build.ML Sun Jun 06 20:29:52 2021 +0200 @@ -4,7 +4,12 @@ Build Isabelle sessions. *) -structure Build: sig end = +signature BUILD = +sig + val add_hook: ((theory * Document_Output.segment list) list -> unit) -> unit +end; + +structure Build: BUILD = struct (* session timing *) @@ -23,28 +28,43 @@ (* build theories *) +local + val hooks = + Synchronized.var "Build.hooks" + ([]: ((theory * Document_Output.segment list) list -> unit) list); +in + +fun add_hook hook = Synchronized.change hooks (cons hook); + +fun apply_hooks loaded_theories = + Synchronized.value hooks + |> List.app (fn hook => hook 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 loaded_theories end; (* build session *)