1.1 --- a/src/Pure/System/build.scala Sun Jul 22 21:59:14 2012 +0200
1.2 +++ b/src/Pure/System/build.scala Sun Jul 22 23:31:57 2012 +0200
1.3 @@ -62,8 +62,10 @@
1.4 keys: Map[String, Key] = Map.empty,
1.5 graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
1.6 {
1.7 + def is_empty: Boolean = graph.is_empty
1.8 +
1.9 + def apply(name: String): Info = graph.get_node(keys(name))
1.10 def defined(name: String): Boolean = keys.isDefinedAt(name)
1.11 -
1.12 def is_inner(name: String): Boolean = !graph.is_maximal(keys(name))
1.13
1.14 def + (key: Key, info: Info): Queue =
1.15 @@ -85,6 +87,8 @@
1.16 new Queue(keys1, graph1)
1.17 }
1.18
1.19 + def - (name: String): Queue = new Queue(keys - name, graph.del_node(keys(name)))
1.20 +
1.21 def required(names: List[String]): Queue =
1.22 {
1.23 val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
1.24 @@ -93,6 +97,14 @@
1.25 new Queue(keys1, graph1)
1.26 }
1.27
1.28 + def dequeue(skip: String => Boolean): Option[(String, Info)] =
1.29 + {
1.30 + val it = graph.entries.dropWhile(
1.31 + { case (key, (_, (deps, _))) => !deps.isEmpty || skip(key.name) })
1.32 + if (it.hasNext) { val (key, (info, _)) = it.next; Some((key.name, info)) }
1.33 + else None
1.34 + }
1.35 +
1.36 def topological_order: List[(String, Info)] =
1.37 graph.topological_order.map(key => (key.name, graph.get_node(key)))
1.38 }
1.39 @@ -325,7 +337,7 @@
1.40
1.41 def terminate: Unit = thread.interrupt
1.42 def is_finished: Boolean = result.is_finished
1.43 - def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
1.44 + def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
1.45 }
1.46
1.47 private def start_job(save: Boolean, name: String, info: Session.Info): Job =
1.48 @@ -366,12 +378,13 @@
1.49 }
1.50
1.51
1.52 - /* Scala entry point */
1.53 + /* build */
1.54
1.55 private def echo(msg: String) { java.lang.System.out.println(msg) }
1.56 - private def echo_n(msg: String) { java.lang.System.out.print(msg) }
1.57 + private def sleep(): Unit = Thread.sleep(500)
1.58
1.59 - def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
1.60 + def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
1.61 + list_only: Boolean, verbose: Boolean,
1.62 more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
1.63 {
1.64 val options = (Options.init() /: more_options)(_.define_simple(_))
1.65 @@ -396,37 +409,60 @@
1.66 val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
1.67 log_dir.file.mkdirs()
1.68
1.69 + // scheduler loop
1.70 + @tailrec def loop(
1.71 + pending: Session.Queue,
1.72 + running: Map[String, Job],
1.73 + results: Map[String, Int]): Map[String, Int] =
1.74 + {
1.75 + if (pending.is_empty) results
1.76 + else if (running.exists({ case (_, job) => job.is_finished })) {
1.77 + val (name, job) = running.find({ case (_, job) => job.is_finished }).get
1.78
1.79 - val rcs =
1.80 - for ((name, info) <- queue.topological_order) yield
1.81 - {
1.82 - if (list_only) { echo(name + " in " + info.dir); 0 }
1.83 + val (out, err, rc) = job.join
1.84 + echo(Library.trim_line(err))
1.85 +
1.86 + val log = log_dir + Path.basic(name)
1.87 + if (rc == 0) {
1.88 + val sources =
1.89 + (queue(name).digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
1.90 + .mkString("sources: ", " ", "\n")
1.91 + File.write_zip(log.ext("gz"), sources + out)
1.92 + }
1.93 else {
1.94 - val save = build_images || queue.is_inner(name)
1.95 - echo((if (save) "Building " else "Running ") + name + " ...")
1.96 -
1.97 - val (out, err, rc) = start_job(save, name, info).join
1.98 - echo_n(err)
1.99 -
1.100 - val log = log_dir + Path.basic(name)
1.101 - if (rc == 0) {
1.102 - val sources =
1.103 - (info.digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
1.104 - .mkString("sources: ", " ", "\n")
1.105 - File.write_zip(log.ext("gz"), sources + out)
1.106 - }
1.107 - else {
1.108 - File.write(log, out)
1.109 - echo(name + " FAILED")
1.110 - echo("(see also " + log.file + ")")
1.111 - val lines = split_lines(out)
1.112 - val tail = lines.drop(lines.length - 20 max 0)
1.113 - echo("\n" + cat_lines(tail))
1.114 - }
1.115 - rc
1.116 + File.write(log, out)
1.117 + echo(name + " FAILED")
1.118 + echo("(see also " + log.file + ")")
1.119 + val lines = split_lines(out)
1.120 + val tail = lines.drop(lines.length - 20 max 0)
1.121 + echo("\n" + cat_lines(tail))
1.122 + }
1.123 + loop(pending - name, running - name, results + (name -> rc))
1.124 + }
1.125 + else if (running.size < (max_jobs max 1)) {
1.126 + pending.dequeue(running.isDefinedAt(_)) match {
1.127 + case Some((name, info)) =>
1.128 + if (list_only) {
1.129 + echo(name + " in " + info.dir)
1.130 + loop(pending - name, running, results + (name -> 0))
1.131 + }
1.132 + else if (info.parent.map(results(_)).forall(_ == 0)) {
1.133 + val save = build_images || queue.is_inner(name)
1.134 + echo((if (save) "Building " else "Running ") + name + " ...")
1.135 + val job = start_job(save, name, info)
1.136 + loop(pending, running + (name -> job), results)
1.137 + }
1.138 + else {
1.139 + echo(name + " CANCELLED")
1.140 + loop(pending - name, running, results + (name -> 1))
1.141 + }
1.142 + case None => sleep(); loop(pending, running, results)
1.143 }
1.144 }
1.145 - (0 /: rcs)(_ max _)
1.146 + else { sleep(); loop(pending, running, results) }
1.147 + }
1.148 +
1.149 + (0 /: loop(queue, Map.empty, Map.empty))({ case (rc1, (_, rc2)) => rc1 max rc2 })
1.150 }
1.151
1.152
1.153 @@ -439,9 +475,11 @@
1.154 case
1.155 Properties.Value.Boolean(all_sessions) ::
1.156 Properties.Value.Boolean(build_images) ::
1.157 + Properties.Value.Int(max_jobs) ::
1.158 Properties.Value.Boolean(list_only) ::
1.159 + Properties.Value.Boolean(verbose) ::
1.160 Command_Line.Chunks(more_dirs, options, sessions) =>
1.161 - build(all_sessions, build_images, list_only,
1.162 + build(all_sessions, build_images, max_jobs, list_only, verbose,
1.163 more_dirs.map(Path.explode), options, sessions)
1.164 case _ => error("Bad arguments:\n" + cat_lines(args))
1.165 }