src/Pure/System/build.scala
changeset 48424 e6b0c14f04c8
parent 48423 0ccf143a2a69
child 48425 0d95980e9aae
equal deleted inserted replaced
48423:0ccf143a2a69 48424:e6b0c14f04c8
    38       override def toString: String = name
    38       override def toString: String = name
    39     }
    39     }
    40 
    40 
    41 
    41 
    42     /* Info */
    42     /* Info */
    43 
       
    44     sealed abstract class Status
       
    45     case object Pending extends Status
       
    46     case object Running extends Status
       
    47 
    43 
    48     sealed case class Info(
    44     sealed case class Info(
    49       dir: Path,
    45       dir: Path,
    50       parent: Option[String],
    46       parent: Option[String],
    51       description: String,
    47       description: String,
    52       options: Options,
    48       options: Options,
    53       theories: List[(Options, List[Path])],
    49       theories: List[(Options, List[Path])],
    54       files: List[Path],
    50       files: List[Path],
    55       digest: SHA1.Digest,
    51       digest: SHA1.Digest)
    56       status: Status = Pending)
       
    57 
    52 
    58 
    53 
    59     /* Queue */
    54     /* Queue */
    60 
    55 
    61     object Queue
    56     object Queue
   266     }
   261     }
   267 
   262 
   268     if (all_sessions) queue else queue.required(sessions)
   263     if (all_sessions) queue else queue.required(sessions)
   269   }
   264   }
   270 
   265 
       
   266 
       
   267 
       
   268   /** build **/
   271 
   269 
   272   /* dependencies */
   270   /* dependencies */
   273 
   271 
   274   sealed case class Node(
   272   sealed case class Node(
   275     loaded_theories: Set[String],
   273     loaded_theories: Set[String],
   312 
   310 
   313           deps + (name -> Node(loaded_theories, sources))
   311           deps + (name -> Node(loaded_theories, sources))
   314       }))
   312       }))
   315 
   313 
   316 
   314 
   317 
   315   /* jobs */
   318   /** build **/
   316 
   319 
   317   private class Job(cwd: JFile, env: Map[String, String], script: String, args: String)
   320   private def echo(msg: String) { java.lang.System.out.println(msg) }
       
   321   private def echo_n(msg: String) { java.lang.System.out.print(msg) }
       
   322 
       
   323   class Build_Job(cwd: JFile, env: Map[String, String], script: String, args: String)
       
   324   {
   318   {
   325     private val args_file = File.tmp_file("args")
   319     private val args_file = File.tmp_file("args")
   326     private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
   320     private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
   327     File.write(args_file, args)
   321     File.write(args_file, args)
   328 
   322 
   329     private val (thread, result) = Simple_Thread.future("build_job") {
   323     private val (thread, result) =
   330       Isabelle_System.bash_env(cwd, env1, script)
   324       Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) }
   331     }
       
   332 
   325 
   333     def terminate: Unit = thread.interrupt
   326     def terminate: Unit = thread.interrupt
   334     def is_finished: Boolean = result.is_finished
   327     def is_finished: Boolean = result.is_finished
   335     def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
   328     def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
   336   }
   329   }
   337 
   330 
   338   private def build_job(save: Boolean, name: String, info: Session.Info): Build_Job =
   331   private def start_job(save: Boolean, name: String, info: Session.Info): Job =
   339   {
   332   {
   340     val parent = info.parent.getOrElse("")
   333     val parent = info.parent.getOrElse("")
   341 
   334 
   342     val cwd = info.dir.file
   335     val cwd = info.dir.file
   343     val env = Map("INPUT" -> parent, "TARGET" -> name)
   336     val env = Map("INPUT" -> parent, "TARGET" -> name)
   367     {
   360     {
   368       import XML.Encode._
   361       import XML.Encode._
   369       pair(bool, pair(string, pair(string, list(string))))(
   362       pair(bool, pair(string, pair(string, list(string))))(
   370         save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
   363         save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
   371     }
   364     }
   372     new Build_Job(cwd, env, script, YXML.string_of_body(args_xml))
   365     new Job(cwd, env, script, YXML.string_of_body(args_xml))
   373   }
   366   }
       
   367 
       
   368 
       
   369   /* Scala entry point */
       
   370 
       
   371   private def echo(msg: String) { java.lang.System.out.println(msg) }
       
   372   private def echo_n(msg: String) { java.lang.System.out.print(msg) }
   374 
   373 
   375   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   374   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   376     more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
   375     more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
   377   {
   376   {
   378     val options = (Options.init() /: more_options)(_.define_simple(_))
   377     val options = (Options.init() /: more_options)(_.define_simple(_))
   395 
   394 
   396     // prepare log dir
   395     // prepare log dir
   397     val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
   396     val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
   398     log_dir.file.mkdirs()
   397     log_dir.file.mkdirs()
   399 
   398 
   400     // run jobs
   399 
   401     val rcs =
   400     val rcs =
   402       for ((name, info) <- queue.topological_order) yield
   401       for ((name, info) <- queue.topological_order) yield
   403       {
   402       {
   404         if (list_only) { echo(name + " in " + info.dir); 0 }
   403         if (list_only) { echo(name + " in " + info.dir); 0 }
   405         else {
   404         else {
   406           val save = build_images || queue.is_inner(name)
   405           val save = build_images || queue.is_inner(name)
   407           echo((if (save) "Building " else "Running ") + name + " ...")
   406           echo((if (save) "Building " else "Running ") + name + " ...")
   408 
   407 
   409           val (out, err, rc) = build_job(save, name, info).join
   408           val (out, err, rc) = start_job(save, name, info).join
   410           echo_n(err)
   409           echo_n(err)
   411 
   410 
   412           val log = log_dir + Path.basic(name)
   411           val log = log_dir + Path.basic(name)
   413           if (rc == 0) {
   412           if (rc == 0) {
   414             val sources =
   413             val sources =