src/Pure/Tools/build.scala
changeset 65415 8cd54b18b68b
parent 65406 cc9e2f1f279d
child 65419 457e4fbed731
     1.1 --- a/src/Pure/Tools/build.scala	Thu Apr 06 21:10:35 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Apr 06 22:04:30 2017 +0200
     1.3 @@ -63,12 +63,12 @@
     1.4        }
     1.5      }
     1.6  
     1.7 -    def apply(tree: Sessions.Tree, store: Sessions.Store): Queue =
     1.8 +    def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
     1.9      {
    1.10 -      val graph = tree.graph
    1.11 -      val sessions = graph.keys
    1.12 +      val graph = sessions.graph
    1.13 +      val names = graph.keys
    1.14  
    1.15 -      val timings = sessions.map(name => (name, load_timings(store, name)))
    1.16 +      val timings = names.map(name => (name, load_timings(store, name)))
    1.17        val command_timings =
    1.18          Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    1.19        val session_timing =
    1.20 @@ -91,7 +91,7 @@
    1.21              case 0 =>
    1.22                compare_timing(name2, name1) match {
    1.23                  case 0 =>
    1.24 -                  tree(name2).timeout compare tree(name1).timeout match {
    1.25 +                  sessions(name2).timeout compare sessions(name1).timeout match {
    1.26                      case 0 => name1 compare name2
    1.27                      case ord => ord
    1.28                    }
    1.29 @@ -101,7 +101,7 @@
    1.30            }
    1.31        }
    1.32  
    1.33 -      new Queue(graph, SortedSet(sessions: _*)(Ordering), command_timings)
    1.34 +      new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
    1.35      }
    1.36    }
    1.37  
    1.38 @@ -170,7 +170,7 @@
    1.39    private class Job(progress: Progress,
    1.40      name: String,
    1.41      val info: Sessions.Info,
    1.42 -    tree: Sessions.Tree,
    1.43 +    sessions: Sessions.T,
    1.44      deps: Sessions.Deps,
    1.45      store: Sessions.Store,
    1.46      do_output: Boolean,
    1.47 @@ -228,7 +228,7 @@
    1.48            val session_result = Future.promise[Process_Result]
    1.49  
    1.50            Isabelle_Process.start(session, options, logic = parent,
    1.51 -            cwd = info.dir.file, env = env, tree = Some(tree), store = store,
    1.52 +            cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
    1.53              phase_changed =
    1.54              {
    1.55                case Session.Ready => session.protocol_command("build_session", args_yxml)
    1.56 @@ -260,11 +260,13 @@
    1.57                  args =
    1.58                    (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
    1.59                    List("--eval", eval),
    1.60 -                env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
    1.61 +                env = env, sessions = Some(sessions), store = store,
    1.62 +                cleanup = () => args_file.delete)
    1.63              }
    1.64              else {
    1.65                ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
    1.66 -                env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
    1.67 +                env = env, sessions = Some(sessions), store = store,
    1.68 +                cleanup = () => args_file.delete)
    1.69              }
    1.70  
    1.71            process.result(
    1.72 @@ -366,53 +368,53 @@
    1.73        system_mode = system_mode,
    1.74        verbose = verbose,
    1.75        pide = pide,
    1.76 -      selection = { full_tree =>
    1.77 -        full_tree.selection(requirements, all_sessions,
    1.78 +      selection = { full_sessions =>
    1.79 +        full_sessions.selection(requirements, all_sessions,
    1.80            exclude_session_groups, exclude_sessions, session_groups, sessions) })
    1.81    }
    1.82  
    1.83    def build_selection(
    1.84 -    options: Options,
    1.85 -    progress: Progress = No_Progress,
    1.86 -    build_heap: Boolean = false,
    1.87 -    clean_build: Boolean = false,
    1.88 -    dirs: List[Path] = Nil,
    1.89 -    select_dirs: List[Path] = Nil,
    1.90 -    numa_shuffling: Boolean = false,
    1.91 -    max_jobs: Int = 1,
    1.92 -    list_files: Boolean = false,
    1.93 -    check_keywords: Set[String] = Set.empty,
    1.94 -    no_build: Boolean = false,
    1.95 -    system_mode: Boolean = false,
    1.96 -    verbose: Boolean = false,
    1.97 -    pide: Boolean = false,
    1.98 -    selection: Sessions.Tree => (List[String], Sessions.Tree) =
    1.99 -      (_.selection(all_sessions = true))): Results =
   1.100 +      options: Options,
   1.101 +      progress: Progress = No_Progress,
   1.102 +      build_heap: Boolean = false,
   1.103 +      clean_build: Boolean = false,
   1.104 +      dirs: List[Path] = Nil,
   1.105 +      select_dirs: List[Path] = Nil,
   1.106 +      numa_shuffling: Boolean = false,
   1.107 +      max_jobs: Int = 1,
   1.108 +      list_files: Boolean = false,
   1.109 +      check_keywords: Set[String] = Set.empty,
   1.110 +      no_build: Boolean = false,
   1.111 +      system_mode: Boolean = false,
   1.112 +      verbose: Boolean = false,
   1.113 +      pide: Boolean = false,
   1.114 +      selection: Sessions.T => (List[String], Sessions.T) = (_.selection(all_sessions = true))
   1.115 +    ): Results =
   1.116    {
   1.117      /* session selection and dependencies */
   1.118  
   1.119      val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   1.120 -    val full_tree = Sessions.load(build_options, dirs, select_dirs)
   1.121 -    val (selected, selected_tree) = selection(full_tree)
   1.122 +    val full_sessions = Sessions.load(build_options, dirs, select_dirs)
   1.123 +    val (selected, selected_sessions) = selection(full_sessions)
   1.124      val deps =
   1.125 -      Sessions.deps(selected_tree, progress = progress, inlined_files = true,
   1.126 +      Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
   1.127          verbose = verbose, list_files = list_files, check_keywords = check_keywords,
   1.128 -        global_theories = full_tree.global_theories)
   1.129 +        global_theories = full_sessions.global_theories)
   1.130  
   1.131      def sources_stamp(name: String): List[String] =
   1.132 -      (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
   1.133 +      (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
   1.134  
   1.135  
   1.136      /* main build process */
   1.137  
   1.138      val store = Sessions.store(system_mode)
   1.139 -    val queue = Queue(selected_tree, store)
   1.140 +    val queue = Queue(selected_sessions, store)
   1.141  
   1.142      store.prepare_output()
   1.143  
   1.144      // optional cleanup
   1.145      if (clean_build) {
   1.146 -      for (name <- full_tree.graph.all_succs(selected)) {
   1.147 +      for (name <- full_sessions.graph.all_succs(selected)) {
   1.148          val files =
   1.149            List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
   1.150              map(store.output_dir + _).filter(_.is_file)
   1.151 @@ -518,7 +520,7 @@
   1.152              //{{{ check/start next job
   1.153              pending.dequeue(running.isDefinedAt(_)) match {
   1.154                case Some((name, info)) =>
   1.155 -                val ancestor_results = selected_tree.ancestors(name).map(results(_))
   1.156 +                val ancestor_results = selected_sessions.ancestors(name).map(results(_))
   1.157                  val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
   1.158  
   1.159                  val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   1.160 @@ -555,8 +557,8 @@
   1.161                    val numa_node = numa_nodes.next(used_node(_))
   1.162                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   1.163                    val job =
   1.164 -                    new Job(progress, name, info, selected_tree, deps, store, do_output, verbose,
   1.165 -                      pide, numa_node, queue.command_timings(name))
   1.166 +                    new Job(progress, name, info, selected_sessions, deps, store, do_output,
   1.167 +                      verbose, pide, numa_node, queue.command_timings(name))
   1.168                    loop(pending, running + (name -> (ancestor_heaps, job)), results)
   1.169                  }
   1.170                  else {
   1.171 @@ -604,7 +606,7 @@
   1.172          (for {
   1.173            (name, result) <- results0.iterator
   1.174            if result.ok
   1.175 -          info = full_tree(name)
   1.176 +          info = full_sessions(name)
   1.177            if info.options.bool("browser_info")
   1.178          } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   1.179              map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)