wenzelm@66820: /*  Title:      Pure/Admin/afp.scala
wenzelm@66820:     Author:     Makarius
wenzelm@66820: 
wenzelm@66820: Administrative support for the Archive of Formal Proofs.
wenzelm@66820: */
wenzelm@66820: 
wenzelm@66820: package isabelle
wenzelm@66820: 
wenzelm@66820: 
wenzelm@69980: import java.time.LocalDate
wenzelm@69974: import scala.collection.immutable.SortedMap
wenzelm@69974: 
wenzelm@69974: 
wenzelm@66820: object AFP
wenzelm@66820: {
wenzelm@69787:   val repos_source = "https://isabelle.sketis.net/repos/afp-devel"
wenzelm@66854: 
wenzelm@69693:   val groups: Map[String, String] =
wenzelm@69693:     Map("large" -> "full 64-bit memory model or word arithmetic required",
wenzelm@69693:       "slow" -> "CPU time much higher than 60min (on mid-range hardware)",
wenzelm@69693:       "very_slow" -> "elapsed time of many hours (on high-end hardware)")
wenzelm@69693: 
wenzelm@69693:   def groups_bulky: List[String] = List("large", "slow")
wenzelm@69693: 
wenzelm@66824:   def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
wenzelm@66824:     new AFP(options, base_dir)
wenzelm@66820: 
wenzelm@69973: 
wenzelm@69973:   /* entries */
wenzelm@69973: 
wenzelm@69977:   def parse_date(s: String): Date =
wenzelm@69977:   {
wenzelm@69977:     val t = Date.Formatter.pattern("uuuu-MM-dd").parse(s)
wenzelm@69980:     Date(LocalDate.from(t).atStartOfDay(Date.timezone_berlin))
wenzelm@69977:   }
wenzelm@69977: 
wenzelm@69975:   sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
wenzelm@69976:   {
wenzelm@69977:     def get(prop: String): Option[String] = Properties.get(metadata, prop)
wenzelm@69977:     def get_string(prop: String): String = get(prop).getOrElse("")
wenzelm@69977:     def get_strings(prop: String): List[String] =
wenzelm@69977:       Library.space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
wenzelm@69977: 
wenzelm@69977:     def title: String = get_string("title")
wenzelm@69977:     def authors: List[String] = get_strings("author")
wenzelm@69981:     def date: Date =
wenzelm@69981:       parse_date(get("date").getOrElse(error("Missing date for entry " + quote(name))))
wenzelm@69977:     def topics: List[String] = get_strings("topic")
wenzelm@69981:     def `abstract`: String = get_string("abstract").trim
wenzelm@69977:     def maintainers: List[String] = get_strings("notify")
wenzelm@69977:     def contributors: List[String] = get_strings("contributors")
wenzelm@69981:     def license: String = get("license").getOrElse("BSD")
wenzelm@69982: 
wenzelm@69982:     def rdf_meta_data: Properties.T =
wenzelm@69982:       RDF.meta_data(
wenzelm@69982:         proper_string(title).map(Markup.META_TITLE -> _).toList :::
wenzelm@69982:         authors.map(Markup.META_CREATOR -> _) :::
wenzelm@69982:         contributors.map(Markup.META_CONTRIBUTOR -> _) :::
wenzelm@69982:         List(Markup.META_DATE -> RDF.date_format(date)) :::
wenzelm@69982:         List(Markup.META_LICENSE -> license) :::
wenzelm@69982:         proper_string(`abstract`).map(Markup.META_DESCRIPTION -> _).toList)
wenzelm@69976:   }
wenzelm@66820: }
wenzelm@66820: 
wenzelm@66824: class AFP private(options: Options, val base_dir: Path)
wenzelm@66820: {
wenzelm@66821:   override def toString: String = base_dir.expand.toString
wenzelm@66821: 
wenzelm@66820:   val main_dir: Path = base_dir + Path.explode("thys")
wenzelm@66820: 
wenzelm@66821: 
wenzelm@69975:   /* metadata */
wenzelm@69975: 
wenzelm@69975:   private val entry_metadata: Map[String, Properties.T] =
wenzelm@69975:   {
wenzelm@69975:     val metadata_file = base_dir + Path.explode("metadata/metadata")
wenzelm@69975: 
wenzelm@69975:     var result = Map.empty[String, Properties.T]
wenzelm@69975:     var section = ""
wenzelm@69975:     var props = List.empty[Properties.Entry]
wenzelm@69975: 
wenzelm@69975:     val Section = """^\[(\S+)\]\s*$""".r
wenzelm@69975:     val Property = """^(\S+)\s*=(.*)$""".r
wenzelm@69975:     val Extra_Line = """^\s+(.*)$""".r
wenzelm@69975:     val Blank_Line = """^\s*$""".r
wenzelm@69975: 
wenzelm@69975:     def flush()
wenzelm@69975:     {
wenzelm@69978:       if (section != "") result += (section -> props.reverse.filter(p => p._2.nonEmpty))
wenzelm@69975:       section = ""
wenzelm@69975:       props = Nil
wenzelm@69975:     }
wenzelm@69975: 
wenzelm@69975:     for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex)
wenzelm@69975:     {
wenzelm@69975:       def err(msg: String): Nothing =
wenzelm@69975:         error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
wenzelm@69975: 
wenzelm@69975:       line match {
wenzelm@69975:         case Section(name) => flush(); section = name
wenzelm@69975:         case Property(a, b) =>
wenzelm@69975:           if (section == "") err("Property without a section")
wenzelm@69978:           props = (a -> b.trim) :: props
wenzelm@69975:         case Extra_Line(line) =>
wenzelm@69975:           props match {
wenzelm@69975:             case Nil => err("Extra line without a property")
wenzelm@69975:             case (a, b) :: rest => props = (a, b + "\n" + line.trim) :: rest
wenzelm@69975:           }
wenzelm@69975:         case Blank_Line() =>
wenzelm@69975:         case _ => err("Bad input")
wenzelm@69975:       }
wenzelm@69975:     }
wenzelm@69975: 
wenzelm@69975:     flush()
wenzelm@69975:     result
wenzelm@69975:   }
wenzelm@69975: 
wenzelm@69975: 
wenzelm@69979:   /* entries */
wenzelm@66821: 
wenzelm@69974:   val entries_map: SortedMap[String, AFP.Entry] =
wenzelm@69973:   {
wenzelm@69973:     val entries =
wenzelm@69974:       for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
wenzelm@69973:         val metadata =
wenzelm@69973:           entry_metadata.getOrElse(name, error("Entry without metadata: " + quote(name)))
wenzelm@69973:         val sessions =
wenzelm@69973:           Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
wenzelm@69973:         AFP.Entry(name, metadata, sessions)
wenzelm@69974:       }
wenzelm@69973: 
wenzelm@69974:     val entries_map =
wenzelm@69974:       (SortedMap.empty[String, AFP.Entry] /: entries)({ case (m, e) => m + (e.name -> e) })
wenzelm@69974: 
wenzelm@69973:     val extra_metadata =
wenzelm@69974:       (for ((name, _) <- entry_metadata.iterator if !entries_map.isDefinedAt(name)) yield name).
wenzelm@69974:         toList.sorted
wenzelm@69974:     if (extra_metadata.nonEmpty)
wenzelm@69974:       error("Meta data without entry: " + commas_quote(extra_metadata))
wenzelm@69973: 
wenzelm@69974:     entries_map
wenzelm@69973:   }
wenzelm@66820: 
wenzelm@69974:   val entries: List[AFP.Entry] = entries_map.toList.map(_._2)
wenzelm@69979: 
wenzelm@69979: 
wenzelm@69979:   /* sessions */
wenzelm@69979: 
wenzelm@69979:   val sessions_map: SortedMap[String, AFP.Entry] =
wenzelm@69979:     (SortedMap.empty[String, AFP.Entry] /: entries)(
wenzelm@69979:       { case (m1, e) => (m1 /: e.sessions)({ case (m2, s) => m2 + (s -> e) }) })
wenzelm@69979: 
wenzelm@66821:   val sessions: List[String] = entries.flatMap(_.sessions)
wenzelm@66824: 
wenzelm@67052:   val sessions_structure: Sessions.Structure =
wenzelm@67026:     Sessions.load_structure(options, dirs = List(main_dir)).
wenzelm@67025:       selection(Sessions.Selection(sessions = sessions.toList))
wenzelm@66821: 
wenzelm@66821: 
wenzelm@66824:   /* dependency graph */
wenzelm@66821: 
wenzelm@66824:   private def sessions_deps(entry: AFP.Entry): List[String] =
wenzelm@66824:     entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
wenzelm@66824: 
wenzelm@66852:   lazy val entries_graph: Graph[String, Unit] =
wenzelm@66821:   {
wenzelm@66821:     val session_entries =
wenzelm@66831:       (Map.empty[String, String] /: entries) {
wenzelm@66831:         case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) }
wenzelm@66821:       }
wenzelm@66831:     (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
wenzelm@66831:       val e1 = entry.name
wenzelm@66832:       (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) =>
wenzelm@66832:         (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
wenzelm@66852:           try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
wenzelm@66852:           catch {
wenzelm@66852:             case exn: Graph.Cycles[_] =>
wenzelm@66852:               error(cat_lines(exn.cycles.map(cycle =>
wenzelm@66852:                 "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
wenzelm@66852:                 " due to session " + quote(s))))
wenzelm@66832:           }
wenzelm@66821:         }
wenzelm@66821:       }
wenzelm@66824:     }
wenzelm@66821:   }
wenzelm@66821: 
wenzelm@66824:   def entries_graph_display: Graph_Display.Graph =
wenzelm@66824:     Graph_Display.make_graph(entries_graph)
wenzelm@66823: 
wenzelm@66824:   def entries_json_text: String =
wenzelm@66824:     (for (entry <- entries.iterator) yield {
wenzelm@66824:       val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_))
wenzelm@66824:       val afp_deps = entries_graph.imm_preds(entry.name).toList
wenzelm@66824:       """
wenzelm@66821:  {""" + JSON.Format(entry.name) + """:
wenzelm@66821:   {"distrib_deps": """ + JSON.Format(distrib_deps) + """,
wenzelm@66821:    "afp_deps": """ + JSON.Format(afp_deps) + """
wenzelm@66821:   }
wenzelm@66821:  }"""
wenzelm@66824:     }).mkString("[", ", ", "\n]\n")
wenzelm@66861: 
wenzelm@66861: 
wenzelm@66861:   /* partition sessions */
wenzelm@66861: 
wenzelm@67817:   val force_partition1: List[String] = List("Category3", "HOL-ODE")
wenzelm@67776: 
wenzelm@66861:   def partition(n: Int): List[String] =
wenzelm@66861:     n match {
wenzelm@66861:       case 0 => Nil
wenzelm@66861:       case 1 | 2 =>
wenzelm@66861:         val graph = sessions_structure.build_graph.restrict(sessions.toSet)
wenzelm@67817:         val force_part1 =
wenzelm@67817:           graph.all_preds(graph.all_succs(force_partition1.filter(graph.defined(_)))).toSet
wenzelm@67817:         val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
wenzelm@67817:         if (n == 1) part1 else part2
wenzelm@66861:       case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
wenzelm@66861:     }
wenzelm@66820: }