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