# HG changeset patch # User wenzelm # Date 1507579685 -7200 # Node ID 9f6ec65f7a6efd25dbd39024aecc91f84aaf0631 # Parent 0b12755ccbb2c3e39e8b4eb6a1f4719a7ed1118b# Parent 49a3a0a6ffaf186f3f261c953799c58f18d3af45 merged diff -r 0b12755ccbb2 -r 9f6ec65f7a6e src/Pure/Admin/afp.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/afp.scala Mon Oct 09 22:08:05 2017 +0200 @@ -0,0 +1,77 @@ +/* Title: Pure/Admin/afp.scala + Author: Makarius + +Administrative support for the Archive of Formal Proofs. +*/ + +package isabelle + + +object AFP +{ + def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP = + new AFP(options, base_dir) + + sealed case class Entry(name: String, sessions: List[String]) +} + +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") + + + /* entries and sessions */ + + val entries: List[AFP.Entry] = + (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield { + val sessions = + Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name) + AFP.Entry(name, sessions) + }).sortBy(_.name) + + val sessions: List[String] = entries.flatMap(_.sessions) + + val sessions_structure: Sessions.T = + Sessions.load(options, dirs = List(main_dir)). + selection(Sessions.Selection(sessions = sessions.toList))._2 + + + /* dependency graph */ + + private def sessions_deps(entry: AFP.Entry): List[String] = + entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted + + val entries_graph: Graph[String, Unit] = + { + val session_entries = + (Multi_Map.empty[String, String] /: entries) { case (m1, e) => + (m1 /: e.sessions) { case (m2, s) => m2.insert(s, e.name) } + } + (Graph.empty[String, Unit] /: entries) { case (g, e1) => + val name1 = e1.name + val g1 = g.default_node(name1, ()) + (g1 /: sessions_deps(e1)) { case (g2, s2) => + (g2 /: session_entries.get_list(s2)) { case (g3, name2) => + if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1) + } + } + } + } + + 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") +} diff -r 0b12755ccbb2 -r 9f6ec65f7a6e src/Pure/General/graph_display.scala --- a/src/Pure/General/graph_display.scala Sun Oct 08 22:28:22 2017 +0200 +++ b/src/Pure/General/graph_display.scala Mon Oct 09 22:08:05 2017 +0200 @@ -60,5 +60,13 @@ import XML.Decode._ list(pair(pair(string, pair(string, x => x)), list(string)))(body) }) + + def make_graph[A]( + graph: isabelle.Graph[String, A], + name: (String, A) => String = (x: String, a: A) => x): Graph = + { + val entries = + (for ((x, (a, (ps, _))) <- graph.iterator) yield ((x, (name(x, a), Nil)), ps.toList)).toList + build_graph(entries) + } } - diff -r 0b12755ccbb2 -r 9f6ec65f7a6e src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun Oct 08 22:28:22 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Mon Oct 09 22:08:05 2017 +0200 @@ -116,7 +116,7 @@ overall_syntax: Outer_Syntax = Outer_Syntax.empty, imported_sources: List[(Path, SHA1.Digest)] = Nil, sources: List[(Path, SHA1.Digest)] = Nil, - session_graph: Graph_Display.Graph = Graph_Display.empty_graph, + session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph, errors: List[String] = Nil, imports: Option[Base] = None) { @@ -253,7 +253,7 @@ progress, overall_syntax.keywords, check_keywords, theory_files) } - val session_graph: Graph_Display.Graph = + val session_graph_display: Graph_Display.Graph = { def session_node(name: String): Graph_Display.Node = Graph_Display.Node("[" + name + "]", "session." + name) @@ -303,7 +303,7 @@ overall_syntax = overall_syntax, imported_sources = check_sources(imported_files), sources = check_sources(session_files), - session_graph = session_graph, + session_graph_display = session_graph_display, errors = thy_deps.errors ::: sources_errors, imports = Some(imports_base)) @@ -479,6 +479,9 @@ val build_graph: Graph[String, Info], val imports_graph: Graph[String, Info]) { + def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph) + def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph) + def apply(name: String): Info = imports_graph.get_node(name) def get(name: String): Option[Info] = if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None @@ -550,26 +553,26 @@ (THEORIES, Keyword.QUASI_COMMAND) + (DOCUMENT_FILES, Keyword.QUASI_COMMAND) + abstract class Entry + sealed case class Chapter(name: String) extends Entry + sealed case class Session_Entry( + pos: Position.T, + name: String, + groups: List[String], + path: String, + parent: Option[String], + description: String, + options: List[Options.Spec], + imports: List[String], + theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])], + document_files: List[(String, String)]) extends Entry + { + def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] = + theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) }) + } + private object Parser extends Parse.Parser with Options.Parser { - private abstract class Entry - private sealed case class Chapter(name: String) extends Entry - private sealed case class Session_Entry( - pos: Position.T, - name: String, - groups: List[String], - path: String, - parent: Option[String], - description: String, - options: List[Options.Spec], - imports: List[String], - theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])], - document_files: List[(String, String)]) extends Entry - { - def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] = - theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) }) - } - private val chapter: Parser[Chapter] = { val chapter_name = atom("chapter name", _.is_name) @@ -618,70 +621,88 @@ Session_Entry(pos, a, b, c, d, e, f, g, h, i) } } - def parse_root(options: Options, select: Boolean, path: Path): List[(String, Info)] = + def parse_root(path: Path): List[Entry] = { - def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) = - { - try { - val name = entry.name - - if (name == "" || name == DRAFT) error("Bad session name") - if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session") - if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session") - - val session_options = options ++ entry.options - - val theories = - entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) }) - - val global_theories = - for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global } - yield { - val thy_name = Path.explode(thy).expand.base_name - if (Long_Name.is_qualified(thy_name)) - error("Bad qualified name for global theory " + - quote(thy_name) + Position.here(pos)) - else thy_name - } - - val document_files = - entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) - - val meta_digest = - SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports, - entry.theories_no_position, entry.document_files).toString) - - val info = - Info(name, entry_chapter, select, entry.pos, entry.groups, - path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options, - entry.imports, theories, global_theories, document_files, meta_digest) - - (name, info) - } - catch { - case ERROR(msg) => - error(msg + "\nThe error(s) above occurred in session entry " + - quote(entry.name) + Position.here(entry.pos)) - } - } - val toks = Token.explode(root_syntax.keywords, File.read(path)) val start = Token.Pos.file(path.implode) parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match { - case Success(result, _) => - var entry_chapter = "Unsorted" - val infos = new mutable.ListBuffer[(String, Info)] - result.foreach { - case Chapter(name) => entry_chapter = name - case entry: Session_Entry => infos += make_info(entry_chapter, entry) - } - infos.toList + case Success(result, _) => result case bad => error(bad.toString) } } } + def parse_root(path: Path): List[Entry] = Parser.parse_root(path) + + def parse_root_entries(path: Path): List[Session_Entry] = + for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry]) + yield entry.asInstanceOf[Session_Entry] + + def read_root(options: Options, select: Boolean, path: Path): List[(String, Info)] = + { + def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) = + { + try { + val name = entry.name + + if (name == "" || name == DRAFT) error("Bad session name") + if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session") + if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session") + + val session_options = options ++ entry.options + + val theories = + entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) }) + + val global_theories = + for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global } + yield { + val thy_name = Path.explode(thy).expand.base_name + if (Long_Name.is_qualified(thy_name)) + error("Bad qualified name for global theory " + + quote(thy_name) + Position.here(pos)) + else thy_name + } + + val document_files = + entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) + + val meta_digest = + SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports, + entry.theories_no_position, entry.document_files).toString) + + val info = + Info(name, entry_chapter, select, entry.pos, entry.groups, + path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options, + entry.imports, theories, global_theories, document_files, meta_digest) + + (name, info) + } + catch { + case ERROR(msg) => + error(msg + "\nThe error(s) above occurred in session entry " + + quote(entry.name) + Position.here(entry.pos)) + } + } + + var entry_chapter = "Unsorted" + val infos = new mutable.ListBuffer[(String, Info)] + parse_root(path).foreach { + case Chapter(name) => entry_chapter = name + case entry: Session_Entry => infos += make_info(entry_chapter, entry) + } + infos.toList + } + + def parse_roots(roots: Path): List[String] = + { + for { + line <- split_lines(File.read(roots)) + if !(line == "" || line.startsWith("#")) + } yield line + } + /* load sessions from certain directories */ @@ -714,10 +735,9 @@ val roots = dir + ROOTS if (roots.is_file) { for { - line <- split_lines(File.read(roots)) - if !(line == "" || line.startsWith("#")) + entry <- parse_roots(roots) dir1 = - try { check_session_dir(dir + Path.explode(line)) } + try { check_session_dir(dir + Path.explode(entry)) } catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString) @@ -743,7 +763,7 @@ } }).toList.map(_._2) - make(unique_roots.flatMap(p => Parser.parse_root(options, p._1, p._2))) + make(unique_roots.flatMap(p => read_root(options, p._1, p._2))) } diff -r 0b12755ccbb2 -r 9f6ec65f7a6e src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Oct 08 22:28:22 2017 +0200 +++ b/src/Pure/Tools/build.scala Mon Oct 09 22:08:05 2017 +0200 @@ -198,7 +198,7 @@ } private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf") - isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph) + isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display) private val future_result: Future[Process_Result] = Future.thread("build") { diff -r 0b12755ccbb2 -r 9f6ec65f7a6e src/Pure/build-jars --- a/src/Pure/build-jars Sun Oct 08 22:28:22 2017 +0200 +++ b/src/Pure/build-jars Mon Oct 09 22:08:05 2017 +0200 @@ -9,6 +9,7 @@ ## sources declare -a SOURCES=( + Admin/afp.scala Admin/build_cygwin.scala Admin/build_doc.scala Admin/build_history.scala