# HG changeset patch # User wenzelm # Date 1622842647 -7200 # Node ID b982362eeca436edaffb747659bbc96419e50d59 # Parent f7ea394490f5a88021ae3f696974530e070d62b5# Parent b73777a0c076fcc48fff49b62815e81ad17955c9 merged, resolving minor conflict; diff -r f7ea394490f5 -r b982362eeca4 src/HOL/Tools/Mirabelle/mirabelle.scala --- a/src/HOL/Tools/Mirabelle/mirabelle.scala Fri Jun 04 23:03:12 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Fri Jun 04 23:37:27 2021 +0200 @@ -161,7 +161,6 @@ var select_dirs: List[Path] = Nil var numa_shuffling = false var output_dir = default_output_dir - var requirements = false var theories: List[String] = Nil var exclude_session_groups: List[String] = Nil var all_sessions = false @@ -183,8 +182,7 @@ -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) - -O DIR output directory for log files (default: """ + default_output_dir + """) - -R refer to requirements of selected sessions + -O DIR output directory for log files (default: """ + default_output_dir + """, -T THEORY theory restriction: NAME or NAME[LINE:END_LINE] -X NAME exclude sessions from group NAME and all descendants -a select all sessions @@ -215,7 +213,6 @@ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), "O:" -> (arg => output_dir = Path.explode(arg)), - "R" -> (_ => requirements = true), "T:" -> (arg => theories = theories ::: List(arg)), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), @@ -244,7 +241,6 @@ mirabelle(options, actions, output_dir, theories = theories, selection = Sessions.Selection( - requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, diff -r f7ea394490f5 -r b982362eeca4 src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Fri Jun 04 23:03:12 2021 +0200 +++ b/src/Pure/PIDE/headless.scala Fri Jun 04 23:37:27 2021 +0200 @@ -574,7 +574,7 @@ val session = new Session(session_base_info.session, options, resources) progress.echo("Starting session " + session_base_info.session + " ...") - Isabelle_Process(session, options, session_base_info.sessions_structure, store, + Isabelle_Process.start(session, options, session_base_info.sessions_structure, store, logic = session_base_info.session, modes = print_mode).await_startup() session diff -r f7ea394490f5 -r b982362eeca4 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Fri Jun 04 23:03:12 2021 +0200 +++ b/src/Pure/System/isabelle_process.scala Fri Jun 04 23:37:27 2021 +0200 @@ -12,7 +12,7 @@ object Isabelle_Process { - def apply( + def start( session: Session, options: Options, sessions_structure: Sessions.Structure, @@ -37,13 +37,16 @@ modes = modes, cwd = cwd, env = env) } catch { case exn @ ERROR(_) => channel.shutdown(); throw exn } - process.stdin.close() - new Isabelle_Process(session, channel, process) + val isabelle_process = new Isabelle_Process(session, process) + process.stdin.close() + session.start(receiver => new Prover(receiver, session.cache, channel, process)) + + isabelle_process } } -class Isabelle_Process private(session: Session, channel: System_Channel, process: Bash.Process) +class Isabelle_Process private(session: Session, process: Bash.Process) { private val startup = Future.promise[String] private val terminated = Future.promise[Process_Result] @@ -62,8 +65,6 @@ case _ => } - session.start(receiver => new Prover(receiver, session.cache, channel, process)) - def await_startup(): Isabelle_Process = startup.join match { case "" => this diff -r f7ea394490f5 -r b982362eeca4 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Jun 04 23:03:12 2021 +0200 +++ b/src/Pure/Thy/thy_info.ML Fri Jun 04 23:37:27 2021 +0200 @@ -187,15 +187,14 @@ datatype result = Result of {theory: theory, exec_id: Document_ID.exec, - present: unit -> unit, commit: unit -> unit, weight: int}; + present: (unit -> unit) option, commit: unit -> unit}; fun theory_result theory = - Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; + Result {theory = theory, exec_id = Document_ID.none, present = NONE, commit = I}; fun result_theory (Result {theory, ...}) = theory; fun result_present (Result {present, ...}) = present; fun result_commit (Result {commit, ...}) = commit; -fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); fun join_theory (Result {theory, exec_id, ...}) = let @@ -220,7 +219,7 @@ let val result = body (task_parents deps parents); val _ = Par_Exn.release_all (join_theory result); - val _ = result_present result (); + val _ = (case result_present result of NONE => () | SOME present => present ()); val _ = result_commit result (); in result_theory result end | Finished thy => thy)) #> ignore; @@ -250,13 +249,11 @@ | Exn.Exn exn => [Exn.Exn exn])); val results2 = futures - |> map_filter (Exn.get_res o Future.join_result) - |> sort result_ord + |> 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 result => Exn.capture (result_present result) ()); + (fn present => Exn.capture present ()); - (* FIXME more precise commit order (!?) *) val results3 = futures |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); @@ -315,7 +312,7 @@ {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; in apply_presentation context thy end; - in (thy, present, size text) end; + in (thy, present) end; (* require_thy -- checking database entries wrt. the file-system *) @@ -352,7 +349,7 @@ val timing_start = Timing.start (); val header = Thy_Header.make (name, put_id header_pos) imports keywords; - val (theory, present, weight) = + val (theory, present) = eval_thy options dir header text_pos text (if name = Context.PureN then [Context.the_global_context ()] else parents); @@ -361,9 +358,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 = present, commit = commit, weight = weight} - end; + in Result {theory = theory, exec_id = exec_id, present = SOME present, commit = commit} end; fun check_thy_deps dir name = (case lookup_deps name of diff -r f7ea394490f5 -r b982362eeca4 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Jun 04 23:03:12 2021 +0200 +++ b/src/Pure/Tools/build.scala Fri Jun 04 23:37:27 2021 +0200 @@ -183,7 +183,8 @@ no_build: Boolean = false, soft_build: Boolean = false, verbose: Boolean = false, - export_files: Boolean = false): Results = + export_files: Boolean = false, + session_setup: (String, Session) => Unit = (_, _) => ()): Results = { val build_options = options + @@ -425,7 +426,7 @@ val numa_node = numa_nodes.next(used_node) val job = new Build_Job(progress, session_name, info, deps, store, do_store, - verbose, log, numa_node, queue.command_timings(session_name)) + log, session_setup, numa_node, queue.command_timings(session_name)) loop(pending, running + (session_name -> (ancestor_heaps, job)), results) } else { diff -r f7ea394490f5 -r b982362eeca4 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Fri Jun 04 23:03:12 2021 +0200 +++ b/src/Pure/Tools/build_job.scala Fri Jun 04 23:37:27 2021 +0200 @@ -202,8 +202,8 @@ deps: Sessions.Deps, store: Sessions.Store, do_store: Boolean, - verbose: Boolean, log: Logger, + session_setup: (String, Session) => Unit, val numa_node: Option[Int], command_timings0: List[Properties.T]) { @@ -411,10 +411,12 @@ case _ => } + session_setup(session_name, session) + val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) val process = - Isabelle_Process(session, options, sessions_structure, store, + Isabelle_Process.start(session, options, sessions_structure, store, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) diff -r f7ea394490f5 -r b982362eeca4 src/Tools/VSCode/src/language_server.scala --- a/src/Tools/VSCode/src/language_server.scala Fri Jun 04 23:03:12 2021 +0200 +++ b/src/Tools/VSCode/src/language_server.scala Fri Jun 04 23:37:27 2021 +0200 @@ -306,8 +306,8 @@ dynamic_output.init() try { - Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options), - modes = modes, logic = base_info.session).await_startup() + Isabelle_Process.start(session, options, base_info.sessions_structure, + Sessions.store(options), modes = modes, logic = base_info.session).await_startup() reply_ok("Welcome to Isabelle/" + base_info.session + Isabelle_System.isabelle_heading()) } catch { case ERROR(msg) => reply_error(msg) } diff -r f7ea394490f5 -r b982362eeca4 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Jun 04 23:03:12 2021 +0200 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Jun 04 23:37:27 2021 +0200 @@ -143,7 +143,7 @@ session.phase_changed += PIDE.plugin.session_phase_changed - Isabelle_Process(session, options, sessions_structure, store, + Isabelle_Process.start(session, options, sessions_structure, store, logic = PIDE.resources.session_name, modes = (space_explode(',', options.string("jedit_print_mode")) :::