src/Pure/System/build.scala
author wenzelm
Fri Jul 20 22:29:25 2012 +0200 (2012-07-20)
changeset 48409 0d2114eb412a
parent 48373 527e2bad7cca
child 48411 5b3440850d36
permissions -rw-r--r--
more explicit java.io.{File => JFile};
     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   type Options = List[(String, Option[String])]
    21 
    22   object Session
    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     sealed case class Info(
    42       dir: Path,
    43       description: String,
    44       options: Options,
    45       theories: List[(Options, String)],
    46       files: List[String])
    47 
    48     object Queue
    49     {
    50       val empty: Queue = new Queue()
    51     }
    52 
    53     final class Queue private(
    54       keys: Map[String, Key] = Map.empty,
    55       graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
    56     {
    57       def defined(name: String): Boolean = keys.isDefinedAt(name)
    58 
    59       def + (key: Key, info: Info, parent: Option[String]): Queue =
    60       {
    61         val keys1 =
    62           if (defined(key.name)) error("Duplicate session: " + quote(key.name))
    63           else keys + (key.name -> key)
    64 
    65         val graph1 =
    66           try {
    67             graph.new_node(key, info).add_deps_acyclic(key, parent.toList.map(keys(_)))
    68           }
    69           catch {
    70             case exn: Graph.Cycles[_] =>
    71               error(cat_lines(exn.cycles.map(cycle =>
    72                 "Cyclic session dependency of " +
    73                   cycle.map(key => quote(key.toString)).mkString(" via "))))
    74           }
    75         new Queue(keys1, graph1)
    76       }
    77 
    78       def required(names: List[String]): Queue =
    79       {
    80         val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
    81         val keys1 = keys -- keys.keySet.filter(name => !req(name))
    82         val graph1 = graph.restrict(key => keys1.isDefinedAt(key.name))
    83         new Queue(keys1, graph1)
    84       }
    85 
    86       def topological_order: List[(Key, Info)] =
    87         graph.topological_order.map(key => (key, graph.get_node(key)))
    88     }
    89   }
    90 
    91 
    92   /* parsing */
    93 
    94   private case class Session_Entry(
    95     name: String,
    96     reset: Boolean,
    97     order: Int,
    98     path: Option[String],
    99     parent: Option[String],
   100     description: String,
   101     options: Options,
   102     theories: List[(Options, List[String])],
   103     files: List[String])
   104 
   105   private object Parser extends Parse.Parser
   106   {
   107     val SESSION = "session"
   108     val IN = "in"
   109     val DESCRIPTION = "description"
   110     val OPTIONS = "options"
   111     val THEORIES = "theories"
   112     val FILES = "files"
   113 
   114     val syntax =
   115       Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   116         SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   117 
   118     val session_entry: Parser[Session_Entry] =
   119     {
   120       val session_name = atom("session name", _.is_name)
   121       val theory_name = atom("theory name", _.is_name)
   122 
   123       val option =
   124         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   125       val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
   126 
   127       val theories =
   128         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
   129           { case _ ~ (x ~ y) => (x, y) }
   130 
   131       ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
   132         (keyword("!") ^^^ true | success(false)) ~
   133         (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~
   134         (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
   135         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
   136         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
   137         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
   138         rep(theories) ~
   139         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
   140           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
   141     }
   142 
   143     def parse_entries(root: JFile): List[Session_Entry] =
   144     {
   145       val toks = syntax.scan(Standard_System.read_file(root))
   146       parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
   147         case Success(result, _) => result
   148         case bad => error(bad.toString)
   149       }
   150     }
   151   }
   152 
   153 
   154   /* find sessions */
   155 
   156   private val ROOT = Path.explode("ROOT")
   157   private val SESSIONS = Path.explode("etc/sessions")
   158 
   159   private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
   160 
   161   private def sessions_root(dir: Path, root: JFile, queue: Session.Queue): Session.Queue =
   162   {
   163     (queue /: Parser.parse_entries(root))((queue1, entry) =>
   164       try {
   165         if (entry.name == "") error("Bad session name")
   166 
   167         val full_name =
   168           if (is_pure(entry.name)) {
   169             if (entry.parent.isDefined) error("Illegal parent session")
   170             else entry.name
   171           }
   172           else
   173             entry.parent match {
   174               case Some(parent_name) if queue1.defined(parent_name) =>
   175                 if (entry.reset) entry.name
   176                 else parent_name + "-" + entry.name
   177               case _ => error("Bad parent session")
   178             }
   179 
   180         val path =
   181           entry.path match {
   182             case Some(p) => Path.explode(p)
   183             case None => Path.basic(entry.name)
   184           }
   185 
   186         val key = Session.Key(full_name, entry.order)
   187         val info = Session.Info(dir + path, entry.description, entry.options,
   188           entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
   189 
   190         queue1 + (key, info, entry.parent)
   191       }
   192       catch {
   193         case ERROR(msg) =>
   194           error(msg + "\nThe error(s) above occurred in session entry " +
   195             quote(entry.name) + Position.str_of(Position.file(root)))
   196       })
   197   }
   198 
   199   private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
   200   {
   201     val root = (dir + ROOT).file
   202     if (root.isFile) sessions_root(dir, root, queue)
   203     else if (strict) error("Bad session root file: " + quote(root.toString))
   204     else queue
   205   }
   206 
   207   private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue =
   208   {
   209     val dirs =
   210       split_lines(Standard_System.read_file(catalog)).
   211         filterNot(line => line == "" || line.startsWith("#"))
   212     (queue /: dirs)((queue1, dir1) =>
   213       try {
   214         val dir2 = dir + Path.explode(dir1)
   215         if (dir2.file.isDirectory) sessions_dir(true, dir2, queue1)
   216         else error("Bad session directory: " + dir2.toString)
   217       }
   218       catch {
   219         case ERROR(msg) =>
   220           error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
   221       })
   222   }
   223 
   224   def find_sessions(more_dirs: List[Path]): Session.Queue =
   225   {
   226     var queue = Session.Queue.empty
   227 
   228     for (dir <- Isabelle_System.components()) {
   229       queue = sessions_dir(false, dir, queue)
   230 
   231       val catalog = (dir + SESSIONS).file
   232       if (catalog.isFile)
   233         queue = sessions_catalog(dir, catalog, queue)
   234     }
   235 
   236     for (dir <- more_dirs) queue = sessions_dir(true, dir, queue)
   237 
   238     queue
   239   }
   240 
   241 
   242 
   243   /** build **/
   244 
   245   private def echo(msg: String) { java.lang.System.out.println(msg) }
   246   private def echo_n(msg: String) { java.lang.System.out.print(msg) }
   247 
   248   private def build_job(build_images: Boolean,  // FIXME
   249     key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
   250   {
   251     val cwd = info.dir.file
   252     val script =
   253       if (is_pure(key.name)) "./build " + (if (build_images) "-b " else "") + key.name
   254       else """echo "Bad session" >&2; exit 2"""
   255     new Isabelle_System.Bash_Job(cwd, null, script)
   256   }
   257 
   258   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   259     more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   260   {
   261     val full_queue = find_sessions(more_dirs)
   262     val build_options = (Options.init() /: options)(_.define_simple(_))
   263 
   264     sessions.filter(name => !full_queue.defined(name)) match {
   265       case Nil =>
   266       case bad => error("Undefined session(s): " + commas_quote(bad))
   267     }
   268 
   269     val required_queue =
   270       if (all_sessions) full_queue
   271       else full_queue.required(sessions)
   272 
   273     // prepare browser info dir
   274     if (build_options.bool("browser_info") &&
   275       !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
   276     {
   277       Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
   278       Standard_System.copy_file(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif").file,
   279         Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif").file)
   280       Standard_System.write_file(Path.explode("$ISABELLE_BROWSER_INFO/index.html").file,
   281         Standard_System.read_file(
   282           Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template").file) +
   283         Standard_System.read_file(
   284           Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template").file) +
   285         Standard_System.read_file(
   286           Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template").file))
   287     }
   288 
   289     // prepare log dir
   290     val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
   291     log_dir.file.mkdirs()
   292 
   293     // run jobs
   294     val rcs =
   295       for ((key, info) <- required_queue.topological_order) yield
   296       {
   297         if (list_only) { echo(key.name + " in " + info.dir); 0 }
   298         else {
   299           if (build_images) echo("Building " + key.name + "...")
   300           else echo("Running " + key.name + "...")
   301 
   302           val (out, err, rc) = build_job(build_images, key, info).join
   303           echo_n(err)
   304 
   305           val log = log_dir + Path.basic(key.name)
   306           if (rc == 0) {
   307             Standard_System.write_file(log.ext("gz").file, out, true)
   308           }
   309           else {
   310             Standard_System.write_file(log.file, out)
   311             echo(key.name + " FAILED")
   312             echo("(see also " + log.file + ")")
   313             val lines = split_lines(out)
   314             val tail = lines.drop(lines.length - 20 max 0)
   315             echo("\n" + cat_lines(tail))
   316           }
   317           rc
   318         }
   319       }
   320     (0 /: rcs)(_ max _)
   321   }
   322 
   323 
   324   /* command line entry point */
   325 
   326   def main(args: Array[String])
   327   {
   328     Command_Line.tool {
   329       args.toList match {
   330         case
   331           Properties.Value.Boolean(all_sessions) ::
   332           Properties.Value.Boolean(build_images) ::
   333           Properties.Value.Boolean(list_only) ::
   334           Command_Line.Chunks(more_dirs, options, sessions) =>
   335             build(all_sessions, build_images, list_only,
   336               more_dirs.map(Path.explode), options, sessions)
   337         case _ => error("Bad arguments:\n" + cat_lines(args))
   338       }
   339     }
   340   }
   341 }
   342