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