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