clarified signature: tree structure is not essential;
authorwenzelm
Thu Apr 06 22:04:30 2017 +0200 (2017-04-06)
changeset 654158cd54b18b68b
parent 65414 d7ebd2b25b82
child 65416 f707dbcf11e3
clarified signature: tree structure is not essential;
Admin/jenkins/build/ci_build_benchmark.scala
Admin/jenkins/build/ci_build_makeall.scala
Admin/jenkins/build/ci_build_makeall_seq.scala
src/Pure/Admin/ci_profile.scala
src/Pure/System/isabelle_process.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/Admin/jenkins/build/ci_build_benchmark.scala	Thu Apr 06 21:10:35 2017 +0200
     1.2 +++ b/Admin/jenkins/build/ci_build_benchmark.scala	Thu Apr 06 22:04:30 2017 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    def pre_hook(args: List[String]) = {}
     1.5    def post_hook(results: Build.Results) = {}
     1.6  
     1.7 -  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
     1.8 -    tree.selection(session_groups = List("timing"))
     1.9 +  def select_sessions(sessions: Sessions.T) =
    1.10 +    sessions.selection(session_groups = List("timing"))
    1.11  
    1.12  }
     2.1 --- a/Admin/jenkins/build/ci_build_makeall.scala	Thu Apr 06 21:10:35 2017 +0200
     2.2 +++ b/Admin/jenkins/build/ci_build_makeall.scala	Thu Apr 06 22:04:30 2017 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4    def pre_hook(args: List[String]) = {}
     2.5    def post_hook(results: Build.Results) = {}
     2.6  
     2.7 -  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
     2.8 -    tree.selection(all_sessions = true)
     2.9 +  def select_sessions(sessions: Sessions.T) =
    2.10 +    sessions.selection(all_sessions = true)
    2.11  
    2.12  }
     3.1 --- a/Admin/jenkins/build/ci_build_makeall_seq.scala	Thu Apr 06 21:10:35 2017 +0200
     3.2 +++ b/Admin/jenkins/build/ci_build_makeall_seq.scala	Thu Apr 06 22:04:30 2017 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4    def pre_hook(args: List[String]) = {}
     3.5    def post_hook(results: Build.Results) = {}
     3.6  
     3.7 -  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
     3.8 -    tree.selection(all_sessions = true)
     3.9 +  def select_sessions(sessions: Sessions.T) =
    3.10 +    sessions.selection(all_sessions = true)
    3.11  
    3.12  }
     4.1 --- a/src/Pure/Admin/ci_profile.scala	Thu Apr 06 21:10:35 2017 +0200
     4.2 +++ b/src/Pure/Admin/ci_profile.scala	Thu Apr 06 22:04:30 2017 +0200
     4.3 @@ -146,5 +146,5 @@
     4.4    def pre_hook(args: List[String]): Unit
     4.5    def post_hook(results: Build.Results): Unit
     4.6  
     4.7 -  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree)
     4.8 +  def select_sessions(sessions: Sessions.T): (List[String], Sessions.T)
     4.9  }
     5.1 --- a/src/Pure/System/isabelle_process.scala	Thu Apr 06 21:10:35 2017 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Apr 06 22:04:30 2017 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4      modes: List[String] = Nil,
     5.5      cwd: JFile = null,
     5.6      env: Map[String, String] = Isabelle_System.settings(),
     5.7 -    tree: Option[Sessions.Tree] = None,
     5.8 +    sessions: Option[Sessions.T] = None,
     5.9      store: Sessions.Store = Sessions.store(),
    5.10      phase_changed: Session.Phase => Unit = null)
    5.11    {
    5.12 @@ -30,7 +30,7 @@
    5.13      session.start(receiver =>
    5.14        Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
    5.15          cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache,
    5.16 -        tree = tree, store = store))
    5.17 +        sessions = sessions, store = store))
    5.18    }
    5.19  
    5.20    def apply(
    5.21 @@ -43,14 +43,14 @@
    5.22      env: Map[String, String] = Isabelle_System.settings(),
    5.23      receiver: Prover.Receiver = Console.println(_),
    5.24      xml_cache: XML.Cache = new XML.Cache(),
    5.25 -    tree: Option[Sessions.Tree] = None,
    5.26 +    sessions: Option[Sessions.T] = None,
    5.27      store: Sessions.Store = Sessions.store()): Prover =
    5.28    {
    5.29      val channel = System_Channel()
    5.30      val process =
    5.31        try {
    5.32          ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
    5.33 -          cwd = cwd, env = env, tree = tree, store = store, channel = Some(channel))
    5.34 +          cwd = cwd, env = env, sessions = sessions, store = store, channel = Some(channel))
    5.35        }
    5.36        catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
    5.37      process.stdin.close
     6.1 --- a/src/Pure/Thy/sessions.scala	Thu Apr 06 21:10:35 2017 +0200
     6.2 +++ b/src/Pure/Thy/sessions.scala	Thu Apr 06 22:04:30 2017 +0200
     6.3 @@ -49,7 +49,7 @@
     6.4      def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2)
     6.5    }
     6.6  
     6.7 -  def deps(tree: Tree,
     6.8 +  def deps(sessions: T,
     6.9        progress: Progress = No_Progress,
    6.10        inlined_files: Boolean = false,
    6.11        verbose: Boolean = false,
    6.12 @@ -57,7 +57,8 @@
    6.13        check_keywords: Set[String] = Set.empty,
    6.14        global_theories: Set[String] = Set.empty): Deps =
    6.15    {
    6.16 -    Deps((Map.empty[String, Base] /: tree.topological_order)({ case (sessions, (name, info)) =>
    6.17 +    Deps((Map.empty[String, Base] /: sessions.topological_order)({
    6.18 +      case (sessions, (name, info)) =>
    6.19          if (progress.stopped) throw Exn.Interrupt()
    6.20  
    6.21          try {
    6.22 @@ -153,14 +154,14 @@
    6.23  
    6.24    def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
    6.25    {
    6.26 -    val full_tree = load(options, dirs = dirs)
    6.27 -    val (_, tree) = full_tree.selection(sessions = List(session))
    6.28 +    val full_sessions = load(options, dirs = dirs)
    6.29 +    val (_, selected_sessions) = full_sessions.selection(sessions = List(session))
    6.30  
    6.31 -    deps(tree, global_theories = full_tree.global_theories)(session)
    6.32 +    deps(selected_sessions, global_theories = full_sessions.global_theories)(session)
    6.33    }
    6.34  
    6.35  
    6.36 -  /* session tree */
    6.37 +  /* cumulative session info */
    6.38  
    6.39    sealed case class Info(
    6.40      chapter: String,
    6.41 @@ -180,44 +181,41 @@
    6.42      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    6.43    }
    6.44  
    6.45 -  object Tree
    6.46 +  def make(infos: Traversable[(String, Info)]): T =
    6.47    {
    6.48 -    def apply(infos: Traversable[(String, Info)]): Tree =
    6.49 -    {
    6.50 -      val graph1 =
    6.51 -        (Graph.string[Info] /: infos) {
    6.52 -          case (graph, (name, info)) =>
    6.53 -            if (graph.defined(name))
    6.54 -              error("Duplicate session " + quote(name) + Position.here(info.pos) +
    6.55 -                Position.here(graph.get_node(name).pos))
    6.56 -            else graph.new_node(name, info)
    6.57 -        }
    6.58 -      val graph2 =
    6.59 -        (graph1 /: graph1.iterator) {
    6.60 -          case (graph, (name, (info, _))) =>
    6.61 -            info.parent match {
    6.62 -              case None => graph
    6.63 -              case Some(parent) =>
    6.64 -                if (!graph.defined(parent))
    6.65 -                  error("Bad parent session " + quote(parent) + " for " +
    6.66 -                    quote(name) + Position.here(info.pos))
    6.67 +    val graph1 =
    6.68 +      (Graph.string[Info] /: infos) {
    6.69 +        case (graph, (name, info)) =>
    6.70 +          if (graph.defined(name))
    6.71 +            error("Duplicate session " + quote(name) + Position.here(info.pos) +
    6.72 +              Position.here(graph.get_node(name).pos))
    6.73 +          else graph.new_node(name, info)
    6.74 +      }
    6.75 +    val graph2 =
    6.76 +      (graph1 /: graph1.iterator) {
    6.77 +        case (graph, (name, (info, _))) =>
    6.78 +          info.parent match {
    6.79 +            case None => graph
    6.80 +            case Some(parent) =>
    6.81 +              if (!graph.defined(parent))
    6.82 +                error("Bad parent session " + quote(parent) + " for " +
    6.83 +                  quote(name) + Position.here(info.pos))
    6.84  
    6.85 -                try { graph.add_edge_acyclic(parent, name) }
    6.86 -                catch {
    6.87 -                  case exn: Graph.Cycles[_] =>
    6.88 -                    error(cat_lines(exn.cycles.map(cycle =>
    6.89 -                      "Cyclic session dependency of " +
    6.90 -                        cycle.map(c => quote(c.toString)).mkString(" via "))) +
    6.91 -                          Position.here(info.pos))
    6.92 -                }
    6.93 -            }
    6.94 -        }
    6.95 +              try { graph.add_edge_acyclic(parent, name) }
    6.96 +              catch {
    6.97 +                case exn: Graph.Cycles[_] =>
    6.98 +                  error(cat_lines(exn.cycles.map(cycle =>
    6.99 +                    "Cyclic session dependency of " +
   6.100 +                      cycle.map(c => quote(c.toString)).mkString(" via "))) +
   6.101 +                        Position.here(info.pos))
   6.102 +              }
   6.103 +          }
   6.104 +      }
   6.105  
   6.106 -      new Tree(graph2)
   6.107 -    }
   6.108 +    new T(graph2)
   6.109    }
   6.110  
   6.111 -  final class Tree private(val graph: Graph[String, Info])
   6.112 +  final class T private[Sessions](val graph: Graph[String, Info])
   6.113      extends PartialFunction[String, Info]
   6.114    {
   6.115      def apply(name: String): Info = graph.get_node(name)
   6.116 @@ -235,7 +233,7 @@
   6.117        exclude_session_groups: List[String] = Nil,
   6.118        exclude_sessions: List[String] = Nil,
   6.119        session_groups: List[String] = Nil,
   6.120 -      sessions: List[String] = Nil): (List[String], Tree) =
   6.121 +      sessions: List[String] = Nil): (List[String], T) =
   6.122      {
   6.123        val bad_sessions =
   6.124          SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
   6.125 @@ -270,7 +268,7 @@
   6.126          else pre_selected
   6.127  
   6.128        val graph1 = graph.restrict(graph.all_preds(selected).toSet)
   6.129 -      (selected, new Tree(graph1))
   6.130 +      (selected, new T(graph1))
   6.131      }
   6.132  
   6.133      def ancestors(name: String): List[String] =
   6.134 @@ -279,7 +277,7 @@
   6.135      def topological_order: List[(String, Info)] =
   6.136        graph.topological_order.map(name => (name, apply(name)))
   6.137  
   6.138 -    override def toString: String = graph.keys_iterator.mkString("Sessions.Tree(", ", ", ")")
   6.139 +    override def toString: String = graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
   6.140    }
   6.141  
   6.142  
   6.143 @@ -450,7 +448,7 @@
   6.144      if (is_session_dir(dir)) dir
   6.145      else error("Bad session root directory: " + dir.toString)
   6.146  
   6.147 -  def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): Tree =
   6.148 +  def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
   6.149    {
   6.150      def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
   6.151        load_root(select, dir) ::: load_roots(select, dir)
   6.152 @@ -481,7 +479,7 @@
   6.153      dirs.foreach(check_session_dir(_))
   6.154      select_dirs.foreach(check_session_dir(_))
   6.155  
   6.156 -    Tree(
   6.157 +    make(
   6.158        for {
   6.159          (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
   6.160          info <- load_dir(select, dir)
     7.1 --- a/src/Pure/Tools/build.scala	Thu Apr 06 21:10:35 2017 +0200
     7.2 +++ b/src/Pure/Tools/build.scala	Thu Apr 06 22:04:30 2017 +0200
     7.3 @@ -63,12 +63,12 @@
     7.4        }
     7.5      }
     7.6  
     7.7 -    def apply(tree: Sessions.Tree, store: Sessions.Store): Queue =
     7.8 +    def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
     7.9      {
    7.10 -      val graph = tree.graph
    7.11 -      val sessions = graph.keys
    7.12 +      val graph = sessions.graph
    7.13 +      val names = graph.keys
    7.14  
    7.15 -      val timings = sessions.map(name => (name, load_timings(store, name)))
    7.16 +      val timings = names.map(name => (name, load_timings(store, name)))
    7.17        val command_timings =
    7.18          Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    7.19        val session_timing =
    7.20 @@ -91,7 +91,7 @@
    7.21              case 0 =>
    7.22                compare_timing(name2, name1) match {
    7.23                  case 0 =>
    7.24 -                  tree(name2).timeout compare tree(name1).timeout match {
    7.25 +                  sessions(name2).timeout compare sessions(name1).timeout match {
    7.26                      case 0 => name1 compare name2
    7.27                      case ord => ord
    7.28                    }
    7.29 @@ -101,7 +101,7 @@
    7.30            }
    7.31        }
    7.32  
    7.33 -      new Queue(graph, SortedSet(sessions: _*)(Ordering), command_timings)
    7.34 +      new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
    7.35      }
    7.36    }
    7.37  
    7.38 @@ -170,7 +170,7 @@
    7.39    private class Job(progress: Progress,
    7.40      name: String,
    7.41      val info: Sessions.Info,
    7.42 -    tree: Sessions.Tree,
    7.43 +    sessions: Sessions.T,
    7.44      deps: Sessions.Deps,
    7.45      store: Sessions.Store,
    7.46      do_output: Boolean,
    7.47 @@ -228,7 +228,7 @@
    7.48            val session_result = Future.promise[Process_Result]
    7.49  
    7.50            Isabelle_Process.start(session, options, logic = parent,
    7.51 -            cwd = info.dir.file, env = env, tree = Some(tree), store = store,
    7.52 +            cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
    7.53              phase_changed =
    7.54              {
    7.55                case Session.Ready => session.protocol_command("build_session", args_yxml)
    7.56 @@ -260,11 +260,13 @@
    7.57                  args =
    7.58                    (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
    7.59                    List("--eval", eval),
    7.60 -                env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
    7.61 +                env = env, sessions = Some(sessions), store = store,
    7.62 +                cleanup = () => args_file.delete)
    7.63              }
    7.64              else {
    7.65                ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
    7.66 -                env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
    7.67 +                env = env, sessions = Some(sessions), store = store,
    7.68 +                cleanup = () => args_file.delete)
    7.69              }
    7.70  
    7.71            process.result(
    7.72 @@ -366,53 +368,53 @@
    7.73        system_mode = system_mode,
    7.74        verbose = verbose,
    7.75        pide = pide,
    7.76 -      selection = { full_tree =>
    7.77 -        full_tree.selection(requirements, all_sessions,
    7.78 +      selection = { full_sessions =>
    7.79 +        full_sessions.selection(requirements, all_sessions,
    7.80            exclude_session_groups, exclude_sessions, session_groups, sessions) })
    7.81    }
    7.82  
    7.83    def build_selection(
    7.84 -    options: Options,
    7.85 -    progress: Progress = No_Progress,
    7.86 -    build_heap: Boolean = false,
    7.87 -    clean_build: Boolean = false,
    7.88 -    dirs: List[Path] = Nil,
    7.89 -    select_dirs: List[Path] = Nil,
    7.90 -    numa_shuffling: Boolean = false,
    7.91 -    max_jobs: Int = 1,
    7.92 -    list_files: Boolean = false,
    7.93 -    check_keywords: Set[String] = Set.empty,
    7.94 -    no_build: Boolean = false,
    7.95 -    system_mode: Boolean = false,
    7.96 -    verbose: Boolean = false,
    7.97 -    pide: Boolean = false,
    7.98 -    selection: Sessions.Tree => (List[String], Sessions.Tree) =
    7.99 -      (_.selection(all_sessions = true))): Results =
   7.100 +      options: Options,
   7.101 +      progress: Progress = No_Progress,
   7.102 +      build_heap: Boolean = false,
   7.103 +      clean_build: Boolean = false,
   7.104 +      dirs: List[Path] = Nil,
   7.105 +      select_dirs: List[Path] = Nil,
   7.106 +      numa_shuffling: Boolean = false,
   7.107 +      max_jobs: Int = 1,
   7.108 +      list_files: Boolean = false,
   7.109 +      check_keywords: Set[String] = Set.empty,
   7.110 +      no_build: Boolean = false,
   7.111 +      system_mode: Boolean = false,
   7.112 +      verbose: Boolean = false,
   7.113 +      pide: Boolean = false,
   7.114 +      selection: Sessions.T => (List[String], Sessions.T) = (_.selection(all_sessions = true))
   7.115 +    ): Results =
   7.116    {
   7.117      /* session selection and dependencies */
   7.118  
   7.119      val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   7.120 -    val full_tree = Sessions.load(build_options, dirs, select_dirs)
   7.121 -    val (selected, selected_tree) = selection(full_tree)
   7.122 +    val full_sessions = Sessions.load(build_options, dirs, select_dirs)
   7.123 +    val (selected, selected_sessions) = selection(full_sessions)
   7.124      val deps =
   7.125 -      Sessions.deps(selected_tree, progress = progress, inlined_files = true,
   7.126 +      Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
   7.127          verbose = verbose, list_files = list_files, check_keywords = check_keywords,
   7.128 -        global_theories = full_tree.global_theories)
   7.129 +        global_theories = full_sessions.global_theories)
   7.130  
   7.131      def sources_stamp(name: String): List[String] =
   7.132 -      (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
   7.133 +      (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
   7.134  
   7.135  
   7.136      /* main build process */
   7.137  
   7.138      val store = Sessions.store(system_mode)
   7.139 -    val queue = Queue(selected_tree, store)
   7.140 +    val queue = Queue(selected_sessions, store)
   7.141  
   7.142      store.prepare_output()
   7.143  
   7.144      // optional cleanup
   7.145      if (clean_build) {
   7.146 -      for (name <- full_tree.graph.all_succs(selected)) {
   7.147 +      for (name <- full_sessions.graph.all_succs(selected)) {
   7.148          val files =
   7.149            List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
   7.150              map(store.output_dir + _).filter(_.is_file)
   7.151 @@ -518,7 +520,7 @@
   7.152              //{{{ check/start next job
   7.153              pending.dequeue(running.isDefinedAt(_)) match {
   7.154                case Some((name, info)) =>
   7.155 -                val ancestor_results = selected_tree.ancestors(name).map(results(_))
   7.156 +                val ancestor_results = selected_sessions.ancestors(name).map(results(_))
   7.157                  val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
   7.158  
   7.159                  val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   7.160 @@ -555,8 +557,8 @@
   7.161                    val numa_node = numa_nodes.next(used_node(_))
   7.162                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   7.163                    val job =
   7.164 -                    new Job(progress, name, info, selected_tree, deps, store, do_output, verbose,
   7.165 -                      pide, numa_node, queue.command_timings(name))
   7.166 +                    new Job(progress, name, info, selected_sessions, deps, store, do_output,
   7.167 +                      verbose, pide, numa_node, queue.command_timings(name))
   7.168                    loop(pending, running + (name -> (ancestor_heaps, job)), results)
   7.169                  }
   7.170                  else {
   7.171 @@ -604,7 +606,7 @@
   7.172          (for {
   7.173            (name, result) <- results0.iterator
   7.174            if result.ok
   7.175 -          info = full_tree(name)
   7.176 +          info = full_sessions(name)
   7.177            if info.options.bool("browser_info")
   7.178          } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   7.179              map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
     8.1 --- a/src/Pure/Tools/ml_process.scala	Thu Apr 06 21:10:35 2017 +0200
     8.2 +++ b/src/Pure/Tools/ml_process.scala	Thu Apr 06 22:04:30 2017 +0200
     8.3 @@ -23,16 +23,16 @@
     8.4      redirect: Boolean = false,
     8.5      cleanup: () => Unit = () => (),
     8.6      channel: Option[System_Channel] = None,
     8.7 -    tree: Option[Sessions.Tree] = None,
     8.8 +    sessions: Option[Sessions.T] = None,
     8.9      store: Sessions.Store = Sessions.store()): Bash.Process =
    8.10    {
    8.11      val logic_name = Isabelle_System.default_logic(logic)
    8.12      val heaps: List[String] =
    8.13        if (raw_ml_system) Nil
    8.14        else {
    8.15 -        val (_, session_tree) =
    8.16 -          tree.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
    8.17 -        (session_tree.ancestors(logic_name) ::: List(logic_name)).
    8.18 +        val (_, selected_sessions) =
    8.19 +          sessions.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
    8.20 +        (selected_sessions.ancestors(logic_name) ::: List(logic_name)).
    8.21            map(a => File.platform_path(store.heap(a)))
    8.22        }
    8.23