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