diff --git a/src/Pure/Admin/afp.scala b/src/Pure/Admin/afp.scala --- a/src/Pure/Admin/afp.scala +++ b/src/Pure/Admin/afp.scala @@ -1,215 +1,217 @@ /* Title: Pure/Admin/afp.scala Author: Makarius Administrative support for the Archive of Formal Proofs. */ package isabelle import java.time.LocalDate import scala.collection.immutable.SortedMap object AFP { val groups: Map[String, String] = Map("large" -> "full 64-bit memory model or word arithmetic required", "slow" -> "CPU time much higher than 60min (on mid-range hardware)", "very_slow" -> "elapsed time of many hours (on high-end hardware)") val groups_bulky: List[String] = List("large", "slow") val chapter: String = "AFP" val force_partition1: List[String] = List("Category3", "HOL-ODE") - def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP = + val BASE: Path = Path.explode("$AFP_BASE") + + def init(options: Options, base_dir: Path = BASE): AFP = new AFP(options, base_dir) /* entries */ def parse_date(s: String): Date = { val t = Date.Formatter.pattern("uuuu-MM-dd").parse(s) Date(LocalDate.from(t).atStartOfDay(Date.timezone_berlin)) } def trim_mail(s: String): String = s.replaceAll("<[^>]*>", "").trim sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String]) { def get(prop: String): Option[String] = Properties.get(metadata, prop) def get_string(prop: String): String = get(prop).getOrElse("") def get_strings(prop: String): List[String] = space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty) def title: String = get_string("title") def authors: List[String] = get_strings("author") def date: Date = parse_date(get("date").getOrElse(error("Missing date for entry " + quote(name)))) def topics: List[String] = get_strings("topic") def `abstract`: String = get_string("abstract").trim def maintainers: List[String] = get_strings("notify") def contributors: List[String] = get_strings("contributors") def license: String = get("license").getOrElse("BSD") def rdf_meta_data: Properties.T = RDF.meta_data( proper_string(title).map(Markup.META_TITLE -> _).toList ::: authors.map(Markup.META_CREATOR -> _) ::: contributors.map(Markup.META_CONTRIBUTOR -> _) ::: List(Markup.META_DATE -> RDF.date_format(date)) ::: List(Markup.META_LICENSE -> license) ::: proper_string(`abstract`).map(Markup.META_DESCRIPTION -> _).toList) } } class AFP private(options: Options, val base_dir: Path) { override def toString: String = base_dir.expand.toString val main_dir: Path = base_dir + Path.explode("thys") /* metadata */ private val entry_metadata: Map[String, Properties.T] = { val metadata_file = base_dir + Path.explode("metadata/metadata") var result = Map.empty[String, Properties.T] var section = "" var props = List.empty[Properties.Entry] val Section = """^\[(\S+)\]\s*$""".r val Property = """^(\S+)\s*=(.*)$""".r val Extra_Line = """^\s+(.*)$""".r val Blank_Line = """^\s*$""".r def flush(): Unit = { if (section != "") result += (section -> props.reverse.filter(p => p._2.nonEmpty)) section = "" props = Nil } for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex) { def err(msg: String): Nothing = error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode))) line match { case Section(name) => flush(); section = name case Property(a, b) => if (section == "") err("Property without a section") props = (a -> b.trim) :: props case Extra_Line(line) => props match { case Nil => err("Extra line without a property") case (a, b) :: rest => props = (a, b + "\n" + line.trim) :: rest } case Blank_Line() => case _ => err("Bad input") } } flush() result } /* entries */ val entries_map: SortedMap[String, AFP.Entry] = { val entries = for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield { val metadata = entry_metadata.getOrElse(name, error("Entry without metadata: " + quote(name))) val sessions = Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name) AFP.Entry(name, metadata, sessions) } val entries_map = entries.foldLeft(SortedMap.empty[String, AFP.Entry]) { case (m, e) => m + (e.name -> e) } val extra_metadata = (for ((name, _) <- entry_metadata.iterator if !entries_map.isDefinedAt(name)) yield name). toList.sorted if (extra_metadata.nonEmpty) error("Meta data without entry: " + commas_quote(extra_metadata)) entries_map } val entries: List[AFP.Entry] = entries_map.toList.map(_._2) /* sessions */ val sessions_map: SortedMap[String, AFP.Entry] = entries.foldLeft(SortedMap.empty[String, AFP.Entry]) { case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e) } } val sessions: List[String] = entries.flatMap(_.sessions) val sessions_structure: Sessions.Structure = Sessions.load_structure(options, dirs = List(main_dir)). selection(Sessions.Selection(sessions = sessions.toList)) /* dependency graph */ private def sessions_deps(entry: AFP.Entry): List[String] = entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds).distinct.sorted lazy val entries_graph: Graph[String, Unit] = { val session_entries = entries.foldLeft(Map.empty[String, String]) { case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e.name) } } entries.foldLeft(Graph.empty[String, Unit]) { case (g, entry) => val e1 = entry.name sessions_deps(entry).foldLeft(g.default_node(e1, ())) { case (g1, s) => session_entries.get(s).filterNot(_ == e1).foldLeft(g1) { case (g2, e2) => try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) } catch { case exn: Graph.Cycles[_] => error(cat_lines(exn.cycles.map(cycle => "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") + " due to session " + quote(s)))) } } } } } def entries_graph_display: Graph_Display.Graph = Graph_Display.make_graph(entries_graph) def entries_json_text: String = (for (entry <- entries.iterator) yield { val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_)) val afp_deps = entries_graph.imm_preds(entry.name).toList """ {""" + JSON.Format(entry.name) + """: {"distrib_deps": """ + JSON.Format(distrib_deps) + """, "afp_deps": """ + JSON.Format(afp_deps) + """ } }""" }).mkString("[", ", ", "\n]\n") /* partition sessions */ def partition(n: Int): List[String] = n match { case 0 => Nil case 1 | 2 => val graph = sessions_structure.build_graph.restrict(sessions.toSet) val force_part1 = graph.all_preds(graph.all_succs(AFP.force_partition1.filter(graph.defined))).toSet val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a)) if (n == 1) part1 else part2 case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)") } } diff --git a/src/Pure/Admin/sync_repos.scala b/src/Pure/Admin/sync_repos.scala --- a/src/Pure/Admin/sync_repos.scala +++ b/src/Pure/Admin/sync_repos.scala @@ -1,113 +1,113 @@ /* Title: Pure/Admin/sync_repos.scala Author: Makarius Synchronize Isabelle + AFP repositories. */ package isabelle object Sync_Repos { def sync_repos(target: String, progress: Progress = new Progress, verbose: Boolean = false, thorough: Boolean = false, preserve_jars: Boolean = false, dry_run: Boolean = false, clean: Boolean = false, rev: String = "", afp_root: Option[Path] = None, afp_rev: String = "" ): Unit = { val target_dir = if (target.endsWith(":") || target.endsWith("/")) target else target + "/" val isabelle_hg = Mercurial.repository(Path.ISABELLE_HOME) val afp_hg = afp_root.map(Mercurial.repository(_)) val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit = hg.sync(dest, rev = r, progress = progress, verbose = verbose, thorough = thorough, dry_run = dry_run, clean = clean, filter = filter ::: more_filter) progress.echo("\n* Isabelle repository:") sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect /etc/ISABELLE_ID")) if (!dry_run) { Isabelle_System.with_tmp_dir("sync") { tmp_dir => val id_path = tmp_dir + Path.explode("ISABELLE_ID") File.write(id_path, isabelle_hg.id(rev = rev)) Isabelle_System.rsync(thorough = thorough, args = List(File.standard_path(id_path), target_dir + "etc/")) } } for (hg <- afp_hg) { progress.echo("\n* AFP repository:") sync(hg, target_dir + "AFP", afp_rev) } } val isabelle_tool = Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories", Scala_Project.here, { args => var afp_root: Option[Path] = None var clean = false var preserve_jars = false var thorough = false var afp_rev = "" var dry_run = false var rev = "" var verbose = false val getopts = Getopts(""" Usage: isabelle sync_repos [OPTIONS] TARGET Options are: - -A ROOT include AFP with given root directory + -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """) -J preserve *.jar files -C clean all unknown/ignored files on target (implies -n for testing; use option -f to confirm) -T thorough treatment of file content and directory times -a REV explicit AFP revision (default: state of working directory) -f force changes: no dry-run -n no changes: dry-run -r REV explicit revision (default: state of working directory) -v verbose Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync". Examples (without -f as "dry-run"): * quick testing - isabelle sync_repos -A '$AFP_BASE' -J -C testmachine:test/isabelle_afp + isabelle sync_repos -A: -J -C testmachine:test/isabelle_afp * accurate testing - isabelle sync_repos -A '$AFP_BASE' -T -C testmachine:test/isabelle_afp + isabelle sync_repos -A: -T -C testmachine:test/isabelle_afp """, - "A:" -> (arg => afp_root = Some(Path.explode(arg))), + "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))), "J" -> (_ => preserve_jars = true), "C" -> { _ => clean = true; dry_run = true }, "T" -> (_ => thorough = true), "a:" -> (arg => afp_rev = arg), "f" -> (_ => dry_run = false), "n" -> (_ => dry_run = true), "r:" -> (arg => rev = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) val target = more_args match { case List(target) => target case _ => getopts.usage() } val progress = new Console_Progress sync_repos(target, progress = progress, verbose = verbose, thorough = thorough, preserve_jars = preserve_jars, dry_run = dry_run, clean = clean, rev = rev, afp_root = afp_root, afp_rev = afp_rev) } ) }