--- 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,
--- 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
--- 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
--- 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
--- 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 {
--- 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)
--- 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) }
--- 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")) :::