src/Pure/System/build.scala
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 48639 675988e64bf9
child 48649 bf9bff84a61d
permissions -rw-r--r--
more official command specifications, including source position;
     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     val parent_heap: String, 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, parent_heap: String,
   349     output: Path, do_output: Boolean, 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), parent_heap, 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 val no_heap: String = "heap: -"
   418 
   419   private def heap_stamp(heap: Option[Path]): String =
   420   {
   421     "heap: " +
   422       (heap match {
   423         case Some(path) =>
   424           val file = path.file
   425           if (file.isFile) file.length.toString + " " + file.lastModified.toString
   426           else "-"
   427         case None => "-"
   428       })
   429   }
   430 
   431   private def read_stamps(path: Path): Option[(String, String, String)] =
   432     if (path.is_file) {
   433       val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(path.file)))
   434       val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
   435       val (s, h1, h2) =
   436         try { (reader.readLine, reader.readLine, reader.readLine) }
   437         finally { reader.close }
   438       if (s != null && s.startsWith("sources: ") &&
   439           h1 != null && h1.startsWith("heap: ") &&
   440           h2 != null && h2.startsWith("heap: ")) Some((s, h1, h2))
   441       else None
   442     }
   443     else None
   444 
   445 
   446   /* build */
   447 
   448   def build(
   449     all_sessions: Boolean = false,
   450     build_heap: Boolean = false,
   451     clean_build: Boolean = false,
   452     more_dirs: List[Path] = Nil,
   453     session_groups: List[String] = Nil,
   454     max_jobs: Int = 1,
   455     no_build: Boolean = false,
   456     build_options: List[String] = Nil,
   457     system_mode: Boolean = false,
   458     verbose: Boolean = false,
   459     sessions: List[String] = Nil): Int =
   460   {
   461     val options = (Options.init() /: build_options)(_.define_simple(_))
   462     val (descendants, queue) =
   463       find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
   464     val deps = dependencies(verbose, queue)
   465 
   466     def make_stamp(name: String): String =
   467       sources_stamp(queue(name).entry_digest :: deps.sources(name))
   468 
   469     val (input_dirs, output_dir, browser_info) =
   470       if (system_mode) {
   471         val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
   472         (List(output_dir), output_dir, Path.explode("~~/browser_info"))
   473       }
   474       else {
   475         val output_dir = Path.explode("$ISABELLE_OUTPUT")
   476         (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
   477          Path.explode("$ISABELLE_BROWSER_INFO"))
   478       }
   479 
   480     // prepare log dir
   481     (output_dir + LOG).file.mkdirs()
   482 
   483     // optional cleanup
   484     if (clean_build) {
   485       for (name <- descendants) {
   486         val files =
   487           List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
   488         if (!files.isEmpty) echo("Cleaning " + name + " ...")
   489         if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
   490       }
   491     }
   492 
   493     // scheduler loop
   494     case class Result(current: Boolean, heap: String, rc: Int)
   495 
   496     @tailrec def loop(
   497       pending: Session.Queue,
   498       running: Map[String, Job],
   499       results: Map[String, Result]): Map[String, Result] =
   500     {
   501       if (pending.is_empty) results
   502       else
   503         running.find({ case (_, job) => job.is_finished }) match {
   504           case Some((name, job)) =>
   505             // finish job
   506 
   507             val (out, err, rc) = job.join
   508             echo(Library.trim_line(err))
   509 
   510             val heap =
   511               if (rc == 0) {
   512                 (output_dir + log(name)).file.delete
   513 
   514                 val sources = make_stamp(name)
   515                 val heap = heap_stamp(job.output_path)
   516                 File.write_gzip(output_dir + log_gz(name),
   517                   sources + "\n" + job.parent_heap + "\n" + heap + "\n" + out)
   518 
   519                 heap
   520               }
   521               else {
   522                 (output_dir + Path.basic(name)).file.delete
   523                 (output_dir + log_gz(name)).file.delete
   524 
   525                 File.write(output_dir + log(name), out)
   526                 echo(name + " FAILED")
   527                 echo("(see also " + (output_dir + log(name)).file.toString + ")")
   528                 val lines = split_lines(out)
   529                 val tail = lines.drop(lines.length - 20 max 0)
   530                 echo("\n" + cat_lines(tail))
   531 
   532                 no_heap
   533               }
   534             loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
   535 
   536           case None if (running.size < (max_jobs max 1)) =>
   537             // check/start next job
   538             pending.dequeue(running.isDefinedAt(_)) match {
   539               case Some((name, info)) =>
   540                 val parent_result =
   541                   info.parent match {
   542                     case None => Result(true, no_heap, 0)
   543                     case Some(parent) => results(parent)
   544                   }
   545                 val output = output_dir + Path.basic(name)
   546                 val do_output = build_heap || queue.is_inner(name)
   547 
   548                 val (current, heap) =
   549                 {
   550                   input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   551                     case Some(dir) =>
   552                       read_stamps(dir + log_gz(name)) match {
   553                         case Some((s, h1, h2)) =>
   554                           val heap = heap_stamp(Some(dir + Path.basic(name)))
   555                           (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
   556                             !(do_output && heap == no_heap), heap)
   557                         case None => (false, no_heap)
   558                       }
   559                     case None => (false, no_heap)
   560                   }
   561                 }
   562                 val all_current = current && parent_result.current
   563 
   564                 if (all_current)
   565                   loop(pending - name, running, results + (name -> Result(true, heap, 0)))
   566                 else if (no_build)
   567                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   568                 else if (parent_result.rc == 0) {
   569                   echo((if (do_output) "Building " else "Running ") + name + " ...")
   570                   val job =
   571                     start_job(name, info, parent_result.heap, output, do_output,
   572                       info.options, verbose, browser_info)
   573                   loop(pending, running + (name -> job), results)
   574                 }
   575                 else {
   576                   echo(name + " CANCELLED")
   577                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   578                 }
   579               case None => sleep(); loop(pending, running, results)
   580             }
   581           case None => sleep(); loop(pending, running, results)
   582         }
   583     }
   584 
   585     val results =
   586       if (deps.is_empty) {
   587         echo("### Nothing to build")
   588         Map.empty
   589       }
   590       else loop(queue, Map.empty, Map.empty)
   591 
   592     val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
   593     if (rc != 0 && (verbose || !no_build)) {
   594       val unfinished =
   595         (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList.sorted
   596       echo("Unfinished session(s): " + commas(unfinished))
   597     }
   598     rc
   599   }
   600 
   601 
   602   /* command line entry point */
   603 
   604   def main(args: Array[String])
   605   {
   606     Command_Line.tool {
   607       args.toList match {
   608         case
   609           Properties.Value.Boolean(all_sessions) ::
   610           Properties.Value.Boolean(build_heap) ::
   611           Properties.Value.Boolean(clean_build) ::
   612           Properties.Value.Int(max_jobs) ::
   613           Properties.Value.Boolean(no_build) ::
   614           Properties.Value.Boolean(system_mode) ::
   615           Properties.Value.Boolean(verbose) ::
   616           Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
   617             build(all_sessions, build_heap, clean_build, more_dirs.map(Path.explode),
   618               session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
   619         case _ => error("Bad arguments:\n" + cat_lines(args))
   620       }
   621     }
   622   }
   623 }
   624