src/Pure/System/build.scala
author wenzelm
Mon Jul 30 12:03:48 2012 +0200 (2012-07-30)
changeset 48595 231e6fa96dbb
parent 48594 c24907e5081e
child 48626 ef374008cb7c
permissions -rw-r--r--
added build option -c;
tuned;
     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.{BufferedInputStream, FileInputStream,
    11   BufferedReader, InputStreamReader, IOException}
    12 import java.util.zip.GZIPInputStream
    13 
    14 import scala.collection.mutable
    15 import scala.annotation.tailrec
    16 
    17 
    18 object Build
    19 {
    20   /** session information **/
    21 
    22   object Session
    23   {
    24     /* Info */
    25 
    26     sealed case class Info(
    27       groups: List[String],
    28       dir: Path,
    29       parent: Option[String],
    30       description: String,
    31       options: Options,
    32       theories: List[(Options, List[Path])],
    33       files: List[Path],
    34       entry_digest: SHA1.Digest)
    35 
    36 
    37     /* Queue */
    38 
    39     object Queue
    40     {
    41       val empty: Queue = new Queue()
    42     }
    43 
    44     final class Queue private(graph: Graph[String, Info] = Graph.string)
    45       extends PartialFunction[String, Info]
    46     {
    47       def apply(name: String): Info = graph.get_node(name)
    48       def isDefinedAt(name: String): Boolean = graph.defined(name)
    49 
    50       def is_inner(name: String): Boolean = !graph.is_maximal(name)
    51 
    52       def is_empty: Boolean = graph.is_empty
    53 
    54       def + (name: String, info: Info): Queue =
    55         new Queue(
    56           try { graph.new_node(name, info).add_deps_acyclic(name, info.parent.toList) }
    57           catch {
    58             case _: Graph.Duplicate[_] => error("Duplicate session: " + quote(name))
    59             case exn: Graph.Cycles[_] =>
    60               error(cat_lines(exn.cycles.map(cycle =>
    61                 "Cyclic session dependency of " +
    62                   cycle.map(c => quote(c.toString)).mkString(" via "))))
    63           })
    64 
    65       def - (name: String): Queue = new Queue(graph.del_node(name))
    66 
    67       def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String])
    68         : (List[String], Queue) =
    69       {
    70         sessions.filterNot(isDefinedAt(_)) match {
    71           case Nil =>
    72           case bad => error("Undefined session(s): " + commas_quote(bad))
    73         }
    74 
    75         val selected =
    76         {
    77           if (all_sessions) graph.keys.toList
    78           else {
    79             val sel_group = session_groups.toSet
    80             val sel = sessions.toSet
    81               graph.keys.toList.filter(name =>
    82                 sel(name) || apply(name).groups.exists(sel_group)).toList
    83           }
    84         }
    85         val descendants = graph.all_succs(selected)
    86         val queue1 = new Queue(graph.restrict(graph.all_preds(selected).toSet))
    87         (descendants, queue1)
    88       }
    89 
    90       def dequeue(skip: String => Boolean): Option[(String, Info)] =
    91       {
    92         val it = graph.entries.dropWhile(
    93           { case (name, (_, (deps, _))) => !deps.isEmpty || skip(name) })
    94         if (it.hasNext) { val (name, (info, _)) = it.next; Some((name, info)) }
    95         else None
    96       }
    97 
    98       def topological_order: List[(String, Info)] =
    99         graph.topological_order.map(name => (name, apply(name)))
   100     }
   101   }
   102 
   103 
   104   /* parsing */
   105 
   106   private case class Session_Entry(
   107     base_name: String,
   108     this_name: Boolean,
   109     groups: List[String],
   110     path: Option[String],
   111     parent: Option[String],
   112     description: String,
   113     options: List[Options.Spec],
   114     theories: List[(List[Options.Spec], List[String])],
   115     files: List[String])
   116 
   117   private object Parser extends Parse.Parser
   118   {
   119     val SESSION = "session"
   120     val IN = "in"
   121     val DESCRIPTION = "description"
   122     val OPTIONS = "options"
   123     val THEORIES = "theories"
   124     val FILES = "files"
   125 
   126     val syntax =
   127       Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   128         SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   129 
   130     val session_entry: Parser[Session_Entry] =
   131     {
   132       val session_name = atom("session name", _.is_name)
   133 
   134       val option =
   135         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   136       val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
   137 
   138       val theories =
   139         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
   140           { case _ ~ (x ~ y) => (x, y) }
   141 
   142       ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
   143         (keyword("!") ^^^ true | success(false)) ~
   144         (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
   145         (opt(keyword(IN) ~! path ^^ { case _ ~ x => x })) ~
   146         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
   147         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
   148         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
   149         rep(theories) ~
   150         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
   151           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
   152     }
   153 
   154     def parse_entries(root: Path): List[Session_Entry] =
   155     {
   156       val toks = syntax.scan(File.read(root))
   157       parse_all(rep(session_entry), Token.reader(toks, root.implode)) match {
   158         case Success(result, _) => result
   159         case bad => error(bad.toString)
   160       }
   161     }
   162   }
   163 
   164 
   165   /* find sessions */
   166 
   167   private val ROOT = Path.explode("ROOT")
   168   private val SESSIONS = Path.explode("etc/sessions")
   169 
   170   private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
   171 
   172   private def sessions_root(options: Options, dir: Path, root: Path, queue: Session.Queue)
   173     : Session.Queue =
   174   {
   175     (queue /: Parser.parse_entries(root))((queue1, entry) =>
   176       try {
   177         if (entry.base_name == "") error("Bad session name")
   178 
   179         val full_name =
   180           if (is_pure(entry.base_name)) {
   181             if (entry.parent.isDefined) error("Illegal parent session")
   182             else entry.base_name
   183           }
   184           else
   185             entry.parent match {
   186               case Some(parent_name) if queue1.isDefinedAt(parent_name) =>
   187                 val full_name =
   188                   if (entry.this_name) entry.base_name
   189                   else parent_name + "-" + entry.base_name
   190                 full_name
   191               case _ => error("Bad parent session")
   192             }
   193 
   194         val path =
   195           entry.path match {
   196             case Some(p) => Path.explode(p)
   197             case None => Path.basic(entry.base_name)
   198           }
   199 
   200         val session_options = options ++ entry.options
   201 
   202         val theories =
   203           entry.theories.map({ case (opts, thys) =>
   204             (session_options ++ opts, thys.map(Path.explode(_))) })
   205         val files = entry.files.map(Path.explode(_))
   206         val entry_digest =
   207           SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
   208 
   209         val info =
   210           Session.Info(entry.groups, dir + path, entry.parent, entry.description,
   211             session_options, theories, files, entry_digest)
   212 
   213         queue1 + (full_name, info)
   214       }
   215       catch {
   216         case ERROR(msg) =>
   217           error(msg + "\nThe error(s) above occurred in session entry " +
   218             quote(entry.base_name) + Position.str_of(root.position))
   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
   226     if (root.is_file) sessions_root(options, dir, root, queue)
   227     else if (strict) error("Bad session root file: " + root.toString)
   228     else queue
   229   }
   230 
   231   private def sessions_catalog(options: Options, dir: Path, catalog: Path, 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.is_dir) 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 " + catalog.toString)
   245       })
   246   }
   247 
   248   def find_sessions(options: Options, more_dirs: List[Path]): Session.Queue =
   249   {
   250     var queue = Session.Queue.empty
   251 
   252     for (dir <- Isabelle_System.components()) {
   253       queue = sessions_dir(options, false, dir, queue)
   254 
   255       val catalog = dir + SESSIONS
   256       if (catalog.is_file) queue = sessions_catalog(options, dir, catalog, queue)
   257     }
   258 
   259     for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
   260 
   261     queue
   262   }
   263 
   264 
   265 
   266   /** build **/
   267 
   268   private def echo(msg: String) { java.lang.System.out.println(msg) }
   269   private def sleep(): Unit = Thread.sleep(500)
   270 
   271 
   272   /* source 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 is_empty: Boolean = deps.isEmpty
   281     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   282   }
   283 
   284   def dependencies(verbose: Boolean, queue: Session.Queue): Deps =
   285     Deps((Map.empty[String, Node] /: queue.topological_order)(
   286       { case (deps, (name, info)) =>
   287           val preloaded =
   288             info.parent match {
   289               case None => Set.empty[String]
   290               case Some(parent) => deps(parent).loaded_theories
   291             }
   292           val thy_info = new Thy_Info(new Thy_Load(preloaded))
   293 
   294           if (verbose) {
   295             val groups =
   296               if (info.groups.isEmpty) ""
   297               else info.groups.mkString(" (", " ", ")")
   298             echo("Checking " + name + groups + " ...")
   299           }
   300 
   301           val thy_deps =
   302             thy_info.dependencies(
   303               info.theories.map(_._2).flatten.
   304                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
   305 
   306           val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
   307 
   308           val all_files =
   309             thy_deps.map({ case (n, h) =>
   310               val thy = Path.explode(n.node).expand
   311               val uses =
   312                 h match {
   313                   case Exn.Res(d) =>
   314                     d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
   315                   case _ => Nil
   316                 }
   317               thy :: uses
   318             }).flatten ::: info.files.map(file => info.dir + file)
   319           val sources =
   320             try { all_files.map(p => (p, SHA1.digest(p))) }
   321             catch {
   322               case ERROR(msg) =>
   323                 error(msg + "\nThe error(s) above occurred in session " + quote(name))
   324             }
   325 
   326           deps + (name -> Node(loaded_theories, sources))
   327       }))
   328 
   329 
   330   /* jobs */
   331 
   332   private class Job(dir: Path, env: Map[String, String], script: String, args: String,
   333     output: Path, do_output: Boolean)
   334   {
   335     private val args_file = File.tmp_file("args")
   336     private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
   337     File.write(args_file, args)
   338 
   339     private val (thread, result) =
   340       Simple_Thread.future("build") { Isabelle_System.bash_env(dir.file, env1, script) }
   341 
   342     def terminate: Unit = thread.interrupt
   343     def is_finished: Boolean = result.is_finished
   344     def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
   345     def output_path: Option[Path] = if (do_output) Some(output) else None
   346   }
   347 
   348   private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean,
   349     options: Options, verbose: Boolean, browser_info: Path): Job =
   350   {
   351     // global browser info dir
   352     if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
   353     {
   354       browser_info.file.mkdirs()
   355       File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
   356         browser_info + Path.explode("isabelle.gif"))
   357       File.write(browser_info + Path.explode("index.html"),
   358         File.read(Path.explode("~~/lib/html/library_index_header.template")) +
   359         File.read(Path.explode("~~/lib/html/library_index_content.template")) +
   360         File.read(Path.explode("~~/lib/html/library_index_footer.template")))
   361     }
   362 
   363     val parent = info.parent.getOrElse("")
   364 
   365     val env =
   366       Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output))
   367     val script =
   368       if (is_pure(name)) {
   369         if (do_output) "./build " + name + " \"$OUTPUT\""
   370         else """ rm -f "$OUTPUT"; ./build """ + name
   371       }
   372       else {
   373         """
   374         . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   375         """ +
   376           (if (do_output)
   377             """
   378             "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
   379             """
   380           else
   381             """
   382             rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
   383             """) +
   384         """
   385         RC="$?"
   386 
   387         . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   388 
   389         if [ "$RC" -eq 0 ]; then
   390           echo "Finished $TARGET ($TIMES_REPORT)" >&2
   391         fi
   392 
   393         exit "$RC"
   394         """
   395       }
   396     val args_xml =
   397     {
   398       import XML.Encode._
   399           pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
   400             pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
   401           (do_output, (options, (verbose, (browser_info, (parent,
   402             (name, info.theories)))))))
   403     }
   404     new Job(info.dir, env, script, YXML.string_of_body(args_xml), output, do_output)
   405   }
   406 
   407 
   408   /* log files and corresponding heaps */
   409 
   410   private val LOG = Path.explode("log")
   411   private def log(name: String): Path = LOG + Path.basic(name)
   412   private def log_gz(name: String): Path = log(name).ext("gz")
   413 
   414   private def sources_stamp(digests: List[SHA1.Digest]): String =
   415     digests.map(_.toString).sorted.mkString("sources: ", " ", "")
   416 
   417   private def heap_stamp(output: Option[Path]): String =
   418   {
   419     "heap: " +
   420       (output match {
   421         case Some(path) =>
   422           val file = path.file
   423           if (file.isFile) file.length.toString + " " + file.lastModified.toString
   424           else "-"
   425         case None => "-"
   426       })
   427   }
   428 
   429   private def check_stamps(dir: Path, name: String): Option[(String, Boolean)] =
   430   {
   431     val file = (dir + log_gz(name)).file
   432     if (file.isFile) {
   433       val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(file)))
   434       val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
   435       val (s, h) = try { (reader.readLine, reader.readLine) } finally { reader.close }
   436       if (s != null && s.startsWith("sources: ") && h != null && h.startsWith("heap: ") &&
   437           h == heap_stamp(Some(dir + Path.basic(name)))) Some((s, h != "heap: -"))
   438       else None
   439     }
   440     else None
   441   }
   442 
   443 
   444   /* build */
   445 
   446   def build(
   447     all_sessions: Boolean = false,
   448     build_heap: Boolean = false,
   449     clean_build: Boolean = false,
   450     more_dirs: List[Path] = Nil,
   451     session_groups: List[String] = Nil,
   452     max_jobs: Int = 1,
   453     no_build: Boolean = false,
   454     build_options: List[String] = Nil,
   455     system_mode: Boolean = false,
   456     verbose: Boolean = false,
   457     sessions: List[String] = Nil): Int =
   458   {
   459     val options = (Options.init() /: build_options)(_.define_simple(_))
   460     val (descendants, queue) =
   461       find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
   462     val deps = dependencies(verbose, queue)
   463 
   464     def make_stamp(name: String): String =
   465       sources_stamp(queue(name).entry_digest :: deps.sources(name))
   466 
   467     val (input_dirs, output_dir, browser_info) =
   468       if (system_mode) {
   469         val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
   470         (List(output_dir), output_dir, Path.explode("~~/browser_info"))
   471       }
   472       else {
   473         val output_dir = Path.explode("$ISABELLE_OUTPUT")
   474         (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
   475          Path.explode("$ISABELLE_BROWSER_INFO"))
   476       }
   477 
   478     // prepare log dir
   479     (output_dir + LOG).file.mkdirs()
   480 
   481     // optional cleanup
   482     if (clean_build) {
   483       for (name <- descendants) {
   484         val files =
   485           List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
   486         if (!files.isEmpty) echo("Cleaning " + name + " ...")
   487         if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
   488       }
   489     }
   490 
   491     // scheduler loop
   492     @tailrec def loop(
   493       pending: Session.Queue,
   494       running: Map[String, Job],
   495       results: Map[String, (Boolean, Int)]): Map[String, (Boolean, Int)] =
   496     {
   497       if (pending.is_empty) results
   498       else
   499         running.find({ case (_, job) => job.is_finished }) match {
   500           case Some((name, job)) =>
   501             // finish job
   502 
   503             val (out, err, rc) = job.join
   504             echo(Library.trim_line(err))
   505 
   506             if (rc == 0) {
   507               val sources = make_stamp(name)
   508               val heap = heap_stamp(job.output_path)
   509               (output_dir + log(name)).file.delete
   510               File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out)
   511             }
   512             else {
   513               (output_dir + log_gz(name)).file.delete
   514               File.write(output_dir + log(name), out)
   515               echo(name + " FAILED")
   516               echo("(see also " + log(name).file.toString + ")")
   517               val lines = split_lines(out)
   518               val tail = lines.drop(lines.length - 20 max 0)
   519               echo("\n" + cat_lines(tail))
   520             }
   521             loop(pending - name, running - name, results + (name -> (false, rc)))
   522 
   523           case None if (running.size < (max_jobs max 1)) =>
   524             // check/start next job
   525             pending.dequeue(running.isDefinedAt(_)) match {
   526               case Some((name, info)) =>
   527                 val parent_result = info.parent.map(results(_))
   528                 val parent_current = parent_result.forall(_._1)
   529                 val parent_ok = parent_result.forall(_._2 == 0)
   530 
   531                 val output = output_dir + Path.basic(name)
   532                 val do_output = build_heap || queue.is_inner(name)
   533 
   534                 val current =
   535                 {
   536                   input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   537                     case Some(dir) =>
   538                       check_stamps(dir, name) match {
   539                         case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
   540                         case None => false
   541                       }
   542                     case None => false
   543                   }
   544                 }
   545                 val all_current = current && parent_current
   546 
   547                 if (all_current)
   548                   loop(pending - name, running, results + (name -> (true, 0)))
   549                 else if (no_build)
   550                   loop(pending - name, running, results + (name -> (false, 1)))
   551                 else if (parent_ok) {
   552                   echo((if (do_output) "Building " else "Running ") + name + " ...")
   553                   val job =
   554                     start_job(name, info, output, do_output, info.options, verbose, browser_info)
   555                   loop(pending, running + (name -> job), results)
   556                 }
   557                 else {
   558                   echo(name + " CANCELLED")
   559                   loop(pending - name, running, results + (name -> (false, 1)))
   560                 }
   561               case None => sleep(); loop(pending, running, results)
   562             }
   563           case None => sleep(); loop(pending, running, results)
   564         }
   565     }
   566 
   567     val results =
   568       if (deps.is_empty) {
   569         echo("### Nothing to build")
   570         Map.empty
   571       }
   572       else loop(queue, Map.empty, Map.empty)
   573 
   574     val rc = (0 /: results)({ case (rc1, (_, (_, rc2))) => rc1 max rc2 })
   575     if (rc != 0 && (verbose || !no_build)) {
   576       val unfinished =
   577         (for ((name, (_, r)) <- results.iterator if r != 0) yield name).toList.sorted
   578       echo("Unfinished session(s): " + commas(unfinished))
   579     }
   580     rc
   581   }
   582 
   583 
   584   /* command line entry point */
   585 
   586   def main(args: Array[String])
   587   {
   588     Command_Line.tool {
   589       args.toList match {
   590         case
   591           Properties.Value.Boolean(all_sessions) ::
   592           Properties.Value.Boolean(build_heap) ::
   593           Properties.Value.Boolean(clean_build) ::
   594           Properties.Value.Int(max_jobs) ::
   595           Properties.Value.Boolean(no_build) ::
   596           Properties.Value.Boolean(system_mode) ::
   597           Properties.Value.Boolean(verbose) ::
   598           Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
   599             build(all_sessions, build_heap, clean_build, more_dirs.map(Path.explode),
   600               session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
   601         case _ => error("Bad arguments:\n" + cat_lines(args))
   602       }
   603     }
   604   }
   605 }
   606