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