# HG changeset patch # User wenzelm # Date 1623008366 -7200 # Node ID c10fe904ac103eb2c638b50488b6072861321f94 # Parent 0510c7a4256a019f8d00866b924b0b64138bfe9e# Parent 1192c68ebe1c0f8d2603ae4651c947a4972cc9c8 merged diff -r 0510c7a4256a -r c10fe904ac10 etc/options --- 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)" diff -r 0510c7a4256a -r c10fe904ac10 src/HOL/ROOT --- 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 diff -r 0510c7a4256a -r c10fe904ac10 src/HOL/Tools/Mirabelle/mirabelle.ML --- 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>\mirabelle_timeout\; - val mirabelle_stride = Options.int options \<^system_option>\mirabelle_stride\; - val mirabelle_actions = Options.string options \<^system_option>\mirabelle_actions\; - val mirabelle_theories = Options.string options \<^system_option>\mirabelle_theories\; + val mirabelle_timeout = Options.default_seconds \<^system_option>\mirabelle_timeout\; + val mirabelle_stride = Options.default_int \<^system_option>\mirabelle_stride\; + val mirabelle_actions = Options.default_string \<^system_option>\mirabelle_actions\; + val mirabelle_theories = Options.default_string \<^system_option>\mirabelle_theories\; 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 *) diff -r 0510c7a4256a -r c10fe904ac10 src/HOL/Tools/Mirabelle/mirabelle.scala --- 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(",")) diff -r 0510c7a4256a -r c10fe904ac10 src/Pure/Thy/thy_info.ML --- 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>\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 ())); 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 *) diff -r 0510c7a4256a -r c10fe904ac10 src/Pure/Tools/build.ML --- 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 *)