src/Pure/System/build.scala
changeset 48418 1a634f9614fb
parent 48411 5b3440850d36
child 48419 6d7b6e47f3ef
equal deleted inserted replaced
48417:bb1d4ec90f30 48418:1a634f9614fb
    38       override def toString: String = name
    38       override def toString: String = name
    39     }
    39     }
    40 
    40 
    41     sealed case class Info(
    41     sealed case class Info(
    42       dir: Path,
    42       dir: Path,
       
    43       parent: Option[String],
    43       description: String,
    44       description: String,
    44       options: Options,
    45       options: Options,
    45       theories: List[(Options, String)],
    46       theories: List[(Options, List[String])],
    46       files: List[String])
    47       files: List[String])
    47 
    48 
    48     object Queue
    49     object Queue
    49     {
    50     {
    50       val empty: Queue = new Queue()
    51       val empty: Queue = new Queue()
    54       keys: Map[String, Key] = Map.empty,
    55       keys: Map[String, Key] = Map.empty,
    55       graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
    56       graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
    56     {
    57     {
    57       def defined(name: String): Boolean = keys.isDefinedAt(name)
    58       def defined(name: String): Boolean = keys.isDefinedAt(name)
    58 
    59 
    59       def + (key: Key, info: Info, parent: Option[String]): Queue =
    60       def + (key: Key, info: Info): Queue =
    60       {
    61       {
    61         val keys1 =
    62         val keys1 =
    62           if (defined(key.name)) error("Duplicate session: " + quote(key.name))
    63           if (defined(key.name)) error("Duplicate session: " + quote(key.name))
    63           else keys + (key.name -> key)
    64           else keys + (key.name -> key)
    64 
    65 
    65         val graph1 =
    66         val graph1 =
    66           try {
    67           try {
    67             graph.new_node(key, info).add_deps_acyclic(key, parent.toList.map(keys(_)))
    68             graph.new_node(key, info).add_deps_acyclic(key, info.parent.toList.map(keys(_)))
    68           }
    69           }
    69           catch {
    70           catch {
    70             case exn: Graph.Cycles[_] =>
    71             case exn: Graph.Cycles[_] =>
    71               error(cat_lines(exn.cycles.map(cycle =>
    72               error(cat_lines(exn.cycles.map(cycle =>
    72                 "Cyclic session dependency of " +
    73                 "Cyclic session dependency of " +
   182             case Some(p) => Path.explode(p)
   183             case Some(p) => Path.explode(p)
   183             case None => Path.basic(entry.name)
   184             case None => Path.basic(entry.name)
   184           }
   185           }
   185 
   186 
   186         val key = Session.Key(full_name, entry.order)
   187         val key = Session.Key(full_name, entry.order)
   187         val info = Session.Info(dir + path, entry.description, entry.options,
   188         val info =
   188           entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
   189           Session.Info(dir + path, entry.parent,
   189 
   190             entry.description, entry.options, entry.theories, entry.files)
   190         queue1 + (key, info, entry.parent)
   191 
       
   192         queue1 + (key, info)
   191       }
   193       }
   192       catch {
   194       catch {
   193         case ERROR(msg) =>
   195         case ERROR(msg) =>
   194           error(msg + "\nThe error(s) above occurred in session entry " +
   196           error(msg + "\nThe error(s) above occurred in session entry " +
   195             quote(entry.name) + Position.str_of(Position.file(root)))
   197             quote(entry.name) + Position.str_of(Position.file(root)))
   242   /** build **/
   244   /** build **/
   243 
   245 
   244   private def echo(msg: String) { java.lang.System.out.println(msg) }
   246   private def echo(msg: String) { java.lang.System.out.println(msg) }
   245   private def echo_n(msg: String) { java.lang.System.out.print(msg) }
   247   private def echo_n(msg: String) { java.lang.System.out.print(msg) }
   246 
   248 
   247   private def build_job(build_images: Boolean,  // FIXME
   249   class Build_Job(cwd: JFile, env: Map[String, String], script: String, args: String)
   248     key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
   250   {
   249   {
   251     private val args_file = File.tmp_file("args")
       
   252     private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
       
   253     File.write(args_file, args)
       
   254 
       
   255     private val (thread, result) = Simple_Thread.future("build_job") {
       
   256       Isabelle_System.bash_env(cwd, env1, script)
       
   257     }
       
   258 
       
   259     def terminate: Unit = thread.interrupt
       
   260     def is_finished: Boolean = result.is_finished
       
   261     def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
       
   262   }
       
   263 
       
   264   private def build_job(build_images: Boolean, name: String, info: Session.Info): Build_Job =
       
   265   {
       
   266     val parent = info.parent.getOrElse("")
       
   267 
   250     val cwd = info.dir.file
   268     val cwd = info.dir.file
       
   269     val env = Map("INPUT" -> parent, "TARGET" -> name)
   251     val script =
   270     val script =
   252       if (is_pure(key.name)) "./build " + (if (build_images) "-b " else "") + key.name
   271       if (is_pure(name)) "./build " + (if (build_images) "-b " else "") + name
   253       else """echo "Bad session" >&2; exit 2"""
   272       else {
   254     new Isabelle_System.Bash_Job(cwd, null, script)
   273         """
       
   274         . "$ISABELLE_HOME/lib/scripts/timestart.bash"
       
   275         """ +
       
   276           (if (build_images)
       
   277             """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
       
   278           else
       
   279             """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
       
   280         """
       
   281         RC="$?"
       
   282 
       
   283         . "$ISABELLE_HOME/lib/scripts/timestop.bash"
       
   284 
       
   285         if [ "$RC" -eq 0 ]; then
       
   286           echo "Finished $TARGET ($TIMES_REPORT)" >&2
       
   287         fi
       
   288 
       
   289         exit "$RC"
       
   290         """
       
   291       }
       
   292     val args_xml =
       
   293     {
       
   294       import XML.Encode._
       
   295       def symbol_string: T[String] = (s => string(Symbol.encode(s)))
       
   296       pair(bool, pair(symbol_string, pair(symbol_string, list(symbol_string))))(
       
   297         build_images, (parent, (name, info.theories.map(_._2).flatten)))
       
   298     }
       
   299     new Build_Job(cwd, env, script, YXML.string_of_body(args_xml))
   255   }
   300   }
   256 
   301 
   257   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   302   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   258     more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   303     more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   259   {
   304   {
   290     val rcs =
   335     val rcs =
   291       for ((key, info) <- required_queue.topological_order) yield
   336       for ((key, info) <- required_queue.topological_order) yield
   292       {
   337       {
   293         if (list_only) { echo(key.name + " in " + info.dir); 0 }
   338         if (list_only) { echo(key.name + " in " + info.dir); 0 }
   294         else {
   339         else {
   295           if (build_images) echo("Building " + key.name + "...")
   340           if (build_images) echo("Building " + key.name + " ...")
   296           else echo("Running " + key.name + "...")
   341           else echo("Running " + key.name + " ...")
   297 
   342 
   298           val (out, err, rc) = build_job(build_images, key, info).join
   343           val (out, err, rc) = build_job(build_images, key.name, info).join
   299           echo_n(err)
   344           echo_n(err)
   300 
   345 
   301           val log = log_dir + Path.basic(key.name)
   346           val log = log_dir + Path.basic(key.name)
   302           if (rc == 0) {
   347           if (rc == 0) {
   303             File.write_zip(log.ext("gz"), out)
   348             File.write_zip(log.ext("gz"), out)