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