--- a/Admin/jenkins/build/ci_build_benchmark.scala Thu Apr 06 21:10:35 2017 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala Thu Apr 06 22:04:30 2017 +0200
@@ -12,7 +12,7 @@
def pre_hook(args: List[String]) = {}
def post_hook(results: Build.Results) = {}
- def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
- tree.selection(session_groups = List("timing"))
+ def select_sessions(sessions: Sessions.T) =
+ sessions.selection(session_groups = List("timing"))
}
--- a/Admin/jenkins/build/ci_build_makeall.scala Thu Apr 06 21:10:35 2017 +0200
+++ b/Admin/jenkins/build/ci_build_makeall.scala Thu Apr 06 22:04:30 2017 +0200
@@ -11,7 +11,7 @@
def pre_hook(args: List[String]) = {}
def post_hook(results: Build.Results) = {}
- def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
- tree.selection(all_sessions = true)
+ def select_sessions(sessions: Sessions.T) =
+ sessions.selection(all_sessions = true)
}
--- a/Admin/jenkins/build/ci_build_makeall_seq.scala Thu Apr 06 21:10:35 2017 +0200
+++ b/Admin/jenkins/build/ci_build_makeall_seq.scala Thu Apr 06 22:04:30 2017 +0200
@@ -11,7 +11,7 @@
def pre_hook(args: List[String]) = {}
def post_hook(results: Build.Results) = {}
- def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
- tree.selection(all_sessions = true)
+ def select_sessions(sessions: Sessions.T) =
+ sessions.selection(all_sessions = true)
}
--- a/src/Pure/Admin/ci_profile.scala Thu Apr 06 21:10:35 2017 +0200
+++ b/src/Pure/Admin/ci_profile.scala Thu Apr 06 22:04:30 2017 +0200
@@ -146,5 +146,5 @@
def pre_hook(args: List[String]): Unit
def post_hook(results: Build.Results): Unit
- def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree)
+ def select_sessions(sessions: Sessions.T): (List[String], Sessions.T)
}
--- a/src/Pure/System/isabelle_process.scala Thu Apr 06 21:10:35 2017 +0200
+++ b/src/Pure/System/isabelle_process.scala Thu Apr 06 22:04:30 2017 +0200
@@ -20,7 +20,7 @@
modes: List[String] = Nil,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
- tree: Option[Sessions.Tree] = None,
+ sessions: Option[Sessions.T] = None,
store: Sessions.Store = Sessions.store(),
phase_changed: Session.Phase => Unit = null)
{
@@ -30,7 +30,7 @@
session.start(receiver =>
Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache,
- tree = tree, store = store))
+ sessions = sessions, store = store))
}
def apply(
@@ -43,14 +43,14 @@
env: Map[String, String] = Isabelle_System.settings(),
receiver: Prover.Receiver = Console.println(_),
xml_cache: XML.Cache = new XML.Cache(),
- tree: Option[Sessions.Tree] = None,
+ sessions: Option[Sessions.T] = None,
store: Sessions.Store = Sessions.store()): Prover =
{
val channel = System_Channel()
val process =
try {
ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
- cwd = cwd, env = env, tree = tree, store = store, channel = Some(channel))
+ cwd = cwd, env = env, sessions = sessions, store = store, channel = Some(channel))
}
catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
process.stdin.close
--- a/src/Pure/Thy/sessions.scala Thu Apr 06 21:10:35 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Apr 06 22:04:30 2017 +0200
@@ -49,7 +49,7 @@
def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2)
}
- def deps(tree: Tree,
+ def deps(sessions: T,
progress: Progress = No_Progress,
inlined_files: Boolean = false,
verbose: Boolean = false,
@@ -57,7 +57,8 @@
check_keywords: Set[String] = Set.empty,
global_theories: Set[String] = Set.empty): Deps =
{
- Deps((Map.empty[String, Base] /: tree.topological_order)({ case (sessions, (name, info)) =>
+ Deps((Map.empty[String, Base] /: sessions.topological_order)({
+ case (sessions, (name, info)) =>
if (progress.stopped) throw Exn.Interrupt()
try {
@@ -153,14 +154,14 @@
def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
{
- val full_tree = load(options, dirs = dirs)
- val (_, tree) = full_tree.selection(sessions = List(session))
+ val full_sessions = load(options, dirs = dirs)
+ val (_, selected_sessions) = full_sessions.selection(sessions = List(session))
- deps(tree, global_theories = full_tree.global_theories)(session)
+ deps(selected_sessions, global_theories = full_sessions.global_theories)(session)
}
- /* session tree */
+ /* cumulative session info */
sealed case class Info(
chapter: String,
@@ -180,44 +181,41 @@
def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
}
- object Tree
+ def make(infos: Traversable[(String, Info)]): T =
{
- def apply(infos: Traversable[(String, Info)]): Tree =
- {
- val graph1 =
- (Graph.string[Info] /: infos) {
- case (graph, (name, info)) =>
- if (graph.defined(name))
- error("Duplicate session " + quote(name) + Position.here(info.pos) +
- Position.here(graph.get_node(name).pos))
- else graph.new_node(name, info)
- }
- val graph2 =
- (graph1 /: graph1.iterator) {
- case (graph, (name, (info, _))) =>
- info.parent match {
- case None => graph
- case Some(parent) =>
- if (!graph.defined(parent))
- error("Bad parent session " + quote(parent) + " for " +
- quote(name) + Position.here(info.pos))
+ val graph1 =
+ (Graph.string[Info] /: infos) {
+ case (graph, (name, info)) =>
+ if (graph.defined(name))
+ error("Duplicate session " + quote(name) + Position.here(info.pos) +
+ Position.here(graph.get_node(name).pos))
+ else graph.new_node(name, info)
+ }
+ val graph2 =
+ (graph1 /: graph1.iterator) {
+ case (graph, (name, (info, _))) =>
+ info.parent match {
+ case None => graph
+ case Some(parent) =>
+ if (!graph.defined(parent))
+ error("Bad parent session " + quote(parent) + " for " +
+ quote(name) + Position.here(info.pos))
- try { graph.add_edge_acyclic(parent, name) }
- catch {
- case exn: Graph.Cycles[_] =>
- error(cat_lines(exn.cycles.map(cycle =>
- "Cyclic session dependency of " +
- cycle.map(c => quote(c.toString)).mkString(" via "))) +
- Position.here(info.pos))
- }
- }
- }
+ try { graph.add_edge_acyclic(parent, name) }
+ catch {
+ case exn: Graph.Cycles[_] =>
+ error(cat_lines(exn.cycles.map(cycle =>
+ "Cyclic session dependency of " +
+ cycle.map(c => quote(c.toString)).mkString(" via "))) +
+ Position.here(info.pos))
+ }
+ }
+ }
- new Tree(graph2)
- }
+ new T(graph2)
}
- final class Tree private(val graph: Graph[String, Info])
+ final class T private[Sessions](val graph: Graph[String, Info])
extends PartialFunction[String, Info]
{
def apply(name: String): Info = graph.get_node(name)
@@ -235,7 +233,7 @@
exclude_session_groups: List[String] = Nil,
exclude_sessions: List[String] = Nil,
session_groups: List[String] = Nil,
- sessions: List[String] = Nil): (List[String], Tree) =
+ sessions: List[String] = Nil): (List[String], T) =
{
val bad_sessions =
SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
@@ -270,7 +268,7 @@
else pre_selected
val graph1 = graph.restrict(graph.all_preds(selected).toSet)
- (selected, new Tree(graph1))
+ (selected, new T(graph1))
}
def ancestors(name: String): List[String] =
@@ -279,7 +277,7 @@
def topological_order: List[(String, Info)] =
graph.topological_order.map(name => (name, apply(name)))
- override def toString: String = graph.keys_iterator.mkString("Sessions.Tree(", ", ", ")")
+ override def toString: String = graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
}
@@ -450,7 +448,7 @@
if (is_session_dir(dir)) dir
else error("Bad session root directory: " + dir.toString)
- def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): Tree =
+ def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
{
def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
load_root(select, dir) ::: load_roots(select, dir)
@@ -481,7 +479,7 @@
dirs.foreach(check_session_dir(_))
select_dirs.foreach(check_session_dir(_))
- Tree(
+ make(
for {
(select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
info <- load_dir(select, dir)
--- a/src/Pure/Tools/build.scala Thu Apr 06 21:10:35 2017 +0200
+++ b/src/Pure/Tools/build.scala Thu Apr 06 22:04:30 2017 +0200
@@ -63,12 +63,12 @@
}
}
- def apply(tree: Sessions.Tree, store: Sessions.Store): Queue =
+ def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
{
- val graph = tree.graph
- val sessions = graph.keys
+ val graph = sessions.graph
+ val names = graph.keys
- val timings = sessions.map(name => (name, load_timings(store, name)))
+ val timings = names.map(name => (name, load_timings(store, name)))
val command_timings =
Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
val session_timing =
@@ -91,7 +91,7 @@
case 0 =>
compare_timing(name2, name1) match {
case 0 =>
- tree(name2).timeout compare tree(name1).timeout match {
+ sessions(name2).timeout compare sessions(name1).timeout match {
case 0 => name1 compare name2
case ord => ord
}
@@ -101,7 +101,7 @@
}
}
- new Queue(graph, SortedSet(sessions: _*)(Ordering), command_timings)
+ new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
}
}
@@ -170,7 +170,7 @@
private class Job(progress: Progress,
name: String,
val info: Sessions.Info,
- tree: Sessions.Tree,
+ sessions: Sessions.T,
deps: Sessions.Deps,
store: Sessions.Store,
do_output: Boolean,
@@ -228,7 +228,7 @@
val session_result = Future.promise[Process_Result]
Isabelle_Process.start(session, options, logic = parent,
- cwd = info.dir.file, env = env, tree = Some(tree), store = store,
+ cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
phase_changed =
{
case Session.Ready => session.protocol_command("build_session", args_yxml)
@@ -260,11 +260,13 @@
args =
(for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
List("--eval", eval),
- env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
+ env = env, sessions = Some(sessions), store = store,
+ cleanup = () => args_file.delete)
}
else {
ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
- env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
+ env = env, sessions = Some(sessions), store = store,
+ cleanup = () => args_file.delete)
}
process.result(
@@ -366,53 +368,53 @@
system_mode = system_mode,
verbose = verbose,
pide = pide,
- selection = { full_tree =>
- full_tree.selection(requirements, all_sessions,
+ selection = { full_sessions =>
+ full_sessions.selection(requirements, all_sessions,
exclude_session_groups, exclude_sessions, session_groups, sessions) })
}
def build_selection(
- options: Options,
- progress: Progress = No_Progress,
- build_heap: Boolean = false,
- clean_build: Boolean = false,
- dirs: List[Path] = Nil,
- select_dirs: List[Path] = Nil,
- numa_shuffling: Boolean = false,
- max_jobs: Int = 1,
- list_files: Boolean = false,
- check_keywords: Set[String] = Set.empty,
- no_build: Boolean = false,
- system_mode: Boolean = false,
- verbose: Boolean = false,
- pide: Boolean = false,
- selection: Sessions.Tree => (List[String], Sessions.Tree) =
- (_.selection(all_sessions = true))): Results =
+ options: Options,
+ progress: Progress = No_Progress,
+ build_heap: Boolean = false,
+ clean_build: Boolean = false,
+ dirs: List[Path] = Nil,
+ select_dirs: List[Path] = Nil,
+ numa_shuffling: Boolean = false,
+ max_jobs: Int = 1,
+ list_files: Boolean = false,
+ check_keywords: Set[String] = Set.empty,
+ no_build: Boolean = false,
+ system_mode: Boolean = false,
+ verbose: Boolean = false,
+ pide: Boolean = false,
+ selection: Sessions.T => (List[String], Sessions.T) = (_.selection(all_sessions = true))
+ ): Results =
{
/* session selection and dependencies */
val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
- val full_tree = Sessions.load(build_options, dirs, select_dirs)
- val (selected, selected_tree) = selection(full_tree)
+ val full_sessions = Sessions.load(build_options, dirs, select_dirs)
+ val (selected, selected_sessions) = selection(full_sessions)
val deps =
- Sessions.deps(selected_tree, progress = progress, inlined_files = true,
+ Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
verbose = verbose, list_files = list_files, check_keywords = check_keywords,
- global_theories = full_tree.global_theories)
+ global_theories = full_sessions.global_theories)
def sources_stamp(name: String): List[String] =
- (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
+ (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
/* main build process */
val store = Sessions.store(system_mode)
- val queue = Queue(selected_tree, store)
+ val queue = Queue(selected_sessions, store)
store.prepare_output()
// optional cleanup
if (clean_build) {
- for (name <- full_tree.graph.all_succs(selected)) {
+ for (name <- full_sessions.graph.all_succs(selected)) {
val files =
List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
map(store.output_dir + _).filter(_.is_file)
@@ -518,7 +520,7 @@
//{{{ check/start next job
pending.dequeue(running.isDefinedAt(_)) match {
case Some((name, info)) =>
- val ancestor_results = selected_tree.ancestors(name).map(results(_))
+ val ancestor_results = selected_sessions.ancestors(name).map(results(_))
val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
@@ -555,8 +557,8 @@
val numa_node = numa_nodes.next(used_node(_))
progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
val job =
- new Job(progress, name, info, selected_tree, deps, store, do_output, verbose,
- pide, numa_node, queue.command_timings(name))
+ new Job(progress, name, info, selected_sessions, deps, store, do_output,
+ verbose, pide, numa_node, queue.command_timings(name))
loop(pending, running + (name -> (ancestor_heaps, job)), results)
}
else {
@@ -604,7 +606,7 @@
(for {
(name, result) <- results0.iterator
if result.ok
- info = full_tree(name)
+ info = full_sessions(name)
if info.options.bool("browser_info")
} yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
--- a/src/Pure/Tools/ml_process.scala Thu Apr 06 21:10:35 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala Thu Apr 06 22:04:30 2017 +0200
@@ -23,16 +23,16 @@
redirect: Boolean = false,
cleanup: () => Unit = () => (),
channel: Option[System_Channel] = None,
- tree: Option[Sessions.Tree] = None,
+ sessions: Option[Sessions.T] = None,
store: Sessions.Store = Sessions.store()): Bash.Process =
{
val logic_name = Isabelle_System.default_logic(logic)
val heaps: List[String] =
if (raw_ml_system) Nil
else {
- val (_, session_tree) =
- tree.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
- (session_tree.ancestors(logic_name) ::: List(logic_name)).
+ val (_, selected_sessions) =
+ sessions.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
+ (selected_sessions.ancestors(logic_name) ::: List(logic_name)).
map(a => File.platform_path(store.heap(a)))
}