1/* Title: Pure/Admin/afp.scala 2 Author: Makarius 3 4Administrative support for the Archive of Formal Proofs. 5*/ 6 7package isabelle 8 9 10object AFP 11{ 12 val repos_source = "https://bitbucket.org/isa-afp/afp-devel" 13 14 def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP = 15 new AFP(options, base_dir) 16 17 sealed case class Entry(name: String, sessions: List[String]) 18} 19 20class AFP private(options: Options, val base_dir: Path) 21{ 22 override def toString: String = base_dir.expand.toString 23 24 val main_dir: Path = base_dir + Path.explode("thys") 25 26 27 /* entries and sessions */ 28 29 val entries: List[AFP.Entry] = 30 (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield { 31 val sessions = 32 Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name) 33 AFP.Entry(name, sessions) 34 }).sortBy(_.name) 35 36 val sessions: List[String] = entries.flatMap(_.sessions) 37 38 val sessions_structure: Sessions.Structure = 39 Sessions.load_structure(options, dirs = List(main_dir)). 40 selection(Sessions.Selection(sessions = sessions.toList)) 41 42 43 /* dependency graph */ 44 45 private def sessions_deps(entry: AFP.Entry): List[String] = 46 entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted 47 48 lazy val entries_graph: Graph[String, Unit] = 49 { 50 val session_entries = 51 (Map.empty[String, String] /: entries) { 52 case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) } 53 } 54 (Graph.empty[String, Unit] /: entries) { case (g, entry) => 55 val e1 = entry.name 56 (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) => 57 (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) => 58 try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) } 59 catch { 60 case exn: Graph.Cycles[_] => 61 error(cat_lines(exn.cycles.map(cycle => 62 "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") + 63 " due to session " + quote(s)))) 64 } 65 } 66 } 67 } 68 } 69 70 def entries_graph_display: Graph_Display.Graph = 71 Graph_Display.make_graph(entries_graph) 72 73 def entries_json_text: String = 74 (for (entry <- entries.iterator) yield { 75 val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_)) 76 val afp_deps = entries_graph.imm_preds(entry.name).toList 77 """ 78 {""" + JSON.Format(entry.name) + """: 79 {"distrib_deps": """ + JSON.Format(distrib_deps) + """, 80 "afp_deps": """ + JSON.Format(afp_deps) + """ 81 } 82 }""" 83 }).mkString("[", ", ", "\n]\n") 84 85 86 /* partition sessions */ 87 88 val force_partition1: List[String] = List("Category3", "HOL-ODE") 89 90 def partition(n: Int): List[String] = 91 n match { 92 case 0 => Nil 93 case 1 | 2 => 94 val graph = sessions_structure.build_graph.restrict(sessions.toSet) 95 val force_part1 = 96 graph.all_preds(graph.all_succs(force_partition1.filter(graph.defined(_)))).toSet 97 val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a)) 98 if (n == 1) part1 else part2 99 case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)") 100 } 101} 102