src/Pure/System/build.scala
changeset 48425 0d95980e9aae
parent 48424 e6b0c14f04c8
child 48447 ef600ce4559c
--- a/src/Pure/System/build.scala	Sun Jul 22 21:59:14 2012 +0200
+++ b/src/Pure/System/build.scala	Sun Jul 22 23:31:57 2012 +0200
@@ -62,8 +62,10 @@
       keys: Map[String, Key] = Map.empty,
       graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
     {
+      def is_empty: Boolean = graph.is_empty
+
+      def apply(name: String): Info = graph.get_node(keys(name))
       def defined(name: String): Boolean = keys.isDefinedAt(name)
-
       def is_inner(name: String): Boolean = !graph.is_maximal(keys(name))
 
       def + (key: Key, info: Info): Queue =
@@ -85,6 +87,8 @@
         new Queue(keys1, graph1)
       }
 
+      def - (name: String): Queue = new Queue(keys - name, graph.del_node(keys(name)))
+
       def required(names: List[String]): Queue =
       {
         val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
@@ -93,6 +97,14 @@
         new Queue(keys1, graph1)
       }
 
+      def dequeue(skip: String => Boolean): Option[(String, Info)] =
+      {
+        val it = graph.entries.dropWhile(
+          { case (key, (_, (deps, _))) => !deps.isEmpty || skip(key.name) })
+        if (it.hasNext) { val (key, (info, _)) = it.next; Some((key.name, info)) }
+        else None
+      }
+
       def topological_order: List[(String, Info)] =
         graph.topological_order.map(key => (key.name, graph.get_node(key)))
     }
@@ -325,7 +337,7 @@
 
     def terminate: Unit = thread.interrupt
     def is_finished: Boolean = result.is_finished
-    def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
+    def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
   }
 
   private def start_job(save: Boolean, name: String, info: Session.Info): Job =
@@ -366,12 +378,13 @@
   }
 
 
-  /* Scala entry point */
+  /* build */
 
   private def echo(msg: String) { java.lang.System.out.println(msg) }
-  private def echo_n(msg: String) { java.lang.System.out.print(msg) }
+  private def sleep(): Unit = Thread.sleep(500)
 
-  def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
+  def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
+    list_only: Boolean, verbose: Boolean,
     more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
   {
     val options = (Options.init() /: more_options)(_.define_simple(_))
@@ -396,37 +409,60 @@
     val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
     log_dir.file.mkdirs()
 
+    // scheduler loop
+    @tailrec def loop(
+      pending: Session.Queue,
+      running: Map[String, Job],
+      results: Map[String, Int]): Map[String, Int] =
+    {
+      if (pending.is_empty) results
+      else if (running.exists({ case (_, job) => job.is_finished })) {
+        val (name, job) = running.find({ case (_, job) => job.is_finished }).get
 
-    val rcs =
-      for ((name, info) <- queue.topological_order) yield
-      {
-        if (list_only) { echo(name + " in " + info.dir); 0 }
-        else {
-          val save = build_images || queue.is_inner(name)
-          echo((if (save) "Building " else "Running ") + name + " ...")
-
-          val (out, err, rc) = start_job(save, name, info).join
-          echo_n(err)
+        val (out, err, rc) = job.join
+        echo(Library.trim_line(err))
 
-          val log = log_dir + Path.basic(name)
-          if (rc == 0) {
-            val sources =
-              (info.digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
-                .mkString("sources: ", " ", "\n")
-            File.write_zip(log.ext("gz"), sources + out)
-          }
-          else {
-            File.write(log, out)
-            echo(name + " FAILED")
-            echo("(see also " + log.file + ")")
-            val lines = split_lines(out)
-            val tail = lines.drop(lines.length - 20 max 0)
-            echo("\n" + cat_lines(tail))
-          }
-          rc
+        val log = log_dir + Path.basic(name)
+        if (rc == 0) {
+          val sources =
+            (queue(name).digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
+              .mkString("sources: ", " ", "\n")
+          File.write_zip(log.ext("gz"), sources + out)
+        }
+        else {
+          File.write(log, out)
+          echo(name + " FAILED")
+          echo("(see also " + log.file + ")")
+          val lines = split_lines(out)
+          val tail = lines.drop(lines.length - 20 max 0)
+          echo("\n" + cat_lines(tail))
+        }
+        loop(pending - name, running - name, results + (name -> rc))
+      }
+      else if (running.size < (max_jobs max 1)) {
+        pending.dequeue(running.isDefinedAt(_)) match {
+          case Some((name, info)) =>
+            if (list_only) {
+              echo(name + " in " + info.dir)
+              loop(pending - name, running, results + (name -> 0))
+            }
+            else if (info.parent.map(results(_)).forall(_ == 0)) {
+              val save = build_images || queue.is_inner(name)
+              echo((if (save) "Building " else "Running ") + name + " ...")
+              val job = start_job(save, name, info)
+              loop(pending, running + (name -> job), results)
+            }
+            else {
+              echo(name + " CANCELLED")
+              loop(pending - name, running, results + (name -> 1))
+            }
+          case None => sleep(); loop(pending, running, results)
         }
       }
-    (0 /: rcs)(_ max _)
+      else { sleep(); loop(pending, running, results) }
+    }
+
+    (0 /: loop(queue, Map.empty, Map.empty))({ case (rc1, (_, rc2)) => rc1 max rc2 })
   }
 
 
@@ -439,9 +475,11 @@
         case
           Properties.Value.Boolean(all_sessions) ::
           Properties.Value.Boolean(build_images) ::
+          Properties.Value.Int(max_jobs) ::
           Properties.Value.Boolean(list_only) ::
+          Properties.Value.Boolean(verbose) ::
           Command_Line.Chunks(more_dirs, options, sessions) =>
-            build(all_sessions, build_images, list_only,
+            build(all_sessions, build_images, max_jobs, list_only, verbose,
               more_dirs.map(Path.explode), options, sessions)
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }