src/Pure/Admin/afp.scala
author wenzelm
Mon Mar 25 14:47:54 2019 +0100 (4 months ago)
changeset 69976 98a440cfbb2b
parent 69975 35cc58a54ffc
child 69977 3c166df11085
permissions -rw-r--r--
provide maintainers as seen in AFP/admin;
suppress empty properties;
     1 /*  Title:      Pure/Admin/afp.scala
     2     Author:     Makarius
     3 
     4 Administrative support for the Archive of Formal Proofs.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.immutable.SortedMap
    11 
    12 
    13 object AFP
    14 {
    15   val repos_source = "https://isabelle.sketis.net/repos/afp-devel"
    16 
    17   val groups: Map[String, String] =
    18     Map("large" -> "full 64-bit memory model or word arithmetic required",
    19       "slow" -> "CPU time much higher than 60min (on mid-range hardware)",
    20       "very_slow" -> "elapsed time of many hours (on high-end hardware)")
    21 
    22   def groups_bulky: List[String] = List("large", "slow")
    23 
    24   def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
    25     new AFP(options, base_dir)
    26 
    27 
    28   /* entries */
    29 
    30   sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
    31   {
    32     def maintainers: List[String] =
    33       Library.space_explode(',', Properties.get(metadata, "notify").getOrElse("")).
    34         map(_.trim).filter(_.nonEmpty)
    35   }
    36 }
    37 
    38 class AFP private(options: Options, val base_dir: Path)
    39 {
    40   override def toString: String = base_dir.expand.toString
    41 
    42   val main_dir: Path = base_dir + Path.explode("thys")
    43 
    44 
    45   /* metadata */
    46 
    47   private val entry_metadata: Map[String, Properties.T] =
    48   {
    49     val metadata_file = base_dir + Path.explode("metadata/metadata")
    50 
    51     var result = Map.empty[String, Properties.T]
    52     var section = ""
    53     var props = List.empty[Properties.Entry]
    54 
    55     val Section = """^\[(\S+)\]\s*$""".r
    56     val Property = """^(\S+)\s*=(.*)$""".r
    57     val Extra_Line = """^\s+(.*)$""".r
    58     val Blank_Line = """^\s*$""".r
    59 
    60     def flush()
    61     {
    62       if (section != "") result += (section -> props.reverse)
    63       section = ""
    64       props = Nil
    65     }
    66 
    67     for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex)
    68     {
    69       def err(msg: String): Nothing =
    70         error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
    71 
    72       line match {
    73         case Section(name) => flush(); section = name
    74         case Property(a, b) =>
    75           if (section == "") err("Property without a section")
    76           val c = b.trim
    77           if (c.nonEmpty) props = (a -> c) :: props
    78         case Extra_Line(line) =>
    79           props match {
    80             case Nil => err("Extra line without a property")
    81             case (a, b) :: rest => props = (a, b + "\n" + line.trim) :: rest
    82           }
    83         case Blank_Line() =>
    84         case _ => err("Bad input")
    85       }
    86     }
    87 
    88     flush()
    89     result
    90   }
    91 
    92 
    93   /* entries and sessions */
    94 
    95   val entries_map: SortedMap[String, AFP.Entry] =
    96   {
    97     val entries =
    98       for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
    99         val metadata =
   100           entry_metadata.getOrElse(name, error("Entry without metadata: " + quote(name)))
   101         val sessions =
   102           Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
   103         AFP.Entry(name, metadata, sessions)
   104       }
   105 
   106     val entries_map =
   107       (SortedMap.empty[String, AFP.Entry] /: entries)({ case (m, e) => m + (e.name -> e) })
   108 
   109     val extra_metadata =
   110       (for ((name, _) <- entry_metadata.iterator if !entries_map.isDefinedAt(name)) yield name).
   111         toList.sorted
   112     if (extra_metadata.nonEmpty)
   113       error("Meta data without entry: " + commas_quote(extra_metadata))
   114 
   115     entries_map
   116   }
   117 
   118   val entries: List[AFP.Entry] = entries_map.toList.map(_._2)
   119   val sessions: List[String] = entries.flatMap(_.sessions)
   120 
   121   val sessions_structure: Sessions.Structure =
   122     Sessions.load_structure(options, dirs = List(main_dir)).
   123       selection(Sessions.Selection(sessions = sessions.toList))
   124 
   125 
   126   /* dependency graph */
   127 
   128   private def sessions_deps(entry: AFP.Entry): List[String] =
   129     entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
   130 
   131   lazy val entries_graph: Graph[String, Unit] =
   132   {
   133     val session_entries =
   134       (Map.empty[String, String] /: entries) {
   135         case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) }
   136       }
   137     (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
   138       val e1 = entry.name
   139       (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) =>
   140         (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
   141           try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
   142           catch {
   143             case exn: Graph.Cycles[_] =>
   144               error(cat_lines(exn.cycles.map(cycle =>
   145                 "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
   146                 " due to session " + quote(s))))
   147           }
   148         }
   149       }
   150     }
   151   }
   152 
   153   def entries_graph_display: Graph_Display.Graph =
   154     Graph_Display.make_graph(entries_graph)
   155 
   156   def entries_json_text: String =
   157     (for (entry <- entries.iterator) yield {
   158       val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_))
   159       val afp_deps = entries_graph.imm_preds(entry.name).toList
   160       """
   161  {""" + JSON.Format(entry.name) + """:
   162   {"distrib_deps": """ + JSON.Format(distrib_deps) + """,
   163    "afp_deps": """ + JSON.Format(afp_deps) + """
   164   }
   165  }"""
   166     }).mkString("[", ", ", "\n]\n")
   167 
   168 
   169   /* partition sessions */
   170 
   171   val force_partition1: List[String] = List("Category3", "HOL-ODE")
   172 
   173   def partition(n: Int): List[String] =
   174     n match {
   175       case 0 => Nil
   176       case 1 | 2 =>
   177         val graph = sessions_structure.build_graph.restrict(sessions.toSet)
   178         val force_part1 =
   179           graph.all_preds(graph.all_succs(force_partition1.filter(graph.defined(_)))).toSet
   180         val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
   181         if (n == 1) part1 else part2
   182       case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
   183     }
   184 }