src/Pure/System/build.scala
author wenzelm
Fri Jul 20 12:45:12 2012 +0200 (2012-07-20)
changeset 48364 9091b659d7b6
parent 48363 cf081b7042d2
child 48368 dc538eef2cf2
permissions -rw-r--r--
minimal build_job;
     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
    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: File): 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: File, 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) + " (file " + quote(root.toString) + ")")
   196       })
   197   }
   198 
   199   private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
   200   {
   201     val root = Isabelle_System.platform_file(dir + ROOT)
   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: File, 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 (Isabelle_System.platform_file(dir2).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 = Isabelle_System.platform_file(dir + SESSIONS)
   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 build_job(build_images: Boolean,  // FIXME
   246     key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
   247   {
   248     val cwd = Isabelle_System.platform_file(info.dir)
   249     val script =
   250       if (is_pure(key.name)) "./build " + key.name
   251       else """echo "Bad session" >&2; exit 2"""
   252     new Isabelle_System.Bash_Job(cwd, null, script)
   253   }
   254 
   255   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   256     more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   257   {
   258     val full_queue = find_sessions(more_dirs)
   259 
   260     sessions.filter(name => !full_queue.defined(name)) match {
   261       case Nil =>
   262       case bad => error("Undefined session(s): " + commas_quote(bad))
   263     }
   264 
   265     val required_queue =
   266       if (all_sessions) full_queue
   267       else full_queue.required(sessions)
   268 
   269     for ((key, info) <- required_queue.topological_order) {
   270       if (list_only) println(key.name + " in " + info.dir)
   271       else {
   272         val (out, err, rc) = build_job(build_images, key, info).join
   273         java.lang.System.err.print(err)
   274       }
   275     }
   276 
   277     0
   278   }
   279 
   280 
   281   /* command line entry point */
   282 
   283   def main(args: Array[String])
   284   {
   285     Command_Line.tool {
   286       args.toList match {
   287         case
   288           Properties.Value.Boolean(all_sessions) ::
   289           Properties.Value.Boolean(build_images) ::
   290           Properties.Value.Boolean(list_only) ::
   291           Command_Line.Chunks(more_dirs, options, sessions) =>
   292             build(all_sessions, build_images, list_only,
   293               more_dirs.map(Path.explode), options, sessions)
   294         case _ => error("Bad arguments:\n" + cat_lines(args))
   295       }
   296     }
   297   }
   298 }
   299