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