src/Pure/Thy/sessions.scala
author wenzelm
Wed Mar 30 21:33:48 2016 +0200 (2016-03-30 ago)
changeset 62769 146945b9e83c
parent 62704 478b49f0d726
child 62864 2d5959cf3c1a
permissions -rw-r--r--
tuned message;
     1 /*  Title:      Pure/Thy/sessions.scala
     2     Author:     Makarius
     3 
     4 Session information.
     5 */
     6 
     7 package isabelle
     8 
     9 import java.nio.ByteBuffer
    10 import java.nio.channels.FileChannel
    11 import java.nio.file.StandardOpenOption
    12 
    13 import scala.collection.SortedSet
    14 import scala.collection.mutable
    15 
    16 
    17 object Sessions
    18 {
    19   /* info */
    20 
    21   val ROOT = Path.explode("ROOT")
    22   val ROOTS = Path.explode("ROOTS")
    23 
    24   def is_pure(name: String): Boolean = name == "Pure"
    25 
    26   sealed case class Info(
    27     chapter: String,
    28     select: Boolean,
    29     pos: Position.T,
    30     groups: List[String],
    31     dir: Path,
    32     parent: Option[String],
    33     description: String,
    34     options: Options,
    35     theories: List[(Boolean, Options, List[Path])],
    36     files: List[Path],
    37     document_files: List[(Path, Path)],
    38     meta_digest: SHA1.Digest)
    39   {
    40     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    41   }
    42 
    43 
    44   /* session tree */
    45 
    46   object Tree
    47   {
    48     def apply(infos: Seq[(String, Info)]): Tree =
    49     {
    50       val graph1 =
    51         (Graph.string[Info] /: infos) {
    52           case (graph, (name, info)) =>
    53             if (graph.defined(name))
    54               error("Duplicate session " + quote(name) + Position.here(info.pos) +
    55                 Position.here(graph.get_node(name).pos))
    56             else graph.new_node(name, info)
    57         }
    58       val graph2 =
    59         (graph1 /: graph1.iterator) {
    60           case (graph, (name, (info, _))) =>
    61             info.parent match {
    62               case None => graph
    63               case Some(parent) =>
    64                 if (!graph.defined(parent))
    65                   error("Bad parent session " + quote(parent) + " for " +
    66                     quote(name) + Position.here(info.pos))
    67 
    68                 try { graph.add_edge_acyclic(parent, name) }
    69                 catch {
    70                   case exn: Graph.Cycles[_] =>
    71                     error(cat_lines(exn.cycles.map(cycle =>
    72                       "Cyclic session dependency of " +
    73                         cycle.map(c => quote(c.toString)).mkString(" via "))) +
    74                           Position.here(info.pos))
    75                 }
    76             }
    77         }
    78       new Tree(graph2)
    79     }
    80   }
    81 
    82   final class Tree private(val graph: Graph[String, Info])
    83     extends PartialFunction[String, Info]
    84   {
    85     def apply(name: String): Info = graph.get_node(name)
    86     def isDefinedAt(name: String): Boolean = graph.defined(name)
    87 
    88     def selection(
    89       requirements: Boolean = false,
    90       all_sessions: Boolean = false,
    91       exclude_session_groups: List[String] = Nil,
    92       exclude_sessions: List[String] = Nil,
    93       session_groups: List[String] = Nil,
    94       sessions: List[String] = Nil): (List[String], Tree) =
    95     {
    96       val bad_sessions =
    97         SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
    98       if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    99 
   100       val excluded =
   101       {
   102         val exclude_group = exclude_session_groups.toSet
   103         val exclude_group_sessions =
   104           (for {
   105             (name, (info, _)) <- graph.iterator
   106             if apply(name).groups.exists(exclude_group)
   107           } yield name).toList
   108         graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
   109       }
   110 
   111       val pre_selected =
   112       {
   113         if (all_sessions) graph.keys
   114         else {
   115           val select_group = session_groups.toSet
   116           val select = sessions.toSet
   117           (for {
   118             (name, (info, _)) <- graph.iterator
   119             if info.select || select(name) || apply(name).groups.exists(select_group)
   120           } yield name).toList
   121         }
   122       }.filterNot(excluded)
   123 
   124       val selected =
   125         if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
   126         else pre_selected
   127 
   128       val graph1 = graph.restrict(graph.all_preds(selected).toSet)
   129       (selected, new Tree(graph1))
   130     }
   131 
   132     def ancestors(name: String): List[String] =
   133       graph.all_preds(List(name)).tail.reverse
   134 
   135     def topological_order: List[(String, Info)] =
   136       graph.topological_order.map(name => (name, apply(name)))
   137 
   138     override def toString: String = graph.keys_iterator.mkString("Sessions.Tree(", ", ", ")")
   139   }
   140 
   141 
   142   /* parser */
   143 
   144   private val CHAPTER = "chapter"
   145   private val SESSION = "session"
   146   private val IN = "in"
   147   private val DESCRIPTION = "description"
   148   private val OPTIONS = "options"
   149   private val GLOBAL_THEORIES = "global_theories"
   150   private val THEORIES = "theories"
   151   private val FILES = "files"
   152   private val DOCUMENT_FILES = "document_files"
   153 
   154   lazy val root_syntax =
   155     Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   156       (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
   157       IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
   158 
   159   object Parser extends Parse.Parser
   160   {
   161     private abstract class Entry
   162     private sealed case class Chapter(name: String) extends Entry
   163     private sealed case class Session_Entry(
   164       pos: Position.T,
   165       name: String,
   166       groups: List[String],
   167       path: String,
   168       parent: Option[String],
   169       description: String,
   170       options: List[Options.Spec],
   171       theories: List[(Boolean, List[Options.Spec], List[String])],
   172       files: List[String],
   173       document_files: List[(String, String)]) extends Entry
   174 
   175     private val chapter: Parser[Chapter] =
   176     {
   177       val chapter_name = atom("chapter name", _.is_name)
   178 
   179       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
   180     }
   181 
   182     private val session_entry: Parser[Session_Entry] =
   183     {
   184       val session_name = atom("session name", _.is_name)
   185 
   186       val option =
   187         name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   188       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
   189 
   190       val theories =
   191         ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
   192           ((options | success(Nil)) ~ rep(theory_xname)) ^^
   193           { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
   194 
   195       val document_files =
   196         $$$(DOCUMENT_FILES) ~!
   197           (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
   198               { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
   199             rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
   200 
   201       command(SESSION) ~!
   202         (position(session_name) ~
   203           (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
   204           (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
   205           ($$$("=") ~!
   206             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
   207               (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
   208               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
   209               rep1(theories) ~
   210               (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
   211               (rep(document_files) ^^ (x => x.flatten))))) ^^
   212         { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
   213             Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
   214     }
   215 
   216     def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
   217     {
   218       def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
   219       {
   220         try {
   221           val name = entry.name
   222 
   223           if (name == "") error("Bad session name")
   224           if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
   225           if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
   226 
   227           val session_options = options ++ entry.options
   228 
   229           val theories =
   230             entry.theories.map({ case (global, opts, thys) =>
   231               (global, session_options ++ opts, thys.map(Path.explode(_))) })
   232           val files = entry.files.map(Path.explode(_))
   233           val document_files =
   234             entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
   235 
   236           val meta_digest =
   237             SHA1.digest((entry_chapter, name, entry.parent, entry.options,
   238               entry.theories, entry.files, entry.document_files).toString)
   239 
   240           val info =
   241             Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
   242               entry.parent, entry.description, session_options, theories, files,
   243               document_files, meta_digest)
   244 
   245           (name, info)
   246         }
   247         catch {
   248           case ERROR(msg) =>
   249             error(msg + "\nThe error(s) above occurred in session entry " +
   250               quote(entry.name) + Position.here(entry.pos))
   251         }
   252       }
   253 
   254       val root = dir + ROOT
   255       if (root.is_file) {
   256         val toks = Token.explode(root_syntax.keywords, File.read(root))
   257         val start = Token.Pos.file(root.implode)
   258 
   259         parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
   260           case Success(result, _) =>
   261             var entry_chapter = "Unsorted"
   262             val infos = new mutable.ListBuffer[(String, Info)]
   263             result.foreach {
   264               case Chapter(name) => entry_chapter = name
   265               case entry: Session_Entry => infos += make_info(entry_chapter, entry)
   266             }
   267             infos.toList
   268           case bad => error(bad.toString)
   269         }
   270       }
   271       else Nil
   272     }
   273   }
   274 
   275 
   276   /* load sessions from certain directories */
   277 
   278   private def is_session_dir(dir: Path): Boolean =
   279     (dir + ROOT).is_file || (dir + ROOTS).is_file
   280 
   281   private def check_session_dir(dir: Path): Path =
   282     if (is_session_dir(dir)) dir
   283     else error("Bad session root directory: " + dir.toString)
   284 
   285   def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): Tree =
   286   {
   287     def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
   288       load_root(select, dir) ::: load_roots(select, dir)
   289 
   290     def load_root(select: Boolean, dir: Path): List[(String, Info)] =
   291       Parser.parse(options, select, dir)
   292 
   293     def load_roots(select: Boolean, dir: Path): List[(String, Info)] =
   294     {
   295       val roots = dir + ROOTS
   296       if (roots.is_file) {
   297         for {
   298           line <- split_lines(File.read(roots))
   299           if !(line == "" || line.startsWith("#"))
   300           dir1 =
   301             try { check_session_dir(dir + Path.explode(line)) }
   302             catch {
   303               case ERROR(msg) =>
   304                 error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
   305             }
   306           info <- load_dir(select, dir1)
   307         } yield info
   308       }
   309       else Nil
   310     }
   311 
   312     val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
   313     dirs.foreach(check_session_dir(_))
   314     select_dirs.foreach(check_session_dir(_))
   315 
   316     Tree(
   317       for {
   318         (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
   319         info <- load_dir(select, dir)
   320       } yield info)
   321   }
   322 
   323 
   324 
   325   /** heap file with SHA1 digest **/
   326 
   327   private val sha1_prefix = "SHA1:"
   328 
   329   def read_heap_digest(heap: Path): Option[String] =
   330   {
   331     if (heap.is_file) {
   332       val file = FileChannel.open(heap.file.toPath, StandardOpenOption.READ)
   333       try {
   334         val len = file.size
   335         val n = sha1_prefix.length + SHA1.digest_length
   336         if (len >= n) {
   337           file.position(len - n)
   338 
   339           val buf = ByteBuffer.allocate(n)
   340           var i = 0
   341           var m = 0
   342           do {
   343             m = file.read(buf)
   344             if (m != -1) i += m
   345           }
   346           while (m != -1 && n > i)
   347 
   348           if (i == n) {
   349             val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
   350             val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
   351             if (prefix == sha1_prefix) Some(s) else None
   352           }
   353           else None
   354         }
   355         else None
   356       }
   357       finally { file.close }
   358     }
   359     else None
   360   }
   361 
   362   def write_heap_digest(heap: Path): String =
   363     read_heap_digest(heap) match {
   364       case None =>
   365         val s = SHA1.digest(heap).rep
   366         File.append(heap, sha1_prefix + s)
   367         s
   368       case Some(s) => s
   369     }
   370 
   371 
   372 
   373   /** persistent store **/
   374 
   375   def log(name: String): Path = Path.basic("log") + Path.basic(name)
   376   def log_gz(name: String): Path = log(name).ext("gz")
   377 
   378   def store(system_mode: Boolean = false): Store = new Store(system_mode)
   379 
   380   class Store private [Sessions](system_mode: Boolean)
   381   {
   382     /* output */
   383 
   384     val browser_info: Path =
   385       if (system_mode) Path.explode("~~/browser_info")
   386       else Path.explode("$ISABELLE_BROWSER_INFO")
   387 
   388     val output_dir: Path =
   389       if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
   390       else Path.explode("$ISABELLE_OUTPUT")
   391 
   392     def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
   393 
   394 
   395     /* input */
   396 
   397     private val input_dirs =
   398       if (system_mode) List(output_dir)
   399       else {
   400         val ml_ident = Path.explode("$ML_IDENTIFIER").expand
   401         output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
   402       }
   403 
   404     def find(name: String): Option[(Path, Option[String])] =
   405       input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
   406         (dir + log_gz(name), read_heap_digest(dir + Path.basic(name))))
   407 
   408     def find_log(name: String): Option[Path] =
   409       input_dirs.map(_ + log(name)).find(_.is_file)
   410 
   411     def find_log_gz(name: String): Option[Path] =
   412       input_dirs.map(_ + log_gz(name)).find(_.is_file)
   413 
   414     def find_heap(name: String): Option[Path] =
   415       input_dirs.map(_ + Path.basic(name)).find(_.is_file)
   416 
   417     def heap(name: String): Path =
   418       find_heap(name) getOrElse
   419         error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
   420           cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
   421   }
   422 }