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