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,208 +1,201 @@ /* 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 BASE: Path = Path.explode("$AFP_BASE") def main_dir(base_dir: Path = BASE): Path = base_dir + Path.explode("thys") def make_dirs(afp_root: Option[Path]): List[Path] = afp_root match { case None => Nil case Some(base_dir) => List(main_dir(base_dir = base_dir)) } 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 = AFP.main_dir(base_dir = base_dir) /* 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, File.standard_path(metadata_file)))) 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") } diff --git a/src/Pure/Admin/build_status.scala b/src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala +++ b/src/Pure/Admin/build_status.scala @@ -1,640 +1,640 @@ /* Title: Pure/Admin/build_status.scala Author: Makarius Present recent build status information from database. */ package isabelle object Build_Status { /* defaults */ val default_target_dir = Path.explode("build_status") val default_image_size = (800, 600) val default_history = 30 def default_profiles: List[Profile] = Isabelle_Cronjob.build_status_profiles /* data profiles */ sealed case class Profile( description: String, history: Int = 0, afp: Boolean = false, bulky: Boolean = false, sql: String = "" ) { def days(options: Options): Int = options.int("build_log_history") max history def stretch(options: Options): Double = (days(options) max default_history min (default_history * 5)).toDouble / default_history def select( options: Options, ml_statistics: Boolean = false, only_sessions: Set[String] = Set.empty ): PostgreSQL.Source = { val columns = List( Build_Log.Column.pull_date(afp = false), Build_Log.Column.pull_date(afp = true), Build_Log.Prop.build_start, Build_Log.Prop.build_host, Build_Log.Prop.isabelle_version, Build_Log.Prop.afp_version, Build_Log.Settings.ISABELLE_BUILD_OPTIONS, Build_Log.Settings.ML_PLATFORM, Build_Log.Column.log_name, Build_Log.Column.session_name, Build_Log.Column.chapter, Build_Log.Column.groups, Build_Log.Column.threads, Build_Log.Column.timing_elapsed, Build_Log.Column.timing_cpu, Build_Log.Column.timing_gc, Build_Log.Column.ml_timing_elapsed, Build_Log.Column.ml_timing_cpu, Build_Log.Column.ml_timing_gc, Build_Log.Column.heap_size, Build_Log.Column.status, Build_Log.Column.errors) ::: (if (ml_statistics) List(Build_Log.Column.ml_statistics) else Nil) Build_Log.private_data.universal_table.select(columns, distinct = true, sql = SQL.where_and( Build_Log.private_data.recent(Build_Log.Column.pull_date(afp), days(options)), Build_Log.Column.status.member( List( Build_Log.Session_Status.finished.toString, Build_Log.Session_Status.failed.toString)), if_proper(only_sessions, Build_Log.Column.session_name.member(only_sessions)), if_proper(sql, SQL.enclose(sql)))) } } /* build status */ def build_status(options: Options, progress: Progress = new Progress, profiles: List[Profile] = default_profiles, only_sessions: Set[String] = Set.empty, target_dir: Path = default_target_dir, ml_statistics: Boolean = false, image_size: (Int, Int) = default_image_size ): Unit = { val ml_statistics_domain = Iterator(ML_Statistics.heap_fields, ML_Statistics.program_fields, ML_Statistics.tasks_fields, ML_Statistics.workers_fields).flatMap(_._2).toSet val data = read_data(options, progress = progress, profiles = profiles, only_sessions = only_sessions, ml_statistics = ml_statistics, ml_statistics_domain = ml_statistics_domain) present_data(data, progress = progress, target_dir = target_dir, image_size = image_size) } /* read data */ sealed case class Data(date: Date, entries: List[Data_Entry]) sealed case class Data_Entry( name: String, hosts: List[String], stretch: Double, sessions: List[Session] ) { def failed_sessions: List[Session] = sessions.filter(_.head.failed).sortBy(_.name) } sealed case class Session( name: String, threads: Int, entries: Map[String, Entry], ml_statistics: ML_Statistics, ml_statistics_date: Long ) { require(entries.nonEmpty, "no entries") lazy val sorted_entries: List[Entry] = entries.valuesIterator.toList.sortBy(entry => - entry.date) def head: Entry = sorted_entries.head def order: Long = - head.timing.elapsed.ms def finished_entries: List[Entry] = sorted_entries.filter(_.finished) def finished_entries_size: Int = finished_entries.map(_.date).toSet.size def check_timing: Boolean = finished_entries_size >= 3 def check_heap: Boolean = finished_entries_size >= 3 && finished_entries.forall(entry => entry.maximum_heap.is_proper || entry.average_heap.is_proper || entry.stored_heap.is_proper) def make_csv: CSV.File = { val header = List("session_name", "chapter", "build_date", "pull_date", "afp_pull_date", "isabelle_version", "afp_version", "timing_elapsed", "timing_cpu", "timing_gc", "ml_timing_elapsed", "ml_timing_cpu", "ml_timing_gc", "maximum_code", "average_code", "maximum_stack", "average_stack", "maximum_heap", "average_heap", "stored_heap", "status") val date_format = Date.Format("uuuu-MM-dd HH:mm:ss") val records = for (entry <- sorted_entries) yield { CSV.Record(name, entry.chapter, date_format(entry.build_start), date_format(entry.pull_date), entry.afp_pull_date match { case Some(date) => date_format(date) case None => "" }, entry.isabelle_version, entry.afp_version, entry.timing.elapsed.ms, entry.timing.cpu.ms, entry.timing.gc.ms, entry.ml_timing.elapsed.ms, entry.ml_timing.cpu.ms, entry.ml_timing.gc.ms, entry.maximum_code, entry.average_code, entry.maximum_stack, entry.average_stack, entry.maximum_heap, entry.average_heap, entry.stored_heap, entry.status) } CSV.File(name, header, records) } } sealed case class Entry( chapter: String, build_start: Date, pull_date: Date, afp_pull_date: Option[Date], isabelle_version: String, afp_version: String, timing: Timing, ml_timing: Timing, maximum_code: Space, average_code: Space, maximum_stack: Space, average_stack: Space, maximum_heap: Space, average_heap: Space, stored_heap: Space, status: Build_Log.Session_Status, errors: List[String] ) { val date: Long = (afp_pull_date getOrElse pull_date).unix_epoch def finished: Boolean = status == Build_Log.Session_Status.finished def failed: Boolean = status == Build_Log.Session_Status.failed def present_errors(name: String): XML.Body = { if (errors.isEmpty) HTML.text(name + print_version(isabelle_version, afp_version, chapter)) else { HTML.tooltip_errors(HTML.text(name), errors.map(s => HTML.text(Symbol.decode(s)))) :: HTML.text(print_version(isabelle_version, afp_version, chapter)) } } } sealed case class Image(name: String, width: Int, height: Int) { def path: Path = Path.basic(name) } def print_version( isabelle_version: String, afp_version: String = "", chapter: String = AFP.chapter ): String = { val body = proper_string(isabelle_version).map("Isabelle/" + _).toList ::: (if (chapter == AFP.chapter) proper_string(afp_version).map("AFP/" + _) else None).toList if_proper(body, body.mkString(" (", ", ", ")")) } def read_data(options: Options, progress: Progress = new Progress, profiles: List[Profile] = default_profiles, only_sessions: Set[String] = Set.empty, ml_statistics: Boolean = false, ml_statistics_domain: String => Boolean = _ => true ): Data = { val date = Date.now() var data_hosts = Map.empty[String, Set[String]] var data_stretch = Map.empty[String, Double] var data_entries = Map.empty[String, Map[String, Session]] def get_hosts(data_name: String): Set[String] = data_hosts.getOrElse(data_name, Set.empty) val store = Build_Log.store(options) using(store.open_database()) { db => for (profile <- profiles.sortBy(_.description)) { progress.echo("input " + quote(profile.description)) val afp = profile.afp val Threads_Option = """threads\s*=\s*(\d+)""".r val sql = profile.select(options, ml_statistics = ml_statistics, only_sessions = only_sessions) progress.echo(sql, verbose = true) db.using_statement(sql) { stmt => using(stmt.execute_query()) { res => while (res.next()) { val log_name = res.string(Build_Log.Column.log_name) val session_name = res.string(Build_Log.Column.session_name) val chapter = res.string(Build_Log.Column.chapter) val groups = split_lines(res.string(Build_Log.Column.groups)) val threads = { val threads1 = res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match { case Threads_Option(Value.Int(i)) => i case _ => 1 } val threads2 = res.get_int(Build_Log.Column.threads).getOrElse(1) threads1 max threads2 } val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM) val ml_platform_64 = ml_platform.startsWith("x86_64-") || ml_platform.startsWith("arm64-") val data_name = profile.description + (if (ml_platform_64) ", 64bit" else "") + (if (threads == 1) "" else ", " + threads + " threads") res.get_string(Build_Log.Prop.build_host).foreach(host => data_hosts += (data_name -> (get_hosts(data_name) + host))) data_stretch += (data_name -> profile.stretch(options)) val isabelle_version = res.string(Build_Log.Prop.isabelle_version) val afp_version = res.string(Build_Log.Prop.afp_version) val ml_stats = ML_Statistics( if (ml_statistics) { Properties.uncompress( res.bytes(Build_Log.Column.ml_statistics), cache = store.cache) } else Nil, domain = ml_statistics_domain, heading = session_name + print_version(isabelle_version, afp_version, chapter)) val entry = Entry( chapter = chapter, build_start = res.date(Build_Log.Prop.build_start), pull_date = res.date(Build_Log.Column.pull_date(afp = false)), afp_pull_date = if (afp) res.get_date(Build_Log.Column.pull_date(afp = true)) else None, isabelle_version = isabelle_version, afp_version = afp_version, timing = res.timing( Build_Log.Column.timing_elapsed, Build_Log.Column.timing_cpu, Build_Log.Column.timing_gc), ml_timing = res.timing( Build_Log.Column.ml_timing_elapsed, Build_Log.Column.ml_timing_cpu, Build_Log.Column.ml_timing_gc), maximum_code = Space.B(ml_stats.maximum(ML_Statistics.CODE_SIZE)), average_code = Space.B(ml_stats.average(ML_Statistics.CODE_SIZE)), maximum_stack = Space.B(ml_stats.maximum(ML_Statistics.STACK_SIZE)), average_stack = Space.B(ml_stats.average(ML_Statistics.STACK_SIZE)), maximum_heap = Space.B(ml_stats.maximum(ML_Statistics.HEAP_SIZE)), average_heap = Space.B(ml_stats.average(ML_Statistics.HEAP_SIZE)), stored_heap = Space.bytes(res.long(Build_Log.Column.heap_size)), status = Build_Log.Session_Status.valueOf(res.string(Build_Log.Column.status)), errors = Build_Log.uncompress_errors( res.bytes(Build_Log.Column.errors), cache = store.cache)) val sessions = data_entries.getOrElse(data_name, Map.empty) val session = sessions.get(session_name) match { case None => val entries = Map(log_name -> entry) Some(Session(session_name, threads, entries, ml_stats, entry.date)) case Some(old) if !old.entries.isDefinedAt(log_name) => val entries1 = old.entries + (log_name -> entry) val (ml_stats1, ml_stats1_date) = if (entry.date > old.ml_statistics_date) (ml_stats, entry.date) else (old.ml_statistics, old.ml_statistics_date) Some(Session(session_name, threads, entries1, ml_stats1, ml_stats1_date)) case Some(_) => None } if (session.isDefined && (!afp || chapter == AFP.chapter) && - (!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) { + (!profile.bulky || groups.exists(Sessions.bulky_groups))) { data_entries += (data_name -> (sessions + (session_name -> session.get))) } } } } } } val sorted_entries = (for { (name, sessions) <- data_entries.toList sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order)) } yield { val hosts = get_hosts(name).toList.sorted val stretch = data_stretch(name) Data_Entry(name, hosts, stretch, sorted_sessions) }).sortBy(_.name) Data(date, sorted_entries) } /* present data */ def present_data(data: Data, progress: Progress = new Progress, target_dir: Path = default_target_dir, image_size: (Int, Int) = default_image_size ): Unit = { def clean_name(name: String): String = name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString) HTML.write_document(target_dir, "index.html", List(HTML.title("Isabelle build status")), List(HTML.chapter("Isabelle build status"), HTML.par( List(HTML.description( List(HTML.text("status date:") -> HTML.text(data.date.toString))))), HTML.par( List(HTML.itemize(data.entries.map(data_entry => List( HTML.link(clean_name(data_entry.name) + "/index.html", HTML.text(data_entry.name))) ::: (data_entry.failed_sessions match { case Nil => Nil case sessions => HTML.break ::: List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) ::: List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name)))) }) )))))) for (data_entry <- data.entries) { val data_name = data_entry.name val (image_width, image_height) = image_size val image_width_stretch = (image_width * data_entry.stretch).toInt progress.echo("output " + quote(data_name)) val dir = Isabelle_System.make_directory(target_dir + Path.basic(clean_name(data_name))) val data_files = (for (session <- data_entry.sessions) yield { val csv_file = session.make_csv csv_file.write(dir) session.name -> csv_file }).toMap val session_plots = Par_List.map((session: Session) => Isabelle_System.with_tmp_file(session.name, "data") { data_file => Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file => def plot_name(kind: String): String = session.name + "_" + kind + ".png" File.write(data_file, cat_lines( session.finished_entries.map(entry => List(entry.date.toString, entry.timing.elapsed.minutes.toString, entry.timing.resources.minutes.toString, entry.ml_timing.elapsed.minutes.toString, entry.ml_timing.resources.minutes.toString, entry.maximum_code.MiB.toString, entry.average_code.MiB.toString, entry.maximum_stack.MiB.toString, entry.average_stack.MiB.toString, entry.maximum_heap.MiB.toString, entry.average_heap.MiB.toString, entry.stored_heap.MiB.toString).mkString(" ")))) val max_time = (session.finished_entries.foldLeft(0.0) { case (m, entry) => m.max(entry.timing.elapsed.minutes). max(entry.timing.resources.minutes). max(entry.ml_timing.elapsed.minutes). max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1 val timing_range = "[0:" + max_time + "]" def gnuplot(plot_name: String, plots: List[String], range: String): Image = { val image = Image(plot_name, image_width_stretch, image_height) File.write(gnuplot_file, """ set terminal png size """ + image.width + "," + image.height + """ set output """ + quote(File.standard_path(dir + image.path)) + """ set xdata time set timefmt "%s" set format x "%d-%b" set xlabel """ + quote(session.name) + """ noenhanced set key left bottom plot [] """ + range + " " + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n") val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file)) if (!result.ok) result.error("Gnuplot failed for " + data_name + "/" + plot_name).check image } val timing_plots = { val plots1 = List( """ using 1:2 smooth sbezier title "elapsed time (smooth)" """, """ using 1:2 smooth csplines title "elapsed time" """) val plots2 = List( """ using 1:3 smooth sbezier title "cpu time (smooth)" """, """ using 1:3 smooth csplines title "cpu time" """) if (session.threads == 1) plots1 else plots1 ::: plots2 } val ml_timing_plots = List( """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """, """ using 1:4 smooth csplines title "ML elapsed time" """, """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """, """ using 1:5 smooth csplines title "ML cpu time" """) val heap_plots = List( """ using 1:10 smooth sbezier title "heap maximum (smooth)" """, """ using 1:10 smooth csplines title "heap maximum" """, """ using 1:11 smooth sbezier title "heap average (smooth)" """, """ using 1:11 smooth csplines title "heap average" """, """ using 1:12 smooth sbezier title "heap stored (smooth)" """, """ using 1:12 smooth csplines title "heap stored" """) def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image = { val image = Image(plot_name, image_width, image_height) val chart = session.ml_statistics.chart( fields.title + ": " + session.ml_statistics.heading, fields.names) Graphics_File.write_chart_png( (dir + image.path).file, chart, image.width, image.height) image } val images = (if (session.check_timing) List( gnuplot(plot_name("timing"), timing_plots, timing_range), gnuplot(plot_name("ml_timing"), ml_timing_plots, timing_range)) else Nil) ::: (if (session.check_heap) List(gnuplot(plot_name("heap"), heap_plots, "[0:]")) else Nil) ::: (if (session.ml_statistics.content.nonEmpty) List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields), jfreechart(plot_name("program_chart"), ML_Statistics.program_fields)) ::: (if (session.threads > 1) List( jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields), jfreechart(plot_name("workers_chart"), ML_Statistics.workers_fields)) else Nil) else Nil) session.name -> images } }, data_entry.sessions).toMap HTML.write_document(dir, "index.html", List(HTML.title("Isabelle build status for " + data_name)), HTML.chapter("Isabelle build status for " + data_name) :: HTML.par( List(HTML.description( List( HTML.text("status date:") -> HTML.text(data.date.toString), HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) :: HTML.par( List(HTML.itemize( data_entry.sessions.map(session => HTML.link("#session_" + session.name, HTML.text(session.name)) :: HTML.text(" (" + session.head.timing.message_resources + ")"))))) :: data_entry.sessions.flatMap(session => List( HTML.section(HTML.id("session_" + session.name), session.name), HTML.par( HTML.description( List( HTML.text("data:") -> List(HTML.link(data_files(session.name).file_name, HTML.text("CSV"))), HTML.text("timing:") -> HTML.text(session.head.timing.message_resources), HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) ::: session.head.maximum_code.print_relevant.map(s => HTML.text("code maximum:") -> HTML.text(s)).toList ::: session.head.average_code.print_relevant.map(s => HTML.text("code average:") -> HTML.text(s)).toList ::: session.head.maximum_stack.print_relevant.map(s => HTML.text("stack maximum:") -> HTML.text(s)).toList ::: session.head.average_stack.print_relevant.map(s => HTML.text("stack average:") -> HTML.text(s)).toList ::: session.head.maximum_heap.print_relevant.map(s => HTML.text("heap maximum:") -> HTML.text(s)).toList ::: session.head.average_heap.print_relevant.map(s => HTML.text("heap average:") -> HTML.text(s)).toList ::: session.head.stored_heap.print_relevant.map(s => HTML.text("heap stored:") -> HTML.text(s)).toList ::: proper_string(session.head.isabelle_version).map(s => HTML.text("Isabelle version:") -> HTML.text(s)).toList ::: proper_string(session.head.afp_version).map(s => HTML.text("AFP version:") -> HTML.text(s)).toList) :: session_plots.getOrElse(session.name, Nil).map(image => HTML.size(image.width / 2, image.height / 2)(HTML.image(image.name))))))) } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_status", "present recent build status information from database", Scala_Project.here, { args => var target_dir = default_target_dir var ml_statistics = false var only_sessions = Set.empty[String] var options = Options.init() var image_size = default_image_size var verbose = false val getopts = Getopts(""" Usage: isabelle build_status [OPTIONS] Options are: -D DIR target directory (default """ + default_target_dir + """) -M include full ML statistics -S SESSIONS only given SESSIONS (comma separated) -l DAYS length of relevant history (default """ + options.int("build_log_history") + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -s WxH size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """) -v verbose Present performance statistics from build log database, which is specified via system options build_log_database_host, build_log_database_user, build_log_history etc. """, "D:" -> (arg => target_dir = Path.explode(arg)), "M" -> (_ => ml_statistics = true), "S:" -> (arg => only_sessions = space_explode(',', arg).toSet), "l:" -> (arg => options = options + ("build_log_history=" + arg)), "o:" -> (arg => options = options + arg), "s:" -> (arg => space_explode('x', arg).map(Value.Int.parse) match { case List(w, h) if w > 0 && h > 0 => image_size = (w, h) case _ => error("Error bad PNG image size: " + quote(arg)) }), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress(verbose = verbose) build_status(options, progress = progress, only_sessions = only_sessions, target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size) }) } diff --git a/src/Pure/Build/sessions.scala b/src/Pure/Build/sessions.scala --- a/src/Pure/Build/sessions.scala +++ b/src/Pure/Build/sessions.scala @@ -1,1333 +1,1364 @@ /* Title: Pure/Build/sessions.scala Author: Makarius Cumulative session information. */ package isabelle import java.io.{File => JFile} import scala.collection.immutable.{SortedSet, SortedMap} import scala.collection.mutable object Sessions { /* main operations */ def background0(session: String): Background = Background.empty(session) def background(options: Options, session: String, progress: Progress = new Progress, dirs: List[Path] = Nil, include_sessions: List[String] = Nil, session_ancestor: Option[String] = None, session_requirements: Boolean = false ): Background = { Background.load(options, session, progress = progress, dirs = dirs, include_sessions = include_sessions, session_ancestor = session_ancestor, session_requirements = session_requirements) } def load_structure( options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, infos: List[Info] = Nil, augment_options: String => List[Options.Spec] = _ => Nil ): Structure = { val roots = load_root_files(dirs = dirs, select_dirs = select_dirs) Structure.make(options, augment_options, roots = roots, infos = infos) } def deps(sessions_structure: Structure, progress: Progress = new Progress, inlined_files: Boolean = false, list_files: Boolean = false, check_keywords: Set[String] = Set.empty ): Deps = { Deps.load(sessions_structure, progress = progress, inlined_files = inlined_files, list_files = list_files, check_keywords = check_keywords) } /* session and theory names */ val ROOTS: Path = Path.explode("ROOTS") val ROOT: Path = Path.explode("ROOT") val roots_name: String = "ROOTS" val root_name: String = "ROOT" val theory_import: String = "Pure.Sessions" val UNSORTED = "Unsorted" val DRAFT = "Draft" def is_pure(name: String): Boolean = name == Thy_Header.PURE def illegal_session(name: String): Boolean = name == "" || name == DRAFT def illegal_theory(name: String): Boolean = name == root_name || File_Format.registry.theory_excluded(name) /* ROOTS file format */ class ROOTS_File_Format extends File_Format { val format_name: String = roots_name val file_ext = "" override def detect(name: String): Boolean = Url.get_base_name(name) match { case Some(base_name) => base_name == roots_name case None => false } override def theory_suffix: String = "ROOTS_file" override def theory_content(name: String): String = """theory "ROOTS" imports Pure begin ROOTS_file "." end""" override def theory_excluded(name: String): Boolean = name == "ROOTS" } /* base info */ object Base { val bootstrap: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax) } sealed case class Base( session_name: String = "", session_pos: Position.T = Position.none, proper_session_theories: List[Document.Node.Name] = Nil, document_theories: List[Document.Node.Name] = Nil, loaded_theories: Graph[String, Outer_Syntax] = Graph.string, // cumulative imports used_theories: List[(Document.Node.Name, Options)] = Nil, // new imports theory_load_commands: Map[String, List[Command_Span.Span]] = Map.empty, known_theories: Map[String, Document.Node.Entry] = Map.empty, known_loaded_files: Map[String, List[Path]] = Map.empty, overall_syntax: Outer_Syntax = Outer_Syntax.empty, imported_sources: List[(Path, SHA1.Digest)] = Nil, session_sources: List[(Path, SHA1.Digest)] = Nil, session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph, errors: List[String] = Nil ) { def session_entry: (String, Base) = session_name -> this override def toString: String = "Sessions.Base(" + print_body + ")" def print_body: String = "session_name = " + quote(session_name) + ", loaded_theories = " + loaded_theories.size + ", used_theories = " + used_theories.length def all_sources: List[(Path, SHA1.Digest)] = imported_sources ::: session_sources def all_document_theories: List[Document.Node.Name] = proper_session_theories ::: document_theories def loaded_theory(name: String): Boolean = loaded_theories.defined(name) def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory) def loaded_theory_syntax(name: String): Option[Outer_Syntax] = if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] = loaded_theory_syntax(name.theory) def theory_syntax(name: Document.Node.Name): Outer_Syntax = loaded_theory_syntax(name) getOrElse overall_syntax def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax = nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax } /* background context */ object Background { def empty(session: String): Background = Background(Base(session_name = session)) def load(options: Options, session: String, progress: Progress = new Progress, dirs: List[Path] = Nil, include_sessions: List[String] = Nil, session_ancestor: Option[String] = None, session_requirements: Boolean = false ): Background = { val full_sessions = load_structure(options, dirs = dirs) val selected_sessions = full_sessions.selection(Selection(sessions = session :: session_ancestor.toList)) val info = selected_sessions(session) val ancestor = session_ancestor orElse info.parent val (session1, infos1) = if (session_requirements && ancestor.isDefined) { val deps = Sessions.deps(selected_sessions, progress = progress) val base = deps(session) val ancestor_loaded = deps.get(ancestor.get) match { case Some(ancestor_base) if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) => ancestor_base.loaded_theories.defined _ case _ => error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session)) } val required_theories = for { thy <- base.loaded_theories.keys if !ancestor_loaded(thy) && selected_sessions.theory_qualifier(thy) != session } yield thy if (required_theories.isEmpty) (ancestor.get, Nil) else { val other_name = info.name + "_requirements(" + ancestor.get + ")" Isabelle_System.isabelle_tmp_prefix() (other_name, List( Info.make( Chapter_Defs.empty, Options.init0(), info.options, augment_options = _ => Nil, dir_selected = false, dir = Path.explode("$ISABELLE_TMP_PREFIX"), chapter = info.chapter, Session_Entry( pos = info.pos, name = other_name, groups = info.groups, path = ".", parent = ancestor, description = "Required theory imports from other sessions", options = Nil, imports = info.deps, directories = Nil, theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))), document_theories = Nil, document_files = Nil, export_files = Nil, export_classpath = Nil)))) } } else (session, Nil) val full_sessions1 = if (infos1.isEmpty) full_sessions else load_structure(options, dirs = dirs, infos = infos1) val selected_sessions1 = full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions)) val deps1 = Sessions.deps(selected_sessions1, progress = progress) Background(deps1(session1), sessions_structure = full_sessions1, errors = deps1.errors, infos = infos1) } } sealed case class Background( base: Base, sessions_structure: Structure = Structure.empty, errors: List[String] = Nil, infos: List[Info] = Nil ) { def session_name: String = base.session_name def info: Info = sessions_structure(session_name) def check_errors: Background = if (errors.isEmpty) this else error(cat_lines(errors)) } /* source dependencies */ object Deps { def load(sessions_structure: Structure, progress: Progress = new Progress, inlined_files: Boolean = false, list_files: Boolean = false, check_keywords: Set[String] = Set.empty ): Deps = { var cache_sources = Map.empty[JFile, SHA1.Digest] def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = { for { path <- paths file = path.file if cache_sources.isDefinedAt(file) || file.isFile } yield { cache_sources.get(file) match { case Some(digest) => (path, digest) case None => val digest = SHA1.digest(file) cache_sources = cache_sources + (file -> digest) (path, digest) } } } val session_bases = sessions_structure.imports_topological_order.foldLeft(Map(Base.bootstrap.session_entry)) { case (session_bases, session_name) => progress.expose_interrupt() val info = sessions_structure(session_name) try { val deps_base = info.deps_base(session_bases) val session_background = Background(base = deps_base, sessions_structure = sessions_structure) val resources = new Resources(session_background) progress.echo( "Session " + info.chapter + "/" + session_name + if_proper(info.groups, info.groups.mkString(" (", " ", ")")), verbose = !list_files) val dependencies = resources.session_dependencies(info) val overall_syntax = dependencies.overall_syntax val proper_session_theories = dependencies.theories.filter(name => sessions_structure.theory_qualifier(name) == session_name) val theory_files = dependencies.theories.map(_.path) val (load_commands, load_commands_errors) = try { if (inlined_files) (dependencies.load_commands, Nil) else (Nil, Nil) } catch { case ERROR(msg) => (Nil, List(msg)) } val theory_load_commands = (for ((name, span) <- load_commands.iterator) yield name.theory -> span).toMap val loaded_files: List[(String, List[Path])] = for ((name, spans) <- load_commands) yield { val (theory, files) = dependencies.loaded_files(name, spans) theory -> files.map(file => Path.explode(file.node)) } val document_files = for ((path1, path2) <- info.document_files) yield info.dir + path1 + path2 val session_files = (theory_files ::: loaded_files.flatMap(_._2) ::: document_files).map(_.expand) val imported_files = if (inlined_files) dependencies.imported_files else Nil if (list_files) { progress.echo(cat_lines(session_files.map(_.implode).sorted.map(" " + _))) } if (check_keywords.nonEmpty) { Check_Keywords.check_keywords( progress, overall_syntax.keywords, check_keywords, theory_files) } val session_graph_display: Graph_Display.Graph = { def session_node(name: String): Graph_Display.Node = Graph_Display.Node("[" + name + "]", "session." + name) def node(name: Document.Node.Name): Graph_Display.Node = { val qualifier = sessions_structure.theory_qualifier(name) if (qualifier == info.name) { Graph_Display.Node(name.theory_base_name, "theory." + name.theory) } else session_node(qualifier) } val required_sessions = dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory)) .map(theory => sessions_structure.theory_qualifier(theory)) .filter(name => name != info.name && sessions_structure.defined(name)) val required_subgraph = sessions_structure.imports_graph .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet) .transitive_closure .restrict(required_sessions.toSet) .transitive_reduction_acyclic val graph0 = required_subgraph.topological_order.foldLeft(Graph_Display.empty_graph) { case (g, session) => val a = session_node(session) val bs = required_subgraph.imm_preds(session).toList.map(session_node) bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a)) } dependencies.entries.foldLeft(graph0) { case (g, entry) => val a = node(entry.name) val bs = entry.header.imports.map(node).filterNot(_ == a) bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a)) } } val known_theories = dependencies.entries.iterator.map(entry => entry.name.theory -> entry). foldLeft(deps_base.known_theories)(_ + _) val known_loaded_files = deps_base.known_loaded_files ++ loaded_files val import_errors = { val known_sessions = sessions_structure.imports_requirements(List(session_name)).toSet for { name <- dependencies.theories qualifier = sessions_structure.theory_qualifier(name) if !known_sessions(qualifier) } yield "Bad import of theory " + quote(name.toString) + ": need to include sessions " + quote(qualifier) + " in ROOT" } val document_errors = info.document_theories.flatMap( { case (thy, pos) => val build_hierarchy = if (sessions_structure.build_graph.defined(session_name)) { sessions_structure.build_hierarchy(session_name) } else Nil def err(msg: String): Option[String] = Some(msg + " " + quote(thy) + Position.here(pos)) known_theories.get(thy).map(_.name) match { case None => err("Unknown document theory") case Some(name) => val qualifier = sessions_structure.theory_qualifier(name) if (proper_session_theories.contains(name)) { err("Redundant document theory from this session:") } else if ( !build_hierarchy.contains(qualifier) && !dependencies.theories.contains(name) ) { err("Document theory from other session not imported properly:") } else None } }) val document_theories = info.document_theories.map({ case (thy, _) => known_theories(thy).name }) val dir_errors = { val ok = info.dirs.map(_.canonical_file).toSet val bad = (for { name <- proper_session_theories.iterator path = Path.explode(name.master_dir) if !ok(path.canonical_file) path1 = File.relative_path(info.dir.canonical, path).getOrElse(path) } yield (path1, name)).toList val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted val errs1 = for { (path1, name) <- bad } yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString) val errs2 = if (bad_dirs.isEmpty) Nil else List("Implicit use of session directories: " + commas(bad_dirs)) val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p val errs4 = (for { name <- proper_session_theories.iterator name1 <- resources.find_theory_node(name.theory) if name.node != name1.node } yield { "Incoherent theory file import:\n " + quote(name.node) + " vs. \n " + quote(name1.node) }).toList errs1 ::: errs2 ::: errs3 ::: errs4 } val sources_errors = for (p <- session_files if !p.is_file) yield "No such file: " + p val path_errors = try { Path.check_case_insensitive(session_files ::: imported_files); Nil } catch { case ERROR(msg) => List(msg) } val bibtex_errors = info.bibtex_entries.errors val base = Base( session_name = info.name, session_pos = info.pos, proper_session_theories = proper_session_theories, document_theories = document_theories, loaded_theories = dependencies.loaded_theories, used_theories = dependencies.theories_adjunct, theory_load_commands = theory_load_commands, known_theories = known_theories, known_loaded_files = known_loaded_files, overall_syntax = overall_syntax, imported_sources = check_sources(imported_files), session_sources = check_sources(session_files), session_graph_display = session_graph_display, errors = dependencies.errors ::: load_commands_errors ::: import_errors ::: document_errors ::: dir_errors ::: sources_errors ::: path_errors ::: bibtex_errors) session_bases + base.session_entry } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in session " + quote(info.name) + Position.here(info.pos)) } } new Deps(sessions_structure, session_bases) } } final class Deps private[Sessions]( val sessions_structure: Structure, val session_bases: Map[String, Base] ) { def background(session: String): Background = Background(base = apply(session), sessions_structure = sessions_structure, errors = errors) def is_empty: Boolean = session_bases.keysIterator.forall(_.isEmpty) def apply(name: String): Base = session_bases(name) def get(name: String): Option[Base] = session_bases.get(name) def sources_shasum(name: String): SHA1.Shasum = { val meta_info = sessions_structure(name).meta_info val sources = SHA1.shasum_sorted( for ((path, digest) <- apply(name).all_sources) yield digest -> File.symbolic_path(path)) meta_info ::: sources } def errors: List[String] = (for { (name, base) <- session_bases.iterator if base.errors.nonEmpty } yield cat_lines(base.errors) + "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.session_pos) ).toList def check_errors: Deps = errors match { case Nil => this case errs => error(cat_lines(errs)) } override def toString: String = "Sessions.Deps(" + sessions_structure + ")" } + /* notable groups */ + + sealed case class Group_Info( + name: String, + description: String, + bulky: Boolean = false, + afp: Boolean = false + ) { + override def toString: String = name + } + + lazy val notable_groups: List[Group_Info] = + List( + Group_Info("large", "full 64-bit memory model or word arithmetic required", + bulky = true, afp = true), + Group_Info("slow", "CPU time much higher than 60min (on mid-range hardware)", + bulky = true, afp = true), + Group_Info("very_slow", "elapsed time of many hours (on high-end hardware)", + afp = true), + Group_Info("AFP", "entry within AFP", afp = true), + Group_Info("doc", "Isabelle documentation"), + Group_Info("no_doc", "suppressed Isabelle documentation") + ) + + lazy val bulky_groups: Set[String] = + Set.from(notable_groups.flatMap(g => if (g.bulky) Some(g.name) else None)) + + lazy val afp_groups: Set[String] = + Set.from(notable_groups.flatMap(g => if (g.afp) Some(g.name) else None)) + + /* cumulative session info */ private val BUILD_PREFS_BG = "= 0 && { val s1 = s.substring(i) s1.startsWith(BUILD_PREFS_BG) && s1.endsWith(BUILD_PREFS_EN) } } def eq_sources(options: Options, shasum1: SHA1.Shasum, shasum2: SHA1.Shasum): Boolean = if (options.bool("build_thorough")) shasum1 == shasum2 else { def trim(shasum: SHA1.Shasum): SHA1.Shasum = shasum.filter(s => !is_build_prefs(s)) trim(shasum1) == trim(shasum2) } sealed case class Chapter_Info( name: String, pos: Position.T, groups: List[String], description: String, sessions: List[String] ) object Info { def make( chapter_defs: Chapter_Defs, options0: Options, options: Options, augment_options: String => List[Options.Spec], dir_selected: Boolean, dir: Path, chapter: String, entry: Session_Entry ): Info = { try { val name = entry.name if (illegal_session(name)) error("Illegal session name " + quote(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_path = dir + Path.explode(entry.path) val directories = entry.directories.map(dir => session_path + Path.explode(dir)) val session_options0 = options ++ entry.options val session_options = session_options0 ++ augment_options(name) val session_prefs = session_options.make_prefs(defaults = session_options0, filter = _.session_content) val build_prefs_digests = session_options.changed(defaults = options0, filter = _.session_content) .map(ch => SHA1.digest(ch.print_prefs) -> make_build_prefs(ch.name)) val theories = entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map({ case ((thy, pos), _) => val thy_name = Thy_Header.import_name(thy) if (illegal_theory(thy_name)) { error("Illegal theory name " + quote(thy_name) + Position.here(pos)) } else (thy, pos) })) }) val global_theories = for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global } yield { val thy_name = Path.explode(thy).file_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 conditions = theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted. map(x => (x, Isabelle_System.getenv(x) != "")) val document_files = entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) val export_files = entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) }) val meta_digest = SHA1.digest( (name, chapter, entry.parent, entry.directories, entry.options, entry.imports, entry.theories_no_position, conditions, entry.document_theories_no_position).toString) val meta_info = SHA1.shasum_meta_info(meta_digest) ::: SHA1.shasum_sorted(build_prefs_digests) val chapter_groups = chapter_defs(chapter).groups val groups = chapter_groups ::: entry.groups.filterNot(chapter_groups.contains) Info(name, chapter, dir_selected, entry.pos, groups, session_path, entry.parent, entry.description, directories, session_options, session_prefs, entry.imports, theories, global_theories, entry.document_theories, document_files, export_files, entry.export_classpath, meta_info) } catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session entry " + quote(entry.name) + Position.here(entry.pos)) } } } sealed case class Info( name: String, chapter: String, dir_selected: Boolean, pos: Position.T, groups: List[String], dir: Path, parent: Option[String], description: String, directories: List[Path], options: Options, session_prefs: String, imports: List[String], theories: List[(Options, List[(String, Position.T)])], global_theories: List[String], document_theories: List[(String, Position.T)], document_files: List[(Path, Path)], export_files: List[(Path, Int, List[String])], export_classpath: List[String], meta_info: SHA1.Shasum ) { def deps: List[String] = parent.toList ::: imports def deps_base(session_bases: String => Base): Base = { val parent_base = session_bases(parent.getOrElse("")) val imports_bases = imports.map(session_bases) parent_base.copy( known_theories = (for { base <- imports_bases.iterator (_, entry) <- base.known_theories.iterator } yield (entry.name.theory -> entry)).foldLeft(parent_base.known_theories)(_ + _), known_loaded_files = imports_bases.iterator.map(_.known_loaded_files). foldLeft(parent_base.known_loaded_files)(_ ++ _)) } def dirs: List[Path] = dir :: directories def main_group: Boolean = groups.contains("main") def doc_group: Boolean = groups.contains("doc") def timeout_ignored: Boolean = !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1) def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale")) def document_enabled: Boolean = options.string("document") match { case "" | "false" => false case "pdf" | "true" => true case doc => error("Bad document specification " + quote(doc)) } def document_variants: List[Document_Build.Document_Variant] = { val variants = space_explode(':', options.string("document_variants")). map(Document_Build.Document_Variant.parse) val dups = Library.duplicates(variants.map(_.name)) if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups)) variants } def document_echo: Boolean = options.bool("document_echo") def documents: List[Document_Build.Document_Variant] = { val variants = document_variants if (!document_enabled || document_files.isEmpty) Nil else variants } def document_output: Option[Path] = options.string("document_output") match { case "" => None case s => Some(dir + Path.explode(s)) } def browser_info: Boolean = options.bool("browser_info") lazy val bibtex_entries: Bibtex.Entries = (for { (document_dir, file) <- document_files.iterator if File.is_bib(file.file_name) } yield { val path = dir + document_dir + file Bibtex.Entries.parse(File.read(path), start = Token.Pos.file(File.standard_path(path))) }).foldRight(Bibtex.Entries.empty)(_ ::: _) def record_proofs: Boolean = options.int("record_proofs") >= 2 def is_afp: Boolean = chapter == AFP.chapter - def is_afp_bulky: Boolean = is_afp && groups.exists(AFP.groups_bulky.contains) + def is_afp_bulky: Boolean = is_afp && groups.exists(bulky_groups) } object Selection { val empty: Selection = Selection() val all: Selection = Selection(all_sessions = true) def session(session: String): Selection = Selection(sessions = List(session)) } sealed case class Selection( requirements: Boolean = false, all_sessions: Boolean = false, base_sessions: List[String] = Nil, exclude_session_groups: List[String] = Nil, exclude_sessions: List[String] = Nil, session_groups: List[String] = Nil, sessions: List[String] = Nil ) { def ++ (other: Selection): Selection = Selection( requirements = requirements || other.requirements, all_sessions = all_sessions || other.all_sessions, base_sessions = Library.merge(base_sessions, other.base_sessions), exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups), exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions), session_groups = Library.merge(session_groups, other.session_groups), sessions = Library.merge(sessions, other.sessions)) } object Structure { val empty: Structure = make(Options.empty) def make( options: Options, augment_options: String => List[Options.Spec] = _ => Nil, roots: List[Root_File] = Nil, infos: List[Info] = Nil ): Structure = { val chapter_defs: Chapter_Defs = roots.foldLeft(Chapter_Defs.empty) { case (defs1, root) => root.entries.foldLeft(defs1) { case (defs2, entry: Chapter_Def) => defs2 + entry case (defs2, _) => defs2 } } val options0 = Options.init0() val session_prefs = options.make_prefs(defaults = options0, filter = _.session_content) val root_infos = { var chapter = UNSORTED val root_infos = new mutable.ListBuffer[Info] for (root <- roots) { root.entries.foreach { case entry: Chapter_Entry => chapter = entry.name case entry: Session_Entry => root_infos += Info.make(chapter_defs, options0, options, augment_options, root.select, root.dir, chapter, entry) case _ => } chapter = UNSORTED } root_infos.toList } val info_graph = (root_infos ::: infos).foldLeft(Graph.string[Info]) { case (graph, info) => if (graph.defined(info.name)) { error("Duplicate session " + quote(info.name) + Position.here(info.pos) + Position.here(graph.get_node(info.name).pos)) } else graph.new_node(info.name, info) } def augment_graph( graph: Graph[String, Info], kind: String, edges: Info => Iterable[String] ) : Graph[String, Info] = { def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) = { if (!g.defined(parent)) { error("Bad " + kind + " session " + quote(parent) + " for " + quote(name) + Position.here(pos)) } try { g.add_edge_acyclic(parent, name) } catch { case exn: Graph.Cycles[_] => error(cat_lines(exn.cycles.map(cycle => "Cyclic session dependency of " + cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos)) } } graph.iterator.foldLeft(graph) { case (g, (name, (info, _))) => edges(info).foldLeft(g)(add_edge(info.pos, name, _, _)) } } val build_graph = augment_graph(info_graph, "parent", _.parent) val imports_graph = augment_graph(build_graph, "imports", _.imports) val session_positions: List[(String, Position.T)] = (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList val session_directories: Map[JFile, String] = (for { session <- imports_graph.topological_order.iterator info = info_graph.get_node(session) dir <- info.dirs.iterator } yield (info, dir)).foldLeft(Map.empty[JFile, String]) { case (dirs, (info, dir)) => val session = info.name val canonical_dir = dir.canonical_file dirs.get(canonical_dir) match { case Some(session1) => val info1 = info_graph.get_node(session1) error("Duplicate use of directory " + dir + "\n for session " + quote(session1) + Position.here(info1.pos) + "\n vs. session " + quote(session) + Position.here(info.pos)) case None => dirs + (canonical_dir -> session) } } val global_theories: Map[String, String] = (for { session <- imports_graph.topological_order.iterator info = info_graph.get_node(session) thy <- info.global_theories.iterator } yield (info, thy) ).foldLeft(Thy_Header.bootstrap_global_theories.toMap) { case (global, (info, thy)) => val qualifier = info.name global.get(thy) match { case Some(qualifier1) if qualifier != qualifier1 => error("Duplicate global theory " + quote(thy) + Position.here(info.pos)) case _ => global + (thy -> qualifier) } } new Structure(chapter_defs, session_prefs, session_positions, session_directories, global_theories, build_graph, imports_graph) } } final class Structure private[Sessions]( chapter_defs: Chapter_Defs, val session_prefs: String, val session_positions: List[(String, Position.T)], val session_directories: Map[JFile, String], val global_theories: Map[String, String], val build_graph: Graph[String, Info], val imports_graph: Graph[String, Info] ) { sessions_structure => def dest_session_directories: List[(String, String)] = for ((file, session) <- session_directories.toList) yield (File.standard_path(file), session) lazy val known_chapters: List[Chapter_Info] = { val chapter_sessions = Multi_Map.from( for ((_, (info, _)) <- build_graph.iterator) yield info.chapter -> info.name) val chapters1 = (for (entry <- chapter_defs.list.iterator) yield { val sessions = chapter_sessions.get_list(entry.name) Chapter_Info(entry.name, entry.pos, entry.groups, entry.description, sessions.sorted) }).toList val chapters2 = (for { (name, sessions) <- chapter_sessions.iterator_list if !chapters1.exists(_.name == name) } yield Chapter_Info(name, Position.none, Nil, "", sessions.sorted)).toList.sortBy(_.name) chapters1 ::: chapters2 } def relevant_chapters: List[Chapter_Info] = known_chapters.filter(_.sessions.nonEmpty) 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 defined(name: String): Boolean = imports_graph.defined(name) def apply(name: String): Info = imports_graph.get_node(name) def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None def theory_qualifier(name: String): String = global_theories.getOrElse(name, Long_Name.qualifier(name)) def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory) def check_sessions(names: List[String]): Unit = { val bad_sessions = SortedSet(names.filterNot(defined): _*).toList if (bad_sessions.nonEmpty) { error("Undefined session(s): " + commas_quote(bad_sessions)) } } def check_sessions(sel: Selection): Unit = check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions) private def selected(graph: Graph[String, Info], sel: Selection): List[String] = { check_sessions(sel) val select_group = sel.session_groups.toSet val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions) val selected0 = if (sel.all_sessions) graph.keys else { (for { (name, (info, _)) <- graph.iterator if info.dir_selected || select_session(name) || info.groups.exists(select_group) } yield name).toList } if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList else selected0 } def selection(sel: Selection): Structure = { check_sessions(sel) val excluded = { val exclude_group = sel.exclude_session_groups.toSet val exclude_group_sessions = (for { (name, (info, _)) <- imports_graph.iterator if info.groups.exists(exclude_group) } yield name).toList imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet } def restrict(graph: Graph[String, Info]): Graph[String, Info] = { val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded) graph.restrict(graph.all_preds(sessions).toSet) } new Structure(chapter_defs, session_prefs, session_positions, session_directories, global_theories, restrict(build_graph), restrict(imports_graph)) } def selection(session: String): Structure = selection(Selection.session(session)) def selection_deps( selection: Selection, progress: Progress = new Progress, loading_sessions: Boolean = false, inlined_files: Boolean = false ): Deps = { val deps = Sessions.deps(sessions_structure.selection(selection), progress = progress, inlined_files = inlined_files) if (loading_sessions) { val selection_size = deps.sessions_structure.build_graph.size if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...") } deps } def build_hierarchy(session: String): List[String] = if (build_graph.defined(session)) build_graph.all_preds(List(session)) else List(session) def build_selection(sel: Selection): List[String] = selected(build_graph, sel) def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss) def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss) def build_topological_order: List[String] = build_graph.topological_order def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel) def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss) def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss) def imports_topological_order: List[String] = imports_graph.topological_order override def toString: String = imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")") } /* parser */ private val CHAPTER_DEFINITION = "chapter_definition" private val CHAPTER = "chapter" private val SESSION = "session" private val DESCRIPTION = "description" private val DIRECTORIES = "directories" private val OPTIONS = "options" private val SESSIONS = "sessions" private val THEORIES = "theories" private val GLOBAL = "global" private val DOCUMENT_THEORIES = "document_theories" private val DOCUMENT_FILES = "document_files" private val EXPORT_FILES = "export_files" private val EXPORT_CLASSPATH = "export_classpath" val root_syntax: Outer_Syntax = Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + "in" + GLOBAL + (CHAPTER_DEFINITION, Keyword.THY_DECL) + (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) + (DESCRIPTION, Keyword.QUASI_COMMAND) + (DIRECTORIES, Keyword.QUASI_COMMAND) + (OPTIONS, Keyword.QUASI_COMMAND) + (SESSIONS, Keyword.QUASI_COMMAND) + (THEORIES, Keyword.QUASI_COMMAND) + (DOCUMENT_THEORIES, Keyword.QUASI_COMMAND) + (DOCUMENT_FILES, Keyword.QUASI_COMMAND) + (EXPORT_FILES, Keyword.QUASI_COMMAND) + (EXPORT_CLASSPATH, Keyword.QUASI_COMMAND) abstract class Entry object Chapter_Def { def empty(chapter: String): Chapter_Def = Chapter_Def(Position.none, chapter, Nil, "") } sealed case class Chapter_Def( pos: Position.T, name: String, groups: List[String], description: String ) extends Entry sealed case class Chapter_Entry(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], directories: List[String], theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])], document_theories: List[(String, Position.T)], document_files: List[(String, String)], export_files: List[(String, Int, List[String])], export_classpath: List[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) })) }) def document_theories_no_position: List[String] = document_theories.map(_._1) } object Chapter_Defs { val empty: Chapter_Defs = new Chapter_Defs(Nil) } class Chapter_Defs private(rev_list: List[Chapter_Def]) { def list: List[Chapter_Def] = rev_list.reverse override def toString: String = list.map(_.name).mkString("Chapter_Defs(", ", ", ")") def get(chapter: String): Option[Chapter_Def] = rev_list.find(_.name == chapter) def apply(chapter: String): Chapter_Def = get(chapter) getOrElse Chapter_Def.empty(chapter) def + (entry: Chapter_Def): Chapter_Defs = get(entry.name) match { case None => new Chapter_Defs(entry :: rev_list) case Some(old_entry) => error("Duplicate chapter definition " + quote(entry.name) + Position.here(old_entry.pos) + Position.here(entry.pos)) } } private object Parsers extends Options.Parsers { private val groups: Parser[List[String]] = ($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil) private val description: Parser[String] = ($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("") private val chapter_def: Parser[Chapter_Def] = command(CHAPTER_DEFINITION) ~! (position(chapter_name) ~ groups ~ description) ^^ { case _ ~ ((a, pos) ~ b ~ c) => Chapter_Def(pos, a, b, c) } private val chapter_entry: Parser[Chapter_Entry] = command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) } private val session_entry: Parser[Session_Entry] = { val options = $$$("[") ~> rep1sep(option_spec, $$$(",")) <~ $$$("]") val theory_entry = position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) } val theories = $$$(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_entry)) ^^ { case _ ~ (x ~ y) => (x, y) } val document_theories = $$$(DOCUMENT_THEORIES) ~! rep1(position(name)) ^^ { case _ ~ x => x } val document_files = $$$(DOCUMENT_FILES) ~! (in_path_parens("document") ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) } val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0) val export_files = $$$(EXPORT_FILES) ~! (in_path_parens("export") ~ prune ~ rep1(embedded)) ^^ { case _ ~ (x ~ y ~ z) => (x, y, z) } val export_classpath = $$$(EXPORT_CLASSPATH) ~! (rep1(embedded) | success(List("*:classpath/*.jar"))) ^^ { case _ ~ x => x } command(SESSION) ~! (position(session_name) ~ groups ~ in_path(".") ~ ($$$("=") ~! (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ description ~ (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~ (($$$(SESSIONS) ~! rep1(session_name) ^^ { case _ ~ x => x }) | success(Nil)) ~ (($$$(DIRECTORIES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~ rep(theories) ~ (opt(document_theories) ^^ (x => x.getOrElse(Nil))) ~ (rep(document_files) ^^ (x => x.flatten)) ~ rep(export_files) ~ opt(export_classpath)))) ^^ { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l ~ m))) => Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l, m.getOrElse(Nil)) } } def parse_root(path: Path): List[Entry] = { val toks = Token.explode(root_syntax.keywords, File.read(path)) val start = Token.Pos.file(path.implode) val parser: Parser[Entry] = chapter_def | chapter_entry | session_entry parse_all(rep(parser), Token.reader(toks, start)) match { case Success(result, _) => result case bad => error(bad.toString) } } } def parse_root(path: Path): List[Entry] = Parsers.parse_root(path) def parse_root_entries(path: Path): List[Session_Entry] = Parsers.parse_root(path).flatMap(Library.as_subclass(classOf[Session_Entry])) 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 */ def is_session_dir(dir: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_file(dir + ROOT) || ssh.is_file(dir + ROOTS) def check_session_dir(dir: Path): Path = if (is_session_dir(dir)) File.pwd() + dir.expand else { error("Bad session root directory: " + dir.expand.toString + "\n (missing \"ROOT\" or \"ROOTS\")") } def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = { val default_dirs = Components.directories().filter(is_session_dir(_)) for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) } yield (select, dir.canonical) } sealed case class Root_File(path: Path, select: Boolean) { val key: JFile = path.canonical_file def dir: Path = path.dir lazy val entries: List[Entry] = Parsers.parse_root(path) } def load_root_files( dirs: List[Path] = Nil, select_dirs: List[Path] = Nil ): List[Root_File] = { def load_dir(select: Boolean, dir: Path): List[Root_File] = load_root(select, dir) ::: load_roots(select, dir) def load_root(select: Boolean, dir: Path): List[Root_File] = { val root = dir + ROOT if (root.is_file) List(Root_File(root, select)) else Nil } def load_roots(select: Boolean, dir: Path): List[Root_File] = { val roots = dir + ROOTS if (roots.is_file) { for { entry <- parse_roots(roots) dir1 = try { check_session_dir(dir + Path.explode(entry)) } catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString) } res <- load_dir(select, dir1) } yield res } else Nil } val raw_roots: List[Root_File] = for { (select, dir) <- directories(dirs, select_dirs) root <- load_dir(select, check_session_dir(dir)) } yield root var next_root = 0 var seen_roots = Map.empty[JFile, (Root_File, Int)] for (root <- raw_roots) { seen_roots.get(root.key) match { case None => seen_roots += (root.key -> (root, next_root)) next_root += 1 case Some((root0, next0)) => val root1 = root0.copy(select = root0.select || root.select) seen_roots += (root0.key -> (root1, next0)) } } seen_roots.valuesIterator.toList.sortBy(_._2).map(_._1) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions", Scala_Project.here, { args => var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var requirements = false var exclude_session_groups: List[String] = Nil var all_sessions = false var build_graph = false var dirs: List[Path] = Nil var session_groups: List[String] = Nil var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle sessions [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -R refer to requirements of selected sessions -X NAME exclude sessions from group NAME and all descendants -a select all sessions -b follow session build dependencies (default: source imports) -d DIR include session directory -g NAME select session group NAME -x NAME exclude session NAME and all descendants Explore the structure of Isabelle sessions and print result names in topological order (on stdout). """, "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "R" -> (_ => requirements = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "b" -> (_ => build_graph = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) val options = Options.init() val selection = Selection(requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions, session_groups = session_groups, sessions = sessions) val sessions_structure = load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection) val order = if (build_graph) sessions_structure.build_topological_order else sessions_structure.imports_topological_order for (name <- order) Output.writeln(name, stdout = true) }) }