src/Pure/Admin/afp.scala
author wenzelm
Mon Mar 25 19:50:52 2019 +0100 (3 months ago)
changeset 69982 f150253cb201
parent 69981 3dced198b9ec
child 69995 2d5c313e8582
permissions -rw-r--r--
RDF meta data for AFP entries;
tuned;
     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 java.time.LocalDate
    11 import scala.collection.immutable.SortedMap
    12 
    13 
    14 object AFP
    15 {
    16   val repos_source = "https://isabelle.sketis.net/repos/afp-devel"
    17 
    18   val groups: Map[String, String] =
    19     Map("large" -> "full 64-bit memory model or word arithmetic required",
    20       "slow" -> "CPU time much higher than 60min (on mid-range hardware)",
    21       "very_slow" -> "elapsed time of many hours (on high-end hardware)")
    22 
    23   def groups_bulky: List[String] = List("large", "slow")
    24 
    25   def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
    26     new AFP(options, base_dir)
    27 
    28 
    29   /* entries */
    30 
    31   def parse_date(s: String): Date =
    32   {
    33     val t = Date.Formatter.pattern("uuuu-MM-dd").parse(s)
    34     Date(LocalDate.from(t).atStartOfDay(Date.timezone_berlin))
    35   }
    36 
    37   sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
    38   {
    39     def get(prop: String): Option[String] = Properties.get(metadata, prop)
    40     def get_string(prop: String): String = get(prop).getOrElse("")
    41     def get_strings(prop: String): List[String] =
    42       Library.space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
    43 
    44     def title: String = get_string("title")
    45     def authors: List[String] = get_strings("author")
    46     def date: Date =
    47       parse_date(get("date").getOrElse(error("Missing date for entry " + quote(name))))
    48     def topics: List[String] = get_strings("topic")
    49     def `abstract`: String = get_string("abstract").trim
    50     def maintainers: List[String] = get_strings("notify")
    51     def contributors: List[String] = get_strings("contributors")
    52     def license: String = get("license").getOrElse("BSD")
    53 
    54     def rdf_meta_data: Properties.T =
    55       RDF.meta_data(
    56         proper_string(title).map(Markup.META_TITLE -> _).toList :::
    57         authors.map(Markup.META_CREATOR -> _) :::
    58         contributors.map(Markup.META_CONTRIBUTOR -> _) :::
    59         List(Markup.META_DATE -> RDF.date_format(date)) :::
    60         List(Markup.META_LICENSE -> license) :::
    61         proper_string(`abstract`).map(Markup.META_DESCRIPTION -> _).toList)
    62   }
    63 }
    64 
    65 class AFP private(options: Options, val base_dir: Path)
    66 {
    67   override def toString: String = base_dir.expand.toString
    68 
    69   val main_dir: Path = base_dir + Path.explode("thys")
    70 
    71 
    72   /* metadata */
    73 
    74   private val entry_metadata: Map[String, Properties.T] =
    75   {
    76     val metadata_file = base_dir + Path.explode("metadata/metadata")
    77 
    78     var result = Map.empty[String, Properties.T]
    79     var section = ""
    80     var props = List.empty[Properties.Entry]
    81 
    82     val Section = """^\[(\S+)\]\s*$""".r
    83     val Property = """^(\S+)\s*=(.*)$""".r
    84     val Extra_Line = """^\s+(.*)$""".r
    85     val Blank_Line = """^\s*$""".r
    86 
    87     def flush()
    88     {
    89       if (section != "") result += (section -> props.reverse.filter(p => p._2.nonEmpty))
    90       section = ""
    91       props = Nil
    92     }
    93 
    94     for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex)
    95     {
    96       def err(msg: String): Nothing =
    97         error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
    98 
    99       line match {
   100         case Section(name) => flush(); section = name
   101         case Property(a, b) =>
   102           if (section == "") err("Property without a section")
   103           props = (a -> b.trim) :: props
   104         case Extra_Line(line) =>
   105           props match {
   106             case Nil => err("Extra line without a property")
   107             case (a, b) :: rest => props = (a, b + "\n" + line.trim) :: rest
   108           }
   109         case Blank_Line() =>
   110         case _ => err("Bad input")
   111       }
   112     }
   113 
   114     flush()
   115     result
   116   }
   117 
   118 
   119   /* entries */
   120 
   121   val entries_map: SortedMap[String, AFP.Entry] =
   122   {
   123     val entries =
   124       for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
   125         val metadata =
   126           entry_metadata.getOrElse(name, error("Entry without metadata: " + quote(name)))
   127         val sessions =
   128           Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
   129         AFP.Entry(name, metadata, sessions)
   130       }
   131 
   132     val entries_map =
   133       (SortedMap.empty[String, AFP.Entry] /: entries)({ case (m, e) => m + (e.name -> e) })
   134 
   135     val extra_metadata =
   136       (for ((name, _) <- entry_metadata.iterator if !entries_map.isDefinedAt(name)) yield name).
   137         toList.sorted
   138     if (extra_metadata.nonEmpty)
   139       error("Meta data without entry: " + commas_quote(extra_metadata))
   140 
   141     entries_map
   142   }
   143 
   144   val entries: List[AFP.Entry] = entries_map.toList.map(_._2)
   145 
   146 
   147   /* sessions */
   148 
   149   val sessions_map: SortedMap[String, AFP.Entry] =
   150     (SortedMap.empty[String, AFP.Entry] /: entries)(
   151       { case (m1, e) => (m1 /: e.sessions)({ case (m2, s) => m2 + (s -> e) }) })
   152 
   153   val sessions: List[String] = entries.flatMap(_.sessions)
   154 
   155   val sessions_structure: Sessions.Structure =
   156     Sessions.load_structure(options, dirs = List(main_dir)).
   157       selection(Sessions.Selection(sessions = sessions.toList))
   158 
   159 
   160   /* dependency graph */
   161 
   162   private def sessions_deps(entry: AFP.Entry): List[String] =
   163     entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
   164 
   165   lazy val entries_graph: Graph[String, Unit] =
   166   {
   167     val session_entries =
   168       (Map.empty[String, String] /: entries) {
   169         case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) }
   170       }
   171     (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
   172       val e1 = entry.name
   173       (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) =>
   174         (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
   175           try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
   176           catch {
   177             case exn: Graph.Cycles[_] =>
   178               error(cat_lines(exn.cycles.map(cycle =>
   179                 "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
   180                 " due to session " + quote(s))))
   181           }
   182         }
   183       }
   184     }
   185   }
   186 
   187   def entries_graph_display: Graph_Display.Graph =
   188     Graph_Display.make_graph(entries_graph)
   189 
   190   def entries_json_text: String =
   191     (for (entry <- entries.iterator) yield {
   192       val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_))
   193       val afp_deps = entries_graph.imm_preds(entry.name).toList
   194       """
   195  {""" + JSON.Format(entry.name) + """:
   196   {"distrib_deps": """ + JSON.Format(distrib_deps) + """,
   197    "afp_deps": """ + JSON.Format(afp_deps) + """
   198   }
   199  }"""
   200     }).mkString("[", ", ", "\n]\n")
   201 
   202 
   203   /* partition sessions */
   204 
   205   val force_partition1: List[String] = List("Category3", "HOL-ODE")
   206 
   207   def partition(n: Int): List[String] =
   208     n match {
   209       case 0 => Nil
   210       case 1 | 2 =>
   211         val graph = sessions_structure.build_graph.restrict(sessions.toSet)
   212         val force_part1 =
   213           graph.all_preds(graph.all_succs(force_partition1.filter(graph.defined(_)))).toSet
   214         val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
   215         if (n == 1) part1 else part2
   216       case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
   217     }
   218 }