src/Pure/System/build.scala
author wenzelm
Thu Jul 19 15:45:59 2012 +0200 (2012-07-19)
changeset 48350 09bf3b73e446
parent 48349 a78e5d399599
child 48351 a0b95a762abb
permissions -rw-r--r--
clarified topological ordering: preserve order of adjacency via reverse fold;
     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       key: Key,
    44       parent: Option[String],
    45       description: String,
    46       options: Options,
    47       theories: List[(Options, String)],
    48       files: List[String])
    49     {
    50       def name: String = key.name
    51     }
    52 
    53     object Queue
    54     {
    55       val empty: Queue = new Queue()
    56     }
    57 
    58     final class Queue private(
    59       keys: Map[String, Key] = Map.empty,
    60       graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
    61     {
    62       def lookup(name: String): Option[Info] =
    63         keys.get(name).map(graph.get_node(_))
    64 
    65       def + (info: Info): Queue =
    66       {
    67         val keys1 =
    68           if (keys.isDefinedAt(info.name)) error("Duplicate session: " + quote(info.name))
    69           else keys + (info.name -> info.key)
    70 
    71         val graph1 =
    72           try {
    73             graph.new_node(info.key, info).
    74               add_deps_acyclic(info.key, info.parent.toList.map(keys(_)))
    75           }
    76           catch {
    77             case exn: Graph.Cycles[_] =>
    78               error(cat_lines(exn.cycles.map(cycle =>
    79                 "Cyclic session dependency of " +
    80                   cycle.map(key => quote(key.toString)).mkString(" via "))))
    81           }
    82         new Queue(keys1, graph1)
    83       }
    84 
    85       def topological_order: List[Info] =
    86         graph.topological_order.map(graph.get_node(_))
    87     }
    88   }
    89 
    90 
    91   /* parsing */
    92 
    93   val ROOT_NAME = "ROOT"
    94 
    95   private case class Session_Entry(
    96     name: String,
    97     reset: Boolean,
    98     order: Int,
    99     path: Option[String],
   100     parent: Option[String],
   101     description: String,
   102     options: Options,
   103     theories: List[(Options, List[String])],
   104     files: List[String])
   105 
   106   private object Parser extends Parse.Parser
   107   {
   108     val SESSION = "session"
   109     val IN = "in"
   110     val DESCRIPTION = "description"
   111     val OPTIONS = "options"
   112     val THEORIES = "theories"
   113     val FILES = "files"
   114 
   115     val syntax =
   116       Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   117         SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   118 
   119     val session_entry: Parser[Session_Entry] =
   120     {
   121       val session_name = atom("session name", _.is_name)
   122       val theory_name = atom("theory name", _.is_name)
   123 
   124       val option =
   125         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   126       val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
   127 
   128       val theories =
   129         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
   130           { case _ ~ (x ~ y) => (x, y) }
   131 
   132       ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
   133         (keyword("!") ^^^ true | success(false)) ~
   134         (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~
   135         (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
   136         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
   137         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
   138         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
   139         rep(theories) ~
   140         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
   141           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
   142     }
   143 
   144     def parse_entries(root: File): List[Session_Entry] =
   145     {
   146       val toks = syntax.scan(Standard_System.read_file(root))
   147       parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
   148         case Success(result, _) => result
   149         case bad => error(bad.toString)
   150       }
   151     }
   152   }
   153 
   154 
   155   /* find sessions */
   156 
   157   def find_sessions(more_dirs: List[Path]): Session.Queue =
   158   {
   159     var sessions = Session.Queue.empty
   160 
   161     for {
   162       (dir, strict) <- Isabelle_System.components().map((_, false)) ++ more_dirs.map((_, true))
   163       root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
   164       _ = (strict && !root.isFile && error("Bad session root file: " + quote(root.toString)))
   165       if root.isFile
   166       entry <- Parser.parse_entries(root)
   167     }
   168     {
   169       try {
   170         if (entry.name == "") error("Bad session name")
   171 
   172         val full_name =
   173           if (entry.name == "RAW" || entry.name == "Pure") {
   174             if (entry.parent.isDefined) error("Illegal parent session")
   175             else entry.name
   176           }
   177           else
   178             entry.parent match {
   179               case None => error("Missing parent session")
   180               case Some(parent) =>
   181                 val parent_info =
   182                   sessions.lookup(parent) getOrElse
   183                     error("Undefined parent session: " + quote(parent))
   184                 if (entry.reset) entry.name
   185                 else parent_info.name + "-" + entry.name
   186             }
   187 
   188         val path =
   189           entry.path match {
   190             case Some(p) => Path.explode(p)
   191             case None => Path.basic(entry.name)
   192           }
   193         val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
   194         val info =
   195           Session.Info(dir + path, Session.Key(full_name, entry.order),
   196             entry.parent, entry.description, entry.options, thys, entry.files)
   197 
   198         sessions += info
   199       }
   200       catch {
   201         case ERROR(msg) =>
   202           error(msg + "\nThe error(s) above occurred in session entry " +
   203             quote(entry.name) + " (file " + quote(root.toString) + ")")
   204       }
   205     }
   206     sessions
   207   }
   208 
   209 
   210 
   211   /** build **/
   212 
   213   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   214     more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   215   {
   216     println("more_dirs = " + more_dirs.toString)
   217     println("options = " + options.toString)
   218     println("sessions = " + sessions.toString)
   219 
   220     for (info <- find_sessions(more_dirs).topological_order)
   221       println(info.name + " in " + info.dir)
   222 
   223     0
   224   }
   225 
   226 
   227   /* command line entry point */
   228 
   229   def main(args: Array[String])
   230   {
   231     Command_Line.tool {
   232       args.toList match {
   233         case
   234           Properties.Value.Boolean(all_sessions) ::
   235           Properties.Value.Boolean(build_images) ::
   236           Properties.Value.Boolean(list_only) ::
   237           Command_Line.Chunks(more_dirs, options, sessions) =>
   238             build(all_sessions, build_images, list_only,
   239               more_dirs.map(Path.explode), options, sessions)
   240         case _ => error("Bad arguments:\n" + cat_lines(args))
   241       }
   242     }
   243   }
   244 }
   245