src/Pure/System/build.scala
author wenzelm
Sun Jul 22 12:26:41 2012 +0200 (2012-07-22)
changeset 48423 0ccf143a2a69
parent 48422 9613780a805b
child 48424 e6b0c14f04c8
permissions -rw-r--r--
maintain set of source digests, including relevant parts of session entry;
     1 /*  Title:      Pure/System/build.scala
     2     Author:     Makarius
     3 
     4 Build and manage Isabelle sessions.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{File => JFile}
    11 
    12 import scala.collection.mutable
    13 import scala.annotation.tailrec
    14 
    15 
    16 object Build
    17 {
    18   /** session information **/
    19 
    20   object Session
    21   {
    22     /* Key */
    23 
    24     object Key
    25     {
    26       object Ordering extends scala.math.Ordering[Key]
    27       {
    28         def compare(key1: Key, key2: Key): Int =
    29           key1.order compare key2.order match {
    30             case 0 => key1.name compare key2.name
    31             case ord => ord
    32           }
    33       }
    34     }
    35 
    36     sealed case class Key(name: String, order: Int)
    37     {
    38       override def toString: String = name
    39     }
    40 
    41 
    42     /* Info */
    43 
    44     sealed abstract class Status
    45     case object Pending extends Status
    46     case object Running extends Status
    47 
    48     sealed case class Info(
    49       dir: Path,
    50       parent: Option[String],
    51       description: String,
    52       options: Options,
    53       theories: List[(Options, List[Path])],
    54       files: List[Path],
    55       digest: SHA1.Digest,
    56       status: Status = Pending)
    57 
    58 
    59     /* Queue */
    60 
    61     object Queue
    62     {
    63       val empty: Queue = new Queue()
    64     }
    65 
    66     final class Queue private(
    67       keys: Map[String, Key] = Map.empty,
    68       graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
    69     {
    70       def defined(name: String): Boolean = keys.isDefinedAt(name)
    71 
    72       def is_inner(name: String): Boolean = !graph.is_maximal(keys(name))
    73 
    74       def + (key: Key, info: Info): Queue =
    75       {
    76         val keys1 =
    77           if (defined(key.name)) error("Duplicate session: " + quote(key.name))
    78           else keys + (key.name -> key)
    79 
    80         val graph1 =
    81           try {
    82             graph.new_node(key, info).add_deps_acyclic(key, info.parent.toList.map(keys(_)))
    83           }
    84           catch {
    85             case exn: Graph.Cycles[_] =>
    86               error(cat_lines(exn.cycles.map(cycle =>
    87                 "Cyclic session dependency of " +
    88                   cycle.map(key => quote(key.toString)).mkString(" via "))))
    89           }
    90         new Queue(keys1, graph1)
    91       }
    92 
    93       def required(names: List[String]): Queue =
    94       {
    95         val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
    96         val keys1 = keys -- keys.keySet.filter(name => !req(name))
    97         val graph1 = graph.restrict(key => keys1.isDefinedAt(key.name))
    98         new Queue(keys1, graph1)
    99       }
   100 
   101       def topological_order: List[(String, Info)] =
   102         graph.topological_order.map(key => (key.name, graph.get_node(key)))
   103     }
   104   }
   105 
   106 
   107   /* parsing */
   108 
   109   private case class Session_Entry(
   110     name: String,
   111     reset: Boolean,
   112     order: Int,
   113     path: Option[String],
   114     parent: Option[String],
   115     description: String,
   116     options: List[Options.Spec],
   117     theories: List[(List[Options.Spec], List[String])],
   118     files: List[String])
   119 
   120   private object Parser extends Parse.Parser
   121   {
   122     val SESSION = "session"
   123     val IN = "in"
   124     val DESCRIPTION = "description"
   125     val OPTIONS = "options"
   126     val THEORIES = "theories"
   127     val FILES = "files"
   128 
   129     val syntax =
   130       Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   131         SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   132 
   133     val session_entry: Parser[Session_Entry] =
   134     {
   135       val session_name = atom("session name", _.is_name)
   136       val theory_name = atom("theory name", _.is_name)
   137 
   138       val option =
   139         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   140       val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
   141 
   142       val theories =
   143         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
   144           { case _ ~ (x ~ y) => (x, y) }
   145 
   146       ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
   147         (keyword("!") ^^^ true | success(false)) ~
   148         (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~
   149         (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
   150         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
   151         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
   152         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
   153         rep(theories) ~
   154         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
   155           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
   156     }
   157 
   158     def parse_entries(root: JFile): List[Session_Entry] =
   159     {
   160       val toks = syntax.scan(File.read(root))
   161       parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
   162         case Success(result, _) => result
   163         case bad => error(bad.toString)
   164       }
   165     }
   166   }
   167 
   168 
   169   /* find sessions */
   170 
   171   private val ROOT = Path.explode("ROOT")
   172   private val SESSIONS = Path.explode("etc/sessions")
   173 
   174   private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
   175 
   176   private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue)
   177     : Session.Queue =
   178   {
   179     (queue /: Parser.parse_entries(root))((queue1, entry) =>
   180       try {
   181         if (entry.name == "") error("Bad session name")
   182 
   183         val full_name =
   184           if (is_pure(entry.name)) {
   185             if (entry.parent.isDefined) error("Illegal parent session")
   186             else entry.name
   187           }
   188           else
   189             entry.parent match {
   190               case Some(parent_name) if queue1.defined(parent_name) =>
   191                 if (entry.reset) entry.name
   192                 else parent_name + "-" + entry.name
   193               case _ => error("Bad parent session")
   194             }
   195 
   196         val path =
   197           entry.path match {
   198             case Some(p) => Path.explode(p)
   199             case None => Path.basic(entry.name)
   200           }
   201 
   202         val key = Session.Key(full_name, entry.order)
   203 
   204         val theories =
   205           entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) })
   206         val files = entry.files.map(Path.explode(_))
   207         val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
   208 
   209         val info =
   210           Session.Info(dir + path, entry.parent,
   211             entry.description, options ++ entry.options, theories, files, digest)
   212 
   213         queue1 + (key, info)
   214       }
   215       catch {
   216         case ERROR(msg) =>
   217           error(msg + "\nThe error(s) above occurred in session entry " +
   218             quote(entry.name) + Position.str_of(Position.file(root)))
   219       })
   220   }
   221 
   222   private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
   223     : Session.Queue =
   224   {
   225     val root = (dir + ROOT).file
   226     if (root.isFile) sessions_root(options, dir, root, queue)
   227     else if (strict) error("Bad session root file: " + quote(root.toString))
   228     else queue
   229   }
   230 
   231   private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue)
   232     : Session.Queue =
   233   {
   234     val dirs =
   235       split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
   236     (queue /: dirs)((queue1, dir1) =>
   237       try {
   238         val dir2 = dir + Path.explode(dir1)
   239         if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1)
   240         else error("Bad session directory: " + dir2.toString)
   241       }
   242       catch {
   243         case ERROR(msg) =>
   244           error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
   245       })
   246   }
   247 
   248   def find_sessions(options: Options, all_sessions: Boolean, sessions: List[String],
   249     more_dirs: List[Path]): Session.Queue =
   250   {
   251     var queue = Session.Queue.empty
   252 
   253     for (dir <- Isabelle_System.components()) {
   254       queue = sessions_dir(options, false, dir, queue)
   255 
   256       val catalog = (dir + SESSIONS).file
   257       if (catalog.isFile)
   258         queue = sessions_catalog(options, dir, catalog, queue)
   259     }
   260 
   261     for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
   262 
   263     sessions.filter(name => !queue.defined(name)) match {
   264       case Nil =>
   265       case bad => error("Undefined session(s): " + commas_quote(bad))
   266     }
   267 
   268     if (all_sessions) queue else queue.required(sessions)
   269   }
   270 
   271 
   272   /* dependencies */
   273 
   274   sealed case class Node(
   275     loaded_theories: Set[String],
   276     sources: List[(Path, SHA1.Digest)])
   277 
   278   sealed case class Deps(deps: Map[String, Node])
   279   {
   280     def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources
   281   }
   282 
   283   def dependencies(queue: Session.Queue): Deps =
   284     Deps((Map.empty[String, Node] /: queue.topological_order)(
   285       { case (deps, (name, info)) =>
   286           val preloaded =
   287             info.parent match {
   288               case None => Set.empty[String]
   289               case Some(parent) => deps(parent).loaded_theories
   290             }
   291           val thy_info = new Thy_Info(new Thy_Load(preloaded))
   292 
   293           val thy_deps =
   294             thy_info.dependencies(
   295               info.theories.map(_._2).flatten.
   296                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
   297 
   298           val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
   299 
   300           val all_files =
   301             thy_deps.map({ case (n, h) =>
   302               val thy = Path.explode(n.node).expand
   303               val uses =
   304                 h match {
   305                   case Exn.Res(d) =>
   306                     d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
   307                   case _ => Nil
   308                 }
   309               thy :: uses
   310             }).flatten ::: info.files.map(file => info.dir + file)
   311           val sources = all_files.par.map(p => (p, SHA1.digest(p))).toList
   312 
   313           deps + (name -> Node(loaded_theories, sources))
   314       }))
   315 
   316 
   317 
   318   /** build **/
   319 
   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   {
   325     private val args_file = File.tmp_file("args")
   326     private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
   327     File.write(args_file, args)
   328 
   329     private val (thread, result) = Simple_Thread.future("build_job") {
   330       Isabelle_System.bash_env(cwd, env1, script)
   331     }
   332 
   333     def terminate: Unit = thread.interrupt
   334     def is_finished: Boolean = result.is_finished
   335     def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
   336   }
   337 
   338   private def build_job(save: Boolean, name: String, info: Session.Info): Build_Job =
   339   {
   340     val parent = info.parent.getOrElse("")
   341 
   342     val cwd = info.dir.file
   343     val env = Map("INPUT" -> parent, "TARGET" -> name)
   344     val script =
   345       if (is_pure(name)) "./build " + (if (save) "-b " else "") + name
   346       else {
   347         """
   348         . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   349         """ +
   350           (if (save)
   351             """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
   352           else
   353             """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
   354         """
   355         RC="$?"
   356 
   357         . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   358 
   359         if [ "$RC" -eq 0 ]; then
   360           echo "Finished $TARGET ($TIMES_REPORT)" >&2
   361         fi
   362 
   363         exit "$RC"
   364         """
   365       }
   366     val args_xml =
   367     {
   368       import XML.Encode._
   369       pair(bool, pair(string, pair(string, list(string))))(
   370         save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
   371     }
   372     new Build_Job(cwd, env, script, YXML.string_of_body(args_xml))
   373   }
   374 
   375   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   376     more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
   377   {
   378     val options = (Options.init() /: more_options)(_.define_simple(_))
   379     val queue = find_sessions(options, all_sessions, sessions, more_dirs)
   380     val deps = dependencies(queue)
   381 
   382 
   383     // prepare browser info dir
   384     if (options.bool("browser_info") &&
   385       !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
   386     {
   387       Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
   388       File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
   389         Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
   390       File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
   391         File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
   392         File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
   393         File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
   394     }
   395 
   396     // prepare log dir
   397     val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
   398     log_dir.file.mkdirs()
   399 
   400     // run jobs
   401     val rcs =
   402       for ((name, info) <- queue.topological_order) yield
   403       {
   404         if (list_only) { echo(name + " in " + info.dir); 0 }
   405         else {
   406           val save = build_images || queue.is_inner(name)
   407           echo((if (save) "Building " else "Running ") + name + " ...")
   408 
   409           val (out, err, rc) = build_job(save, name, info).join
   410           echo_n(err)
   411 
   412           val log = log_dir + Path.basic(name)
   413           if (rc == 0) {
   414             val sources =
   415               (info.digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
   416                 .mkString("sources: ", " ", "\n")
   417             File.write_zip(log.ext("gz"), sources + out)
   418           }
   419           else {
   420             File.write(log, out)
   421             echo(name + " FAILED")
   422             echo("(see also " + log.file + ")")
   423             val lines = split_lines(out)
   424             val tail = lines.drop(lines.length - 20 max 0)
   425             echo("\n" + cat_lines(tail))
   426           }
   427           rc
   428         }
   429       }
   430     (0 /: rcs)(_ max _)
   431   }
   432 
   433 
   434   /* command line entry point */
   435 
   436   def main(args: Array[String])
   437   {
   438     Command_Line.tool {
   439       args.toList match {
   440         case
   441           Properties.Value.Boolean(all_sessions) ::
   442           Properties.Value.Boolean(build_images) ::
   443           Properties.Value.Boolean(list_only) ::
   444           Command_Line.Chunks(more_dirs, options, sessions) =>
   445             build(all_sessions, build_images, list_only,
   446               more_dirs.map(Path.explode), options, sessions)
   447         case _ => error("Bad arguments:\n" + cat_lines(args))
   448       }
   449     }
   450   }
   451 }
   452