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