src/Pure/Admin/afp.scala
author wenzelm
Sat Jan 19 20:18:26 2019 +0100 (7 months ago)
changeset 69693 06153e2e0cdb
parent 67817 93faefc25fe7
child 69787 60b5a4731695
permissions -rw-r--r--
more official AFP.groups;
clarified bulky sessions;
     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   val groups: Map[String, String] =
    15     Map("large" -> "full 64-bit memory model or word arithmetic required",
    16       "slow" -> "CPU time much higher than 60min (on mid-range hardware)",
    17       "very_slow" -> "elapsed time of many hours (on high-end hardware)")
    18 
    19   def groups_bulky: List[String] = List("large", "slow")
    20 
    21   def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
    22     new AFP(options, base_dir)
    23 
    24   sealed case class Entry(name: String, sessions: List[String])
    25 }
    26 
    27 class AFP private(options: Options, val base_dir: Path)
    28 {
    29   override def toString: String = base_dir.expand.toString
    30 
    31   val main_dir: Path = base_dir + Path.explode("thys")
    32 
    33 
    34   /* entries and sessions */
    35 
    36   val entries: List[AFP.Entry] =
    37     (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
    38       val sessions =
    39         Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
    40       AFP.Entry(name, sessions)
    41     }).sortBy(_.name)
    42 
    43   val sessions: List[String] = entries.flatMap(_.sessions)
    44 
    45   val sessions_structure: Sessions.Structure =
    46     Sessions.load_structure(options, dirs = List(main_dir)).
    47       selection(Sessions.Selection(sessions = sessions.toList))
    48 
    49 
    50   /* dependency graph */
    51 
    52   private def sessions_deps(entry: AFP.Entry): List[String] =
    53     entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
    54 
    55   lazy val entries_graph: Graph[String, Unit] =
    56   {
    57     val session_entries =
    58       (Map.empty[String, String] /: entries) {
    59         case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) }
    60       }
    61     (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
    62       val e1 = entry.name
    63       (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) =>
    64         (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
    65           try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
    66           catch {
    67             case exn: Graph.Cycles[_] =>
    68               error(cat_lines(exn.cycles.map(cycle =>
    69                 "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
    70                 " due to session " + quote(s))))
    71           }
    72         }
    73       }
    74     }
    75   }
    76 
    77   def entries_graph_display: Graph_Display.Graph =
    78     Graph_Display.make_graph(entries_graph)
    79 
    80   def entries_json_text: String =
    81     (for (entry <- entries.iterator) yield {
    82       val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_))
    83       val afp_deps = entries_graph.imm_preds(entry.name).toList
    84       """
    85  {""" + JSON.Format(entry.name) + """:
    86   {"distrib_deps": """ + JSON.Format(distrib_deps) + """,
    87    "afp_deps": """ + JSON.Format(afp_deps) + """
    88   }
    89  }"""
    90     }).mkString("[", ", ", "\n]\n")
    91 
    92 
    93   /* partition sessions */
    94 
    95   val force_partition1: List[String] = List("Category3", "HOL-ODE")
    96 
    97   def partition(n: Int): List[String] =
    98     n match {
    99       case 0 => Nil
   100       case 1 | 2 =>
   101         val graph = sessions_structure.build_graph.restrict(sessions.toSet)
   102         val force_part1 =
   103           graph.all_preds(graph.all_succs(force_partition1.filter(graph.defined(_)))).toSet
   104         val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
   105         if (n == 1) part1 else part2
   106       case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
   107     }
   108 }