src/Pure/Admin/afp.scala
author wenzelm
Tue Nov 07 16:44:25 2017 +0100 (21 months ago)
changeset 67025 961285f581e6
parent 66861 f6676691ef8a
child 67026 687c822ee5e3
permissions -rw-r--r--
clarifified selection: always wrt. build_graph structure;
tuned signature;
     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 
    10 object 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 
    20 class 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.T =
    39     Sessions.load(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   def partition(n: Int): List[String] =
    89     n match {
    90       case 0 => Nil
    91       case 1 | 2 =>
    92         val graph = sessions_structure.build_graph.restrict(sessions.toSet)
    93         val (isolated_sessions, connected_sessions) = graph.keys.partition(graph.is_isolated(_))
    94         if (n == 1) isolated_sessions else connected_sessions
    95       case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
    96     }
    97 }