diff --git a/src/Pure/Admin/build_log.scala b/src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala +++ b/src/Pure/Admin/build_log.scala @@ -1,1176 +1,1179 @@ /* Title: Pure/Admin/build_log.scala Author: Makarius Management of build log files and database storage. */ package isabelle import java.io.{File => JFile} import java.time.format.{DateTimeFormatter, DateTimeParseException} import java.util.Locale import scala.collection.immutable.SortedMap import scala.collection.mutable import scala.util.matching.Regex object Build_Log { /** content **/ /* properties */ object Prop { val build_tags = SQL.Column.string("build_tags") // lines val build_args = SQL.Column.string("build_args") // lines val build_group_id = SQL.Column.string("build_group_id") val build_id = SQL.Column.string("build_id") val build_engine = SQL.Column.string("build_engine") val build_host = SQL.Column.string("build_host") val build_start = SQL.Column.date("build_start") val build_end = SQL.Column.date("build_end") val isabelle_version = SQL.Column.string("isabelle_version") val afp_version = SQL.Column.string("afp_version") val all_props: List[SQL.Column] = List(build_tags, build_args, build_group_id, build_id, build_engine, build_host, build_start, build_end, isabelle_version, afp_version) } /* settings */ object Settings { val ISABELLE_BUILD_OPTIONS = SQL.Column.string("ISABELLE_BUILD_OPTIONS") val ML_PLATFORM = SQL.Column.string("ML_PLATFORM") val ML_HOME = SQL.Column.string("ML_HOME") val ML_SYSTEM = SQL.Column.string("ML_SYSTEM") val ML_OPTIONS = SQL.Column.string("ML_OPTIONS") val ml_settings = List(ML_PLATFORM, ML_HOME, ML_SYSTEM, ML_OPTIONS) val all_settings = ISABELLE_BUILD_OPTIONS :: ml_settings type Entry = (String, String) type T = List[Entry] object Entry { def unapply(s: String): Option[Entry] = s.indexOf('=') match { case -1 => None case i => val a = s.substring(0, i) val b = Library.perhaps_unquote(s.substring(i + 1)) Some((a, b)) } def apply(a: String, b: String): String = a + "=" + quote(b) def getenv(a: String): String = apply(a, Isabelle_System.getenv(a)) } def show(): String = cat_lines( List(Entry.getenv("ISABELLE_TOOL_JAVA_OPTIONS"), Entry.getenv(ISABELLE_BUILD_OPTIONS.name), "") ::: ml_settings.map(c => Entry.getenv(c.name))) } /* file names */ def log_date(date: Date): String = String.format(Locale.ROOT, "%s.%05d", DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep), java.lang.Long.valueOf((date.time - date.midnight.time).ms / 1000)) def log_subdir(date: Date): Path = Path.explode("log") + Path.explode(date.rep.getYear.toString) def log_filename(engine: String, date: Date, more: List[String] = Nil): Path = Path.explode((engine :: log_date(date) :: more).mkString("", "_", ".log")) /** log file **/ def print_date(date: Date): String = Log_File.Date_Format(date) object Log_File { /* log file */ def plain_name(name: String): String = { List(".log", ".log.gz", ".log.xz", ".gz", ".xz").find(name.endsWith) match { case Some(s) => Library.try_unsuffix(s, name).get case None => name } } def apply(name: String, lines: List[String]): Log_File = new Log_File(plain_name(name), lines.map(Library.trim_line)) def apply(name: String, text: String): Log_File = new Log_File(plain_name(name), Library.trim_split_lines(text)) def apply(file: JFile): Log_File = { val name = file.getName val text = if (name.endsWith(".gz")) File.read_gzip(file) else if (name.endsWith(".xz")) File.read_xz(file) else File.read(file) apply(name, text) } def apply(path: Path): Log_File = apply(path.file) /* log file collections */ def is_log(file: JFile, prefixes: List[String] = List(Build_History.log_prefix, Identify.log_prefix, Identify.log_prefix2, Isatest.log_prefix, AFP_Test.log_prefix, Jenkins.log_prefix), suffixes: List[String] = List(".log", ".log.gz", ".log.xz")): Boolean = { val name = file.getName prefixes.exists(name.startsWith) && suffixes.exists(name.endsWith) && name != "isatest.log" && name != "afp-test.log" && name != "main.log" } /* date format */ val Date_Format = { val fmts = Date.Formatter.variants( List("EEE MMM d HH:mm:ss O yyyy", "EEE MMM d HH:mm:ss VV yyyy"), List(Locale.ENGLISH, Locale.GERMAN)) ::: List( DateTimeFormatter.RFC_1123_DATE_TIME, Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(Date.timezone_berlin)) def tune_timezone(s: String): String = s match { case "CET" | "MET" => "GMT+1" case "CEST" | "MEST" => "GMT+2" case "EST" => "Europe/Berlin" case _ => s } def tune_weekday(s: String): String = s match { case "Die" => "Di" case "Mit" => "Mi" case "Don" => "Do" case "Fre" => "Fr" case "Sam" => "Sa" case "Son" => "So" case _ => s } def tune(s: String): String = Word.implode( Word.explode(s) match { case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone) case a :: bs => tune_weekday(a) :: bs.map(tune_timezone) case Nil => Nil } ) Date.Format.make(fmts, tune) } } class Log_File private(val name: String, val lines: List[String]) { log_file => override def toString: String = name def text: String = cat_lines(lines) def err(msg: String): Nothing = error("Error in log file " + quote(name) + ": " + msg) /* date format */ object Strict_Date { def unapply(s: String): Some[Date] = try { Some(Log_File.Date_Format.parse(s)) } catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) } } /* inlined text */ def filter(Marker: Protocol_Message.Marker): List[String] = for (Marker(text) <- lines) yield text def find(Marker: Protocol_Message.Marker): Option[String] = lines.collectFirst({ case Marker(text) => text }) def find_match(regexes: List[Regex]): Option[String] = regexes match { case Nil => None case regex :: rest => lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1). map(res => res.get.head) orElse find_match(rest) } /* settings */ def get_setting(a: String): Option[Settings.Entry] = lines.find(_.startsWith(a + "=")) match { case Some(line) => Settings.Entry.unapply(line) case None => None } def get_all_settings: Settings.T = for { c <- Settings.all_settings; entry <- get_setting(c.name) } yield entry /* properties (YXML) */ - val xml_cache: XML.Cache = XML.make_cache() + val xml_cache: XML.Cache = XML.Cache.make() def parse_props(text: String): Properties.T = try { xml_cache.props(XML.Decode.properties(YXML.parse_body(text))) } catch { case _: XML.Error => log_file.err("malformed properties") } def filter_props(marker: Protocol_Message.Marker): List[Properties.T] = for (text <- filter(marker) if YXML.detect(text)) yield parse_props(text) def find_props(marker: Protocol_Message.Marker): Option[Properties.T] = for (text <- find(marker) if YXML.detect(text)) yield parse_props(text) /* parse various formats */ def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file) def parse_build_info(ml_statistics: Boolean = false): Build_Info = Build_Log.parse_build_info(log_file, ml_statistics) def parse_session_info( command_timings: Boolean = false, theory_timings: Boolean = false, ml_statistics: Boolean = false, task_statistics: Boolean = false): Session_Info = Build_Log.parse_session_info( log_file, command_timings, theory_timings, ml_statistics, task_statistics) } /** digested meta info: produced by Admin/build_history in log.xz file **/ object Meta_Info { val empty: Meta_Info = Meta_Info(Nil, Nil) } sealed case class Meta_Info(props: Properties.T, settings: Settings.T) { def is_empty: Boolean = props.isEmpty && settings.isEmpty def get(c: SQL.Column): Option[String] = Properties.get(props, c.name) orElse Properties.get(settings, c.name) def get_date(c: SQL.Column): Option[Date] = get(c).map(Log_File.Date_Format.parse) } object Identify { val log_prefix = "isabelle_identify_" val log_prefix2 = "plain_identify_" def engine(log_file: Log_File): String = if (log_file.name.startsWith(Jenkins.log_prefix)) "jenkins_identify" else if (log_file.name.startsWith(log_prefix2)) "plain_identify" else "identify" def content(date: Date, isabelle_version: Option[String], afp_version: Option[String]): String = terminate_lines( List("isabelle_identify: " + Build_Log.print_date(date), "") ::: isabelle_version.map("Isabelle version: " + _).toList ::: afp_version.map("AFP version: " + _).toList) val Start = new Regex("""^isabelle_identify: (.+)$""") val No_End = new Regex("""$.""") val Isabelle_Version = List(new Regex("""^Isabelle version: (\S+)$""")) val AFP_Version = List(new Regex("""^AFP version: (\S+)$""")) } object Isatest { val log_prefix = "isatest-makeall-" val engine = "isatest" val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""") val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""") val Isabelle_Version = List(new Regex("""^Isabelle version: (\S+)$""")) } object AFP_Test { val log_prefix = "afp-test-devel-" val engine = "afp-test" val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""") val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""") val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""") val Isabelle_Version = List(new Regex("""^Isabelle version: .* -- hg id (\S+)$""")) val AFP_Version = List(new Regex("""^AFP version: .* -- hg id (\S+)$""")) val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""") } object Jenkins { val log_prefix = "jenkins_" val engine = "jenkins" val Host = new Regex("""^Building remotely on (\S+) \((\S+)\).*$""") val Start = new Regex("""^(?:Started by an SCM change|Started from command line by admin|).*$""") val Start_Date = new Regex("""^Build started at (.+)$""") val No_End = new Regex("""$.""") val Isabelle_Version = List(new Regex("""^(?:Build for Isabelle id|Isabelle id) (\w+).*$"""), new Regex("""^ISABELLE_CI_REPO_ID="(\w+)".*$"""), new Regex("""^(\w{12}) tip.*$""")) val AFP_Version = List(new Regex("""^(?:Build for AFP id|AFP id) (\w+).*$"""), new Regex("""^ISABELLE_CI_AFP_ID="(\w+)".*$""")) val CONFIGURATION = "=== CONFIGURATION ===" val BUILD = "=== BUILD ===" } private def parse_meta_info(log_file: Log_File): Meta_Info = { def parse(engine: String, host: String, start: Date, End: Regex, Isabelle_Version: List[Regex], AFP_Version: List[Regex]): Meta_Info = { val build_id = { val prefix = proper_string(host) orElse proper_string(engine) getOrElse "build" prefix + ":" + start.time.ms } val build_engine = if (engine == "") Nil else List(Prop.build_engine.name -> engine) val build_host = if (host == "") Nil else List(Prop.build_host.name -> host) val start_date = List(Prop.build_start.name -> print_date(start)) val end_date = log_file.lines.last match { case End(log_file.Strict_Date(end_date)) => List(Prop.build_end.name -> print_date(end_date)) case _ => Nil } val isabelle_version = log_file.find_match(Isabelle_Version).map(Prop.isabelle_version.name -> _) val afp_version = log_file.find_match(AFP_Version).map(Prop.afp_version.name -> _) Meta_Info((Prop.build_id.name -> build_id) :: build_engine ::: build_host ::: start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, log_file.get_all_settings) } log_file.lines match { case line :: _ if Protocol.Meta_Info_Marker.test_yxml(line) => Meta_Info(log_file.find_props(Protocol.Meta_Info_Marker).get, log_file.get_all_settings) case Identify.Start(log_file.Strict_Date(start)) :: _ => parse(Identify.engine(log_file), "", start, Identify.No_End, Identify.Isabelle_Version, Identify.AFP_Version) case Isatest.Start(log_file.Strict_Date(start), host) :: _ => parse(Isatest.engine, host, start, Isatest.End, Isatest.Isabelle_Version, Nil) case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ => parse(AFP_Test.engine, host, start, AFP_Test.End, AFP_Test.Isabelle_Version, AFP_Test.AFP_Version) case AFP_Test.Start_Old(log_file.Strict_Date(start)) :: _ => parse(AFP_Test.engine, "", start, AFP_Test.End, AFP_Test.Isabelle_Version, AFP_Test.AFP_Version) case Jenkins.Start() :: _ => log_file.lines.dropWhile(_ != Jenkins.BUILD) match { case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ => val host = log_file.lines.takeWhile(_ != Jenkins.CONFIGURATION).collectFirst({ case Jenkins.Host(a, b) => a + "." + b }).getOrElse("") parse(Jenkins.engine, host, start.to(Date.timezone_berlin), Jenkins.No_End, Jenkins.Isabelle_Version, Jenkins.AFP_Version) case _ => Meta_Info.empty } case line :: _ if line.startsWith("\u0000") => Meta_Info.empty case List(Isatest.End(_)) => Meta_Info.empty case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty case Nil => Meta_Info.empty case _ => log_file.err("cannot detect log file format") } } /** build info: toplevel output of isabelle build or Admin/build_history **/ val SESSION_NAME = "session_name" object Session_Status extends Enumeration { val existing, finished, failed, cancelled = Value } sealed case class Session_Entry( chapter: String = "", groups: List[String] = Nil, threads: Option[Int] = None, timing: Timing = Timing.zero, ml_timing: Timing = Timing.zero, sources: Option[String] = None, heap_size: Option[Long] = None, status: Option[Session_Status.Value] = None, errors: List[String] = Nil, theory_timings: Map[String, Timing] = Map.empty, ml_statistics: List[Properties.T] = Nil) { def proper_groups: Option[String] = if (groups.isEmpty) None else Some(cat_lines(groups)) def finished: Boolean = status == Some(Session_Status.finished) def failed: Boolean = status == Some(Session_Status.failed) } object Build_Info { val sessions_dummy: Map[String, Session_Entry] = Map("" -> Session_Entry(theory_timings = Map("" -> Timing.zero))) } sealed case class Build_Info(sessions: Map[String, Session_Entry]) { def finished_sessions: List[String] = for ((a, b) <- sessions.toList if b.finished) yield a def failed_sessions: List[String] = for ((a, b) <- sessions.toList if b.failed) yield a } private def parse_build_info(log_file: Log_File, parse_ml_statistics: Boolean): Build_Info = { object Chapter_Name { def unapply(s: String): Some[(String, String)] = space_explode('/', s) match { case List(chapter, name) => Some((chapter, name)) case _ => Some(("", s)) } } val Session_No_Groups = new Regex("""^Session (\S+)$""") val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""") val Session_Finished1 = new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""") val Session_Finished2 = new Regex("""^Finished ([^\s/]+) \((\d+):(\d+):(\d+) elapsed time.*$""") val Session_Timing = new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""") val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""") val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""") val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""") object Theory_Timing { def unapply(line: String): Option[(String, (String, Timing))] = Protocol.Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props) match { case Some((SESSION_NAME, session) :: props) => for (theory <- Markup.Name.unapply(props)) yield (session, theory -> Markup.Timing_Properties.parse(props)) case _ => None } } var chapter = Map.empty[String, String] var groups = Map.empty[String, List[String]] var threads = Map.empty[String, Int] var timing = Map.empty[String, Timing] var ml_timing = Map.empty[String, Timing] var started = Set.empty[String] var sources = Map.empty[String, String] var heap_sizes = Map.empty[String, Long] var theory_timings = Map.empty[String, Map[String, Timing]] var ml_statistics = Map.empty[String, List[Properties.T]] var errors = Map.empty[String, List[String]] def all_sessions: Set[String] = chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++ started ++ sources.keySet ++ heap_sizes.keySet ++ theory_timings.keySet ++ ml_statistics.keySet for (line <- log_file.lines) { line match { case Session_No_Groups(Chapter_Name(chapt, name)) => chapter += (name -> chapt) groups += (name -> Nil) case Session_Groups(Chapter_Name(chapt, name), grps) => chapter += (name -> chapt) groups += (name -> Word.explode(grps)) case Session_Started(name) => started += name case Session_Finished1(name, Value.Int(e1), Value.Int(e2), Value.Int(e3), Value.Int(c1), Value.Int(c2), Value.Int(c3)) => val elapsed = Time.hms(e1, e2, e3) val cpu = Time.hms(c1, c2, c3) timing += (name -> Timing(elapsed, cpu, Time.zero)) case Session_Finished2(name, Value.Int(e1), Value.Int(e2), Value.Int(e3)) => val elapsed = Time.hms(e1, e2, e3) timing += (name -> Timing(elapsed, Time.zero, Time.zero)) case Session_Timing(name, Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) => val elapsed = Time.seconds(e) val cpu = Time.seconds(c) val gc = Time.seconds(g) ml_timing += (name -> Timing(elapsed, cpu, gc)) threads += (name -> t) case Sources(name, s) => sources += (name -> s) case Heap(name, Value.Long(size)) => heap_sizes += (name -> size) case _ if Protocol.Theory_Timing_Marker.test_yxml(line) => line match { case Theory_Timing(name, theory_timing) => theory_timings += (name -> (theory_timings.getOrElse(name, Map.empty) + theory_timing)) case _ => log_file.err("malformed theory_timing " + quote(line)) } case _ if parse_ml_statistics && Protocol.ML_Statistics_Marker.test_yxml(line) => Protocol.ML_Statistics_Marker.unapply(line).map(log_file.parse_props) match { case Some((SESSION_NAME, name) :: props) => ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil))) case _ => log_file.err("malformed ML_statistics " + quote(line)) } case _ if Protocol.Error_Message_Marker.test_yxml(line) => Protocol.Error_Message_Marker.unapply(line).map(log_file.parse_props) match { case Some(List((SESSION_NAME, name), (Markup.CONTENT, msg))) => errors += (name -> (msg :: errors.getOrElse(name, Nil))) case _ => log_file.err("malformed error message " + quote(line)) } case _ => } } val sessions = Map( (for (name <- all_sessions.toList) yield { val status = if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name)) Session_Status.finished else if (started(name)) Session_Status.failed else Session_Status.existing val entry = Session_Entry( chapter = chapter.getOrElse(name, ""), groups = groups.getOrElse(name, Nil), threads = threads.get(name), timing = timing.getOrElse(name, Timing.zero), ml_timing = ml_timing.getOrElse(name, Timing.zero), sources = sources.get(name), heap_size = heap_sizes.get(name), status = Some(status), errors = errors.getOrElse(name, Nil).reverse, theory_timings = theory_timings.getOrElse(name, Map.empty), ml_statistics = ml_statistics.getOrElse(name, Nil).reverse) (name -> entry) }):_*) Build_Info(sessions) } /** session info: produced by isabelle build as session database **/ sealed case class Session_Info( session_timing: Properties.T, command_timings: List[Properties.T], theory_timings: List[Properties.T], ml_statistics: List[Properties.T], task_statistics: List[Properties.T], errors: List[String]) { def error(s: String): Session_Info = copy(errors = errors ::: List(s)) } private def parse_session_info( log_file: Log_File, command_timings: Boolean, theory_timings: Boolean, ml_statistics: Boolean, task_statistics: Boolean): Session_Info = { Session_Info( session_timing = log_file.find_props(Protocol.Session_Timing_Marker) getOrElse Nil, command_timings = if (command_timings) log_file.filter_props(Protocol.Command_Timing_Marker) else Nil, theory_timings = if (theory_timings) log_file.filter_props(Protocol.Theory_Timing_Marker) else Nil, ml_statistics = if (ml_statistics) log_file.filter_props(Protocol.ML_Statistics_Marker) else Nil, task_statistics = if (task_statistics) log_file.filter_props(Protocol.Task_Statistics_Marker) else Nil, errors = log_file.filter(Protocol.Error_Message_Marker)) } - def compress_errors(errors: List[String], cache: XZ.Cache = XZ.cache()): Option[Bytes] = + def compress_errors(errors: List[String], cache: XZ.Cache = XZ.Cache()): Option[Bytes] = if (errors.isEmpty) None else { Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))). compress(cache = cache)) } - def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.cache()): List[String] = + def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.Cache()): List[String] = if (bytes.is_empty) Nil else { XML.Decode.list(YXML.string_of_body)(YXML.parse_body(bytes.uncompress(cache = cache).text)) } /** persistent store **/ /* SQL data model */ object Data { def build_log_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table = SQL.Table("isabelle_build_log_" + name, columns, body) /* main content */ val log_name = SQL.Column.string("log_name").make_primary_key val session_name = SQL.Column.string("session_name").make_primary_key val theory_name = SQL.Column.string("theory_name").make_primary_key val chapter = SQL.Column.string("chapter") val groups = SQL.Column.string("groups") val threads = SQL.Column.int("threads") val timing_elapsed = SQL.Column.long("timing_elapsed") val timing_cpu = SQL.Column.long("timing_cpu") val timing_gc = SQL.Column.long("timing_gc") val timing_factor = SQL.Column.double("timing_factor") val ml_timing_elapsed = SQL.Column.long("ml_timing_elapsed") val ml_timing_cpu = SQL.Column.long("ml_timing_cpu") val ml_timing_gc = SQL.Column.long("ml_timing_gc") val ml_timing_factor = SQL.Column.double("ml_timing_factor") val theory_timing_elapsed = SQL.Column.long("theory_timing_elapsed") val theory_timing_cpu = SQL.Column.long("theory_timing_cpu") val theory_timing_gc = SQL.Column.long("theory_timing_gc") val heap_size = SQL.Column.long("heap_size") val status = SQL.Column.string("status") val errors = SQL.Column.bytes("errors") val sources = SQL.Column.string("sources") val ml_statistics = SQL.Column.bytes("ml_statistics") val known = SQL.Column.bool("known") val meta_info_table = build_log_table("meta_info", log_name :: Prop.all_props ::: Settings.all_settings) val sessions_table = build_log_table("sessions", List(log_name, session_name, chapter, groups, threads, timing_elapsed, timing_cpu, timing_gc, timing_factor, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor, heap_size, status, errors, sources)) val theories_table = build_log_table("theories", List(log_name, session_name, theory_name, theory_timing_elapsed, theory_timing_cpu, theory_timing_gc)) val ml_statistics_table = build_log_table("ml_statistics", List(log_name, session_name, ml_statistics)) /* AFP versions */ val isabelle_afp_versions_table: SQL.Table = { val version1 = Prop.isabelle_version val version2 = Prop.afp_version build_log_table("isabelle_afp_versions", List(version1.make_primary_key, version2), SQL.select(List(version1, version2), distinct = true) + meta_info_table + " WHERE " + version1.defined + " AND " + version2.defined) } /* earliest pull date for repository version (PostgreSQL queries) */ def pull_date(afp: Boolean = false): SQL.Column = if (afp) SQL.Column.date("afp_pull_date") else SQL.Column.date("pull_date") def pull_date_table(afp: Boolean = false): SQL.Table = { val (name, versions) = if (afp) ("afp_pull_date", List(Prop.isabelle_version, Prop.afp_version)) else ("pull_date", List(Prop.isabelle_version)) build_log_table(name, versions.map(_.make_primary_key) ::: List(pull_date(afp)), "SELECT " + versions.mkString(", ") + ", min(" + Prop.build_start + ") AS " + pull_date(afp) + " FROM " + meta_info_table + " WHERE " + (versions ::: List(Prop.build_start)).map(_.defined).mkString(" AND ") + " GROUP BY " + versions.mkString(", ")) } /* recent entries */ def recent_time(days: Int): SQL.Source = "now() - INTERVAL '" + days.max(0) + " days'" def recent_pull_date_table( days: Int, rev: String = "", afp_rev: Option[String] = None): SQL.Table = { val afp = afp_rev.isDefined val rev2 = afp_rev.getOrElse("") val table = pull_date_table(afp) val version1 = Prop.isabelle_version val version2 = Prop.afp_version val eq1 = version1(table) + " = " + SQL.string(rev) val eq2 = version2(table) + " = " + SQL.string(rev2) SQL.Table("recent_pull_date", table.columns, table.select(table.columns, "WHERE " + pull_date(afp)(table) + " > " + recent_time(days) + (if (rev != "" && rev2 == "") " OR " + eq1 else if (rev == "" && rev2 != "") " OR " + eq2 else if (rev != "" && rev2 != "") " OR (" + eq1 + " AND " + eq2 + ")" else ""))) } def select_recent_log_names(days: Int): SQL.Source = { val table1 = meta_info_table val table2 = recent_pull_date_table(days) table1.select(List(log_name), distinct = true) + SQL.join_inner + table2.query_named + " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2) } def select_recent_versions(days: Int, rev: String = "", afp_rev: Option[String] = None, sql: SQL.Source = ""): SQL.Source = { val afp = afp_rev.isDefined val version = Prop.isabelle_version val table1 = recent_pull_date_table(days, rev = rev, afp_rev = afp_rev) val table2 = meta_info_table val aux_table = SQL.Table("aux", table2.columns, table2.select(sql = sql)) val columns = table1.columns.map(c => c(table1)) ::: List(known.copy(expr = log_name(aux_table).defined)) SQL.select(columns, distinct = true) + table1.query_named + SQL.join_outer + aux_table.query_named + " ON " + version(table1) + " = " + version(aux_table) + " ORDER BY " + pull_date(afp)(table1) + " DESC" } /* universal view on main data */ val universal_table: SQL.Table = { val afp_pull_date = pull_date(afp = true) val version1 = Prop.isabelle_version val version2 = Prop.afp_version val table1 = meta_info_table val table2 = pull_date_table(afp = true) val table3 = pull_date_table() val a_columns = log_name :: afp_pull_date :: table1.columns.tail val a_table = SQL.Table("a", a_columns, SQL.select(List(log_name, afp_pull_date) ::: table1.columns.tail.map(_.apply(table1))) + table1 + SQL.join_outer + table2 + " ON " + version1(table1) + " = " + version1(table2) + " AND " + version2(table1) + " = " + version2(table2)) val b_columns = log_name :: pull_date() :: a_columns.tail val b_table = SQL.Table("b", b_columns, SQL.select( List(log_name(a_table), pull_date()(table3)) ::: a_columns.tail.map(_.apply(a_table))) + a_table.query_named + SQL.join_outer + table3 + " ON " + version1(a_table) + " = " + version1(table3)) val c_columns = b_columns ::: sessions_table.columns.tail val c_table = SQL.Table("c", c_columns, SQL.select(log_name(b_table) :: c_columns.tail) + b_table.query_named + SQL.join_inner + sessions_table + " ON " + log_name(b_table) + " = " + log_name(sessions_table)) SQL.Table("isabelle_build_log", c_columns ::: List(ml_statistics), { SQL.select(c_columns.map(_.apply(c_table)) ::: List(ml_statistics)) + c_table.query_named + SQL.join_outer + ml_statistics_table + " ON " + log_name(c_table) + " = " + log_name(ml_statistics_table) + " AND " + session_name(c_table) + " = " + session_name(ml_statistics_table) }) } } /* database access */ - def store(options: Options): Store = new Store(options) + def store(options: Options, + xml_cache: XML.Cache = XML.Cache.make(), + xz_cache: XZ.Cache = XZ.Cache.make()): Store = + new Store(options, xml_cache, xz_cache) - class Store private[Build_Log](options: Options) + class Store private[Build_Log]( + options: Options, + val xml_cache: XML.Cache, + val xz_cache: XZ.Cache) { - val xml_cache: XML.Cache = XML.make_cache() - val xz_cache: XZ.Cache = XZ.make_cache() - def open_database( user: String = options.string("build_log_database_user"), password: String = options.string("build_log_database_password"), database: String = options.string("build_log_database_name"), host: String = options.string("build_log_database_host"), port: Int = options.int("build_log_database_port"), ssh_host: String = options.string("build_log_ssh_host"), ssh_user: String = options.string("build_log_ssh_user"), ssh_port: Int = options.int("build_log_ssh_port")): PostgreSQL.Database = { PostgreSQL.open_database( user = user, password = password, database = database, host = host, port = port, ssh = if (ssh_host == "") None else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = port)), ssh_close = true) } def update_database(db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false) { val log_files = dirs.flatMap(dir => File.find_files(dir.file, pred = Log_File.is_log(_), follow_links = true)) write_info(db, log_files, ml_statistics = ml_statistics) db.create_view(Data.pull_date_table()) db.create_view(Data.pull_date_table(afp = true)) db.create_view(Data.universal_table) } def snapshot_database(db: PostgreSQL.Database, sqlite_database: Path, days: Int = 100, ml_statistics: Boolean = false) { Isabelle_System.make_directory(sqlite_database.dir) sqlite_database.file.delete using(SQLite.open_database(sqlite_database))(db2 => { db.transaction { db2.transaction { // main content db2.create_table(Data.meta_info_table) db2.create_table(Data.sessions_table) db2.create_table(Data.theories_table) db2.create_table(Data.ml_statistics_table) val recent_log_names = db.using_statement(Data.select_recent_log_names(days))(stmt => stmt.execute_query().iterator(_.string(Data.log_name)).toList) for (log_name <- recent_log_names) { read_meta_info(db, log_name).foreach(meta_info => update_meta_info(db2, log_name, meta_info)) update_sessions(db2, log_name, read_build_info(db, log_name)) if (ml_statistics) { update_ml_statistics(db2, log_name, read_build_info(db, log_name, ml_statistics = true)) } } // pull_date for (afp <- List(false, true)) { val afp_rev = if (afp) Some("") else None val table = Data.pull_date_table(afp) db2.create_table(table) db2.using_statement(table.insert())(stmt2 => { db.using_statement( Data.recent_pull_date_table(days, afp_rev = afp_rev).query)(stmt => { val res = stmt.execute_query() while (res.next()) { for ((c, i) <- table.columns.zipWithIndex) { stmt2.string(i + 1) = res.get_string(c) } stmt2.execute() } }) }) } // full view db2.create_view(Data.universal_table) } } db2.rebuild }) } def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] = db.using_statement(table.select(List(column), distinct = true))(stmt => stmt.execute_query().iterator(_.string(column)).toSet) def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info) { val table = Data.meta_info_table db.using_statement(db.insert_permissive(table))(stmt => { stmt.string(1) = log_name for ((c, i) <- table.columns.tail.zipWithIndex) { if (c.T == SQL.Type.Date) stmt.date(i + 2) = meta_info.get_date(c) else stmt.string(i + 2) = meta_info.get(c) } stmt.execute() }) } def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info) { val table = Data.sessions_table db.using_statement(db.insert_permissive(table))(stmt => { val sessions = if (build_info.sessions.isEmpty) Build_Info.sessions_dummy else build_info.sessions for ((session_name, session) <- sessions) { stmt.string(1) = log_name stmt.string(2) = session_name stmt.string(3) = proper_string(session.chapter) stmt.string(4) = session.proper_groups stmt.int(5) = session.threads stmt.long(6) = session.timing.elapsed.proper_ms stmt.long(7) = session.timing.cpu.proper_ms stmt.long(8) = session.timing.gc.proper_ms stmt.double(9) = session.timing.factor stmt.long(10) = session.ml_timing.elapsed.proper_ms stmt.long(11) = session.ml_timing.cpu.proper_ms stmt.long(12) = session.ml_timing.gc.proper_ms stmt.double(13) = session.ml_timing.factor stmt.long(14) = session.heap_size stmt.string(15) = session.status.map(_.toString) stmt.bytes(16) = compress_errors(session.errors, cache = xz_cache) stmt.string(17) = session.sources stmt.execute() } }) } def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info) { val table = Data.theories_table db.using_statement(db.insert_permissive(table))(stmt => { val sessions = if (build_info.sessions.forall({ case (_, session) => session.theory_timings.isEmpty })) Build_Info.sessions_dummy else build_info.sessions for { (session_name, session) <- sessions (theory_name, timing) <- session.theory_timings } { stmt.string(1) = log_name stmt.string(2) = session_name stmt.string(3) = theory_name stmt.long(4) = timing.elapsed.ms stmt.long(5) = timing.cpu.ms stmt.long(6) = timing.gc.ms stmt.execute() } }) } def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info) { val table = Data.ml_statistics_table db.using_statement(db.insert_permissive(table))(stmt => { val ml_stats: List[(String, Option[Bytes])] = Par_List.map[(String, Session_Entry), (String, Option[Bytes])]( { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = xz_cache).proper) }, build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList) val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None) for ((session_name, ml_statistics) <- entries) { stmt.string(1) = log_name stmt.string(2) = session_name stmt.bytes(3) = ml_statistics stmt.execute() } }) } def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false) { abstract class Table_Status(table: SQL.Table) { db.create_table(table) private var known: Set[String] = domain(db, table, Data.log_name) def required(file: JFile): Boolean = !known(Log_File.plain_name(file.getName)) def update_db(db: SQL.Database, log_file: Log_File): Unit def update(log_file: Log_File) { if (!known(log_file.name)) { update_db(db, log_file) known += log_file.name } } } val status = List( new Table_Status(Data.meta_info_table) { override def update_db(db: SQL.Database, log_file: Log_File): Unit = update_meta_info(db, log_file.name, log_file.parse_meta_info()) }, new Table_Status(Data.sessions_table) { override def update_db(db: SQL.Database, log_file: Log_File): Unit = update_sessions(db, log_file.name, log_file.parse_build_info()) }, new Table_Status(Data.theories_table) { override def update_db(db: SQL.Database, log_file: Log_File): Unit = update_theories(db, log_file.name, log_file.parse_build_info()) }, new Table_Status(Data.ml_statistics_table) { override def update_db(db: SQL.Database, log_file: Log_File): Unit = if (ml_statistics) { update_ml_statistics(db, log_file.name, log_file.parse_build_info(ml_statistics = true)) } }) for (file_group <- files.filter(file => status.exists(_.required(file))). grouped(options.int("build_log_transaction_size") max 1)) { val log_files = Par_List.map[JFile, Log_File](Log_File.apply, file_group) db.transaction { log_files.foreach(log_file => status.foreach(_.update(log_file))) } } } def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] = { val table = Data.meta_info_table val columns = table.columns.tail db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt => { val res = stmt.execute_query() if (!res.next) None else { val results = columns.map(c => c.name -> (if (c.T == SQL.Type.Date) res.get_date(c).map(Log_File.Date_Format(_)) else res.get_string(c))) val n = Prop.all_props.length val props = for ((x, Some(y)) <- results.take(n)) yield (x, y) val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y) Some(Meta_Info(props, settings)) } }) } def read_build_info( db: SQL.Database, log_name: String, session_names: List[String] = Nil, ml_statistics: Boolean = false): Build_Info = { val table1 = Data.sessions_table val table2 = Data.ml_statistics_table val where_log_name = Data.log_name(table1).where_equal(log_name) + " AND " + Data.session_name(table1) + " <> ''" val where = if (session_names.isEmpty) where_log_name else where_log_name + " AND " + SQL.member(Data.session_name(table1).ident, session_names) val columns1 = table1.columns.tail.map(_.apply(table1)) val (columns, from) = if (ml_statistics) { val columns = columns1 ::: List(Data.ml_statistics(table2)) val join = table1 + SQL.join_outer + table2 + " ON " + Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " + Data.session_name(table1) + " = " + Data.session_name(table2) (columns, SQL.enclose(join)) } else (columns1, table1.ident) val sessions = db.using_statement(SQL.select(columns) + from + " " + where)(stmt => { stmt.execute_query().iterator(res => { val session_name = res.string(Data.session_name) val session_entry = Session_Entry( chapter = res.string(Data.chapter), groups = split_lines(res.string(Data.groups)), threads = res.get_int(Data.threads), timing = res.timing(Data.timing_elapsed, Data.timing_cpu, Data.timing_gc), ml_timing = res.timing(Data.ml_timing_elapsed, Data.ml_timing_cpu, Data.ml_timing_gc), sources = res.get_string(Data.sources), heap_size = res.get_long(Data.heap_size), status = res.get_string(Data.status).map(Session_Status.withName), errors = uncompress_errors(res.bytes(Data.errors), cache = xz_cache), ml_statistics = if (ml_statistics) { Properties.uncompress( - res.bytes(Data.ml_statistics), cache = xz_cache, Some(xml_cache)) + res.bytes(Data.ml_statistics), cache = xz_cache, xml_cache = xml_cache) } else Nil) session_name -> session_entry }).toMap }) Build_Info(sessions) } } } diff --git a/src/Pure/General/bytes.scala b/src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala +++ b/src/Pure/General/bytes.scala @@ -1,214 +1,214 @@ /* Title: Pure/General/bytes.scala Author: Makarius Immutable byte vectors versus UTF8 strings. */ package isabelle import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream, OutputStream, InputStream, FileInputStream, FileOutputStream} import java.net.URL import java.util.Base64 import org.tukaani.xz.{XZInputStream, XZOutputStream} object Bytes { val empty: Bytes = new Bytes(Array[Byte](), 0, 0) def apply(s: CharSequence): Bytes = { val str = s.toString if (str.isEmpty) empty else { val b = UTF8.bytes(str) new Bytes(b, 0, b.length) } } def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length) def apply(a: Array[Byte], offset: Int, length: Int): Bytes = if (length == 0) empty else { val b = new Array[Byte](length) System.arraycopy(a, offset, b, 0, length) new Bytes(b, 0, b.length) } val newline: Bytes = apply("\n") def base64(s: String): Bytes = { val a = Base64.getDecoder.decode(s) new Bytes(a, 0, a.length) } /* read */ def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes = if (limit == 0) empty else { val out = new ByteArrayOutputStream(if (limit == Integer.MAX_VALUE) hint else limit) val buf = new Array[Byte](8192) var m = 0 do { m = stream.read(buf, 0, buf.size min (limit - out.size)) if (m != -1) out.write(buf, 0, m) } while (m != -1 && limit > out.size) new Bytes(out.toByteArray, 0, out.size) } def read(file: JFile): Bytes = { val length = file.length val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt using(new FileInputStream(file))(read_stream(_, limit = limit)) } def read(path: Path): Bytes = read(path.file) def read(url: URL): Bytes = using(url.openStream)(read_stream(_)) /* write */ def write(file: JFile, bytes: Bytes): Unit = using(new FileOutputStream(file))(bytes.write_stream(_)) def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes) } final class Bytes private( protected val bytes: Array[Byte], protected val offset: Int, val length: Int) extends CharSequence { /* equality */ override def equals(that: Any): Boolean = { that match { case other: Bytes => if (this eq other) true else if (length != other.length) false else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i)) case _ => false } } private lazy val hash: Int = { var h = 0 for (i <- offset until offset + length) { val b = bytes(i).asInstanceOf[Int] & 0xFF h = 31 * h + b } h } override def hashCode(): Int = hash /* content */ lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes) def is_empty: Boolean = length == 0 def iterator: Iterator[Byte] = for (i <- (offset until (offset + length)).iterator) yield bytes(i) def array: Array[Byte] = { val a = new Array[Byte](length) System.arraycopy(bytes, offset, a, 0, length) a } def text: String = UTF8.decode_chars(s => s, bytes, offset, offset + length).toString def base64: String = { val b = if (offset == 0 && length == bytes.length) bytes else Bytes(bytes, offset, length).bytes Base64.getEncoder.encodeToString(b) } def maybe_base64: (Boolean, String) = { val s = text if (this == Bytes(s)) (false, s) else (true, base64) } override def toString: String = "Bytes(" + length + ")" def proper: Option[Bytes] = if (is_empty) None else Some(this) def proper_text: Option[String] = if (is_empty) None else Some(text) def +(other: Bytes): Bytes = if (other.is_empty) this else if (is_empty) other else { val new_bytes = new Array[Byte](length + other.length) System.arraycopy(bytes, offset, new_bytes, 0, length) System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length) new Bytes(new_bytes, 0, new_bytes.length) } /* CharSequence operations */ def charAt(i: Int): Char = if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char] else throw new IndexOutOfBoundsException def subSequence(i: Int, j: Int): Bytes = { if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i) else throw new IndexOutOfBoundsException } def trim_line: Bytes = if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10) subSequence(0, length - 2) else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10)) subSequence(0, length - 1) else this /* streams */ def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length) def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length) /* XZ data compression */ - def uncompress(cache: XZ.Cache = XZ.cache()): Bytes = + def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes = using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length)) - def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()): Bytes = + def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes = { val result = new ByteArrayOutputStream(length) using(new XZOutputStream(result, options, cache))(write_stream(_)) new Bytes(result.toByteArray, 0, result.size) } - def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()) + def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()) : (Boolean, Bytes) = { val compressed = compress(options = options, cache = cache) if (compressed.length < length) (true, compressed) else (false, this) } } diff --git a/src/Pure/General/cache.scala b/src/Pure/General/cache.scala --- a/src/Pure/General/cache.scala +++ b/src/Pure/General/cache.scala @@ -1,55 +1,75 @@ /* Title: Pure/General/cache.scala Author: Makarius Cache for partial sharing (weak table). */ package isabelle -import java.util.{Collections, WeakHashMap} +import java.util.{Collections, WeakHashMap, Map => JMap} import java.lang.ref.WeakReference -class Cache(initial_size: Int = 131071, max_string: Int = 100) +object Cache { - private val table = - Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size)) + val default_max_string = 100 + val default_initial_size = 131071 - def size: Int = table.size + def make(max_string: Int = default_max_string, initial_size: Int = default_initial_size): Cache = + new Cache(max_string, initial_size) - override def toString: String = "Cache(" + size + ")" + val none: Cache = make(max_string = 0) +} + +class Cache(max_string: Int, initial_size: Int) +{ + val no_cache: Boolean = max_string == 0 + + private val table: JMap[Any, WeakReference[Any]] = + if (max_string == 0) null + else Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size)) + + override def toString: String = + if (no_cache) "Cache.none" else "Cache(size = " + table.size + ")" protected def lookup[A](x: A): Option[A] = { - val ref = table.get(x) - if (ref == null) None - else Option(ref.asInstanceOf[WeakReference[A]].get) + if (table == null) None + else { + val ref = table.get(x) + if (ref == null) None + else Option(ref.asInstanceOf[WeakReference[A]].get) + } } protected def store[A](x: A): A = { - table.put(x, new WeakReference[Any](x)) - x + if (table == null) x + else { + table.put(x, new WeakReference[Any](x)) + x + } } protected def cache_string(x: String): String = { if (x == "") "" else if (x == "true") "true" else if (x == "false") "false" else if (x == "0.0") "0.0" else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x)) else { lookup(x) match { case Some(y) => y case None => val z = Library.isolate_substring(x) if (z.length > max_string) z else store(z) } } } // main methods - def string(x: String): String = synchronized { cache_string(x) } + def string(x: String): String = + if (no_cache) x else synchronized { cache_string(x) } } diff --git a/src/Pure/General/properties.scala b/src/Pure/General/properties.scala --- a/src/Pure/General/properties.scala +++ b/src/Pure/General/properties.scala @@ -1,138 +1,129 @@ /* Title: Pure/General/properties.scala Author: Makarius Property lists. */ package isabelle object Properties { /* entries */ type Entry = (java.lang.String, java.lang.String) type T = List[Entry] def defined(props: T, name: java.lang.String): java.lang.Boolean = props.exists({ case (x, _) => x == name }) def get(props: T, name: java.lang.String): Option[java.lang.String] = props.collectFirst({ case (x, y) if x == name => y }) def put(props: T, entry: Entry): T = { val (x, y) = entry def update(ps: T): T = ps match { case (p @ (x1, _)) :: rest => if (x1 == x) (x1, y) :: rest else p :: update(rest) case Nil => Nil } if (defined(props, x)) update(props) else entry :: props } /* external storage */ def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps))) - def decode(bs: Bytes, xml_cache: Option[XML.Cache] = None): T = - { - val ps = XML.Decode.properties(YXML.parse_body(bs.text)) - xml_cache match { - case None => ps - case Some(cache) => cache.props(ps) - } - } + def decode(bs: Bytes, xml_cache: XML.Cache = XML.Cache.none): T = + xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text))) def compress(ps: List[T], options: XZ.Options = XZ.options(), - cache: XZ.Cache = XZ.cache()): Bytes = + cache: XZ.Cache = XZ.Cache()): Bytes = { if (ps.isEmpty) Bytes.empty else { Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))). compress(options = options, cache = cache) } } def uncompress(bs: Bytes, - cache: XZ.Cache = XZ.cache(), - xml_cache: Option[XML.Cache] = None): List[T] = + cache: XZ.Cache = XZ.Cache(), + xml_cache: XML.Cache = XML.Cache.none): List[T] = { if (bs.is_empty) Nil else { val ps = XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text)) - xml_cache match { - case None => ps - case Some(cache) => ps.map(cache.props) - } + if (xml_cache.no_cache) ps else ps.map(xml_cache.props) } } /* multi-line entries */ def encode_lines(props: T): T = props.map({ case (a, b) => (a, Library.encode_lines(b)) }) def decode_lines(props: T): T = props.map({ case (a, b) => (a, Library.decode_lines(b)) }) def lines_nonempty(x: java.lang.String, ys: List[java.lang.String]): Properties.T = if (ys.isEmpty) Nil else List((x, cat_lines(ys))) /* entry types */ class String(val name: java.lang.String) { def apply(value: java.lang.String): T = List((name, value)) def unapply(props: T): Option[java.lang.String] = props.find(_._1 == name).map(_._2) def get(props: T): java.lang.String = unapply(props).getOrElse("") } class Boolean(val name: java.lang.String) { def apply(value: scala.Boolean): T = List((name, Value.Boolean(value))) def unapply(props: T): Option[scala.Boolean] = props.find(_._1 == name) match { case None => None case Some((_, value)) => Value.Boolean.unapply(value) } def get(props: T): scala.Boolean = unapply(props).getOrElse(false) } class Int(val name: java.lang.String) { def apply(value: scala.Int): T = List((name, Value.Int(value))) def unapply(props: T): Option[scala.Int] = props.find(_._1 == name) match { case None => None case Some((_, value)) => Value.Int.unapply(value) } def get(props: T): scala.Int = unapply(props).getOrElse(0) } class Long(val name: java.lang.String) { def apply(value: scala.Long): T = List((name, Value.Long(value))) def unapply(props: T): Option[scala.Long] = props.find(_._1 == name) match { case None => None case Some((_, value)) => Value.Long.unapply(value) } def get(props: T): scala.Long = unapply(props).getOrElse(0) } class Double(val name: java.lang.String) { def apply(value: scala.Double): T = List((name, Value.Double(value))) def unapply(props: T): Option[scala.Double] = props.find(_._1 == name) match { case None => None case Some((_, value)) => Value.Double.unapply(value) } def get(props: T): scala.Double = unapply(props).getOrElse(0.0) } } diff --git a/src/Pure/General/xz.scala b/src/Pure/General/xz.scala --- a/src/Pure/General/xz.scala +++ b/src/Pure/General/xz.scala @@ -1,34 +1,37 @@ /* Title: Pure/General/xz.scala Author: Makarius Support for XZ data compression. */ package isabelle import org.tukaani.xz.{LZMA2Options, ArrayCache, BasicArrayCache} object XZ { /* options */ type Options = LZMA2Options def options(preset: Int = 3): Options = { val opts = new LZMA2Options opts.setPreset(preset) opts } /* cache */ type Cache = ArrayCache - def no_cache(): ArrayCache = ArrayCache.getDummyCache() - def cache(): ArrayCache = ArrayCache.getDefaultCache() - def make_cache(): ArrayCache = new BasicArrayCache + object Cache + { + def none: ArrayCache = ArrayCache.getDummyCache() + def apply(): ArrayCache = ArrayCache.getDefaultCache() + def make(): ArrayCache = new BasicArrayCache + } } diff --git a/src/Pure/PIDE/session.scala b/src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala +++ b/src/Pure/PIDE/session.scala @@ -1,777 +1,777 @@ /* Title: Pure/PIDE/session.scala Author: Makarius Options: :folding=explicit: PIDE editor session, potentially with running prover process. */ package isabelle import scala.collection.immutable.Queue import scala.collection.mutable import scala.annotation.tailrec object Session { /* outlets */ object Consumer { def apply[A](name: String)(consume: A => Unit): Consumer[A] = new Consumer[A](name, consume) } final class Consumer[-A] private(val name: String, val consume: A => Unit) class Outlet[A](dispatcher: Consumer_Thread[() => Unit]) { private val consumers = Synchronized[List[Consumer[A]]](Nil) def += (c: Consumer[A]) { consumers.change(Library.update(c)) } def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) } def post(a: A) { for (c <- consumers.value.iterator) { dispatcher.send(() => try { c.consume(a) } catch { case exn: Throwable => Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn)) }) } } } /* change */ sealed case class Change( previous: Document.Version, syntax_changed: List[Document.Node.Name], deps_changed: Boolean, doc_edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name], version: Document.Version) case object Change_Flush /* events */ //{{{ case class Command_Timing(props: Properties.T) case class Theory_Timing(props: Properties.T) case class Runtime_Statistics(props: Properties.T) case class Task_Statistics(props: Properties.T) case class Global_Options(options: Options) case object Caret_Focus case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])]) case class Commands_Changed( assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) sealed abstract class Phase { def print: String = this match { case Terminated(result) => if (result.ok) "finished" else "failed" case _ => Word.lowercase(this.toString) } } case object Inactive extends Phase // stable case object Startup extends Phase // transient case object Ready extends Phase // metastable case object Shutdown extends Phase // transient case class Terminated(result: Process_Result) extends Phase // stable //}}} /* syslog */ private[Session] class Syslog(limit: Int) { private var queue = Queue.empty[XML.Elem] private var length = 0 def += (msg: XML.Elem): Unit = synchronized { queue = queue.enqueue(msg) length += 1 if (length > limit) queue = queue.dequeue._2 } def content: String = synchronized { cat_lines(queue.iterator.map(XML.content)) + (if (length > limit) "\n(A total of " + length + " messages...)" else "") } } /* protocol handlers */ type Protocol_Function = Prover.Protocol_Output => Boolean abstract class Protocol_Handler extends Isabelle_System.Service { def init(session: Session): Unit = {} def exit(): Unit = {} def functions: List[(String, Protocol_Function)] = Nil def prover_options(options: Options): Options = options } } class Session(_session_options: => Options, val resources: Resources) extends Document.Session { session => - val xml_cache: XML.Cache = XML.make_cache() - val xz_cache: XZ.Cache = XZ.make_cache() + val xml_cache: XML.Cache = XML.Cache.make() + val xz_cache: XZ.Cache = XZ.Cache.make() def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none /* global flags */ @volatile var timing: Boolean = false @volatile var verbose: Boolean = false /* dynamic session options */ def session_options: Options = _session_options def output_delay: Time = session_options.seconds("editor_output_delay") def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay") def prune_delay: Time = session_options.seconds("editor_prune_delay") def prune_size: Int = session_options.int("editor_prune_size") def syslog_limit: Int = session_options.int("editor_syslog_limit") def reparse_limit: Int = session_options.int("editor_reparse_limit") /* dispatcher */ private val dispatcher = Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true } def assert_dispatcher[A](body: => A): A = { assert(dispatcher.check_thread) body } def require_dispatcher[A](body: => A): A = { require(dispatcher.check_thread) body } def send_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread) body else dispatcher.send(() => body) } def send_wait_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread) body else dispatcher.send_wait(() => body) } /* outlets */ val finished_theories = new Session.Outlet[Document.Snapshot](dispatcher) val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher) val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher) val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher) val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher) val global_options = new Session.Outlet[Session.Global_Options](dispatcher) val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher) val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher) val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher) val phase_changed = new Session.Outlet[Session.Phase](dispatcher) val syslog_messages = new Session.Outlet[Prover.Output](dispatcher) val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher) val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher) val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher) val all_messages = new Session.Outlet[Prover.Message](dispatcher) // potential bottle-neck! /** main protocol manager **/ /* internal messages */ private case class Start(start_prover: Prover.Receiver => Prover) private case object Stop private case class Get_State(promise: Promise[Document.State]) private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Protocol_Command(name: String, args: List[String]) private case class Update_Options(options: Options) private case object Consolidate_Execution private case object Prune_History /* phase */ private def post_phase(new_phase: Session.Phase): Session.Phase = { phase_changed.post(new_phase) new_phase } private val _phase = Synchronized[Session.Phase](Session.Inactive) private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase)) def phase: Session.Phase = _phase.value def is_ready: Boolean = phase == Session.Ready /* syslog */ private val syslog = new Session.Syslog(syslog_limit) def syslog_content(): String = syslog.content /* pipelined change parsing */ private case class Text_Edits( previous: Future[Document.Version], doc_blobs: Document.Blobs, text_edits: List[Document.Edit_Text], consolidate: List[Document.Node.Name], version_result: Promise[Document.Version]) private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) { case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) => val prev = previous.get_finished val change = Timing.timeit("parse_change", timing) { resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate) } version_result.fulfill(change.version) manager.send(change) true } /* buffered changes */ private object change_buffer { private var assignment: Boolean = false private var nodes: Set[Document.Node.Name] = Set.empty private var commands: Set[Command] = Set.empty def flush(): Unit = synchronized { if (assignment || nodes.nonEmpty || commands.nonEmpty) commands_changed.post(Session.Commands_Changed(assignment, nodes, commands)) if (nodes.nonEmpty) consolidation.update(nodes) assignment = false nodes = Set.empty commands = Set.empty } private val delay_flush = Delay.first(output_delay) { flush() } def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit = synchronized { assignment |= assign for (node <- edited_nodes) { nodes += node } for (command <- cmds) { nodes += command.node_name command.blobs_names.foreach(nodes += _) commands += command } delay_flush.invoke() } def shutdown() { delay_flush.revoke() flush() } } /* postponed changes */ private object postponed_changes { private var postponed: List[Session.Change] = Nil def store(change: Session.Change): Unit = synchronized { postponed ::= change } def flush(state: Document.State): List[Session.Change] = synchronized { val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous)) postponed = unassigned assigned.reverse } } /* node consolidation */ private object consolidation { private val delay = Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) } private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty) private val state = Synchronized(init_state) def exit() { delay.revoke() state.change(_ => None) } def update(new_nodes: Set[Document.Node.Name] = Set.empty) { val active = state.change_result(st => (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes))) if (active) delay.invoke() } def flush(): Set[Document.Node.Name] = state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None)) } /* prover process */ private object prover { private val variable = Synchronized[Option[Prover]](None) def defined: Boolean = variable.value.isDefined def get: Prover = variable.value.get def set(p: Prover) { variable.change(_ => Some(p)) } def reset { variable.change(_ => None) } def await_reset() { variable.guarded_access({ case None => Some((), None) case _ => None }) } } /* file formats and protocol handlers */ private lazy val file_formats: File_Format.Session = File_Format.registry.start_session(session) private val protocol_handlers = Protocol_Handlers.init(session) def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] = protocol_handlers.get(c.getName) match { case Some(h) if Library.is_subclass(h.getClass, c) => Some(h.asInstanceOf[C]) case _ => None } def init_protocol_handler(handler: Session.Protocol_Handler): Unit = protocol_handlers.init(handler) def prover_options(options: Options): Options = protocol_handlers.prover_options(file_formats.prover_options(options)) /* debugger */ private val debugger_handler = new Debugger.Handler(this) init_protocol_handler(debugger_handler) def debugger: Debugger = debugger_handler.debugger /* manager thread */ private val delay_prune = Delay.first(prune_delay) { manager.send(Prune_History) } private val manager: Consumer_Thread[Any] = { /* global state */ val global_state = Synchronized(Document.State.init) /* raw edits */ def handle_raw_edits( doc_blobs: Document.Blobs = Document.Blobs.empty, edits: List[Document.Edit_Text] = Nil, consolidate: List[Document.Node.Name] = Nil) //{{{ { require(prover.defined) if (edits.nonEmpty) prover.get.discontinue_execution() val previous = global_state.value.history.tip.version val version = Future.promise[Document.Version] global_state.change(_.continue_history(previous, edits, version)) raw_edits.post(Session.Raw_Edits(doc_blobs, edits)) change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version)) } //}}} /* resulting changes */ def handle_change(change: Session.Change) //{{{ { require(prover.defined) // define commands { val id_commands = new mutable.ListBuffer[Command] def id_command(command: Command) { for { (name, digest) <- command.blobs_defined if !global_state.value.defined_blob(digest) } { change.version.nodes(name).get_blob match { case Some(blob) => global_state.change(_.define_blob(digest)) prover.get.define_blob(digest, blob.bytes) case None => Output.error_message("Missing blob " + quote(name.toString)) } } if (!global_state.value.defined_command(command.id)) { global_state.change(_.define_command(command)) id_commands += command } } for { (_, edit) <- change.doc_edits } { edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) }) } if (id_commands.nonEmpty) { prover.get.define_commands_bulk(resources, id_commands.toList) } } val assignment = global_state.value.the_assignment(change.previous).check_finished global_state.change(_.define_version(change.version, assignment)) prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate) resources.commit(change) } //}}} /* prover output */ def handle_output(output: Prover.Output) //{{{ { def bad_output() { if (verbose) Output.warning("Ignoring bad prover output: " + output.message.toString) } def change_command(f: Document.State => (Command.State, Document.State)) { try { val st = global_state.change_result(f) if (!st.command.span.is_theory) { change_buffer.invoke(false, Nil, List(st.command)) } } catch { case _: Document.State.Fail => bad_output() } } output match { case msg: Prover.Protocol_Output => val handled = protocol_handlers.invoke(msg) if (!handled) { msg.properties match { case Protocol.Command_Timing(props, state_id, timing) if prover.defined => command_timings.post(Session.Command_Timing(props)) val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache)) case Markup.Theory_Timing(props) => theory_timings.post(Session.Theory_Timing(props)) case Markup.Task_Statistics(props) => task_statistics.post(Session.Task_Statistics(props)) case Protocol.Export(args) if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => val id = Value.Long.unapply(args.id.get).get val export = Export.make_entry("", args, msg.bytes, cache = xz_cache) change_command(_.add_export(id, (args.serial, export))) case Protocol.Loading_Theory(node_name, id) => val blobs_info = build_blobs_info(node_name) try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) } catch { case _: Document.State.Fail => bad_output() } case List(Markup.Commands_Accepted.PROPERTY) => msg.text match { case Protocol.Commands_Accepted(ids) => ids.foreach(id => change_command(_.accumulate(id, Protocol.Commands_Accepted.message, xml_cache))) case _ => bad_output() } case List(Markup.Assign_Update.PROPERTY) => msg.text match { case Protocol.Assign_Update(id, edited, update) => try { val (edited_nodes, cmds) = global_state.change_result(_.assign(id, edited, update)) change_buffer.invoke(true, edited_nodes, cmds) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } delay_prune.invoke() case List(Markup.Removed_Versions.PROPERTY) => msg.text match { case Protocol.Removed(removed) => try { global_state.change(_.removed_versions(removed)) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } case _ => bad_output() } } case _ => output.properties match { case Position.Id(state_id) => change_command(_.accumulate(state_id, output.message, xml_cache)) case _ if output.is_init => val init_ok = try { Isabelle_System.make_services(classOf[Session.Protocol_Handler]) .foreach(init_protocol_handler) true } catch { case exn: Throwable => prover.get.protocol_command("Prover.stop", "1", Exn.message(exn)) false } if (init_ok) { prover.get.options(prover_options(session_options)) prover.get.init_session(resources) phase = Session.Ready debugger.ready() } case Markup.Process_Result(result) if output.is_exit => if (prover.defined) protocol_handlers.exit() for (id <- global_state.value.theories.keys) { val snapshot = global_state.change_result(_.end_theory(id)) finished_theories.post(snapshot) } file_formats.stop_session phase = Session.Terminated(result) prover.reset case _ => raw_output_messages.post(output) } } } //}}} /* main thread */ Consumer_Thread.fork[Any]("Session.manager", daemon = true) { case arg: Any => //{{{ arg match { case output: Prover.Output => if (output.is_syslog) { syslog += output.message syslog_messages.post(output) } if (output.is_stdout || output.is_stderr) raw_output_messages.post(output) else handle_output(output) all_messages.post(output) case input: Prover.Input => all_messages.post(input) case Start(start_prover) if !prover.defined => prover.set(start_prover(manager.send(_))) case Stop => consolidation.exit() delay_prune.revoke() if (prover.defined) { global_state.change(_ => Document.State.init) prover.get.terminate } case Get_State(promise) => promise.fulfill(global_state.value) case Consolidate_Execution => if (prover.defined) { val state = global_state.value state.stable_tip_version match { case None => consolidation.update() case Some(version) => val consolidate = consolidation.flush().iterator.filter(name => !resources.session_base.loaded_theory(name) && !state.node_consolidated(version, name) && state.node_maybe_consolidated(version, name)).toList if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate) } } case Prune_History => if (prover.defined) { val old_versions = global_state.change_result(_.remove_versions(prune_size)) if (old_versions.nonEmpty) prover.get.remove_versions(old_versions) } case Update_Options(options) => if (prover.defined && is_ready) { prover.get.options(prover_options(options)) handle_raw_edits() } global_options.post(Session.Global_Options(options)) case Cancel_Exec(exec_id) if prover.defined => prover.get.cancel_exec(exec_id) case Session.Raw_Edits(doc_blobs, edits) if prover.defined => handle_raw_edits(doc_blobs = doc_blobs, edits = edits) case Session.Dialog_Result(id, serial, result) if prover.defined => prover.get.dialog_result(serial, result) handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) case Protocol_Command(name, args) if prover.defined => prover.get.protocol_command_args(name, args) case change: Session.Change if prover.defined => val state = global_state.value if (!state.removing_versions && state.is_assigned(change.previous)) handle_change(change) else postponed_changes.store(change) case Session.Change_Flush if prover.defined => val state = global_state.value if (!state.removing_versions) postponed_changes.flush(state).foreach(handle_change) case bad => if (verbose) Output.warning("Ignoring bad message: " + bad.toString) } true //}}} } } /* main operations */ def get_state(): Document.State = { if (manager.is_active) { val promise = Future.promise[Document.State] manager.send_wait(Get_State(promise)) promise.join } else Document.State.init } def snapshot(name: Document.Node.Name = Document.Node.Name.empty, pending_edits: List[Text.Edit] = Nil): Document.Snapshot = get_state().snapshot(name, pending_edits) def recent_syntax(name: Document.Node.Name): Outer_Syntax = get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse resources.session_base.overall_syntax @tailrec final def await_stable_snapshot(): Document.Snapshot = { val snapshot = this.snapshot() if (snapshot.is_outdated) { output_delay.sleep await_stable_snapshot() } else snapshot } def start(start_prover: Prover.Receiver => Prover) { file_formats _phase.change( { case Session.Inactive => manager.send(Start(start_prover)) post_phase(Session.Startup) case phase => error("Cannot start prover in phase " + quote(phase.print)) }) } def stop(): Process_Result = { val was_ready = _phase.guarded_access( { case Session.Startup | Session.Shutdown => None case Session.Terminated(_) => Some((false, phase)) case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0))))) case Session.Ready => Some((true, post_phase(Session.Shutdown))) }) if (was_ready) manager.send(Stop) prover.await_reset() change_parser.shutdown() change_buffer.shutdown() manager.shutdown() dispatcher.shutdown() phase match { case Session.Terminated(result) => result case phase => error("Bad session phase after shutdown: " + quote(phase.print)) } } def protocol_command(name: String, args: String*) { manager.send(Protocol_Command(name, args.toList)) } def cancel_exec(exec_id: Document_ID.Exec) { manager.send(Cancel_Exec(exec_id)) } def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) { if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) } def update_options(options: Options) { manager.send_wait(Update_Options(options)) } def dialog_result(id: Document_ID.Generic, serial: Long, result: String) { manager.send(Session.Dialog_Result(id, serial, result)) } } diff --git a/src/Pure/PIDE/xml.scala b/src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala +++ b/src/Pure/PIDE/xml.scala @@ -1,416 +1,428 @@ /* Title: Pure/PIDE/xml.scala Author: Makarius Untyped XML trees and basic data representation. */ package isabelle object XML { /** XML trees **/ /* datatype representation */ type Attribute = Properties.Entry type Attributes = Properties.T sealed abstract class Tree { override def toString: String = string_of_tree(this) } type Body = List[Tree] case class Elem(markup: Markup, body: Body) extends Tree { def name: String = markup.name def update_attributes(more_attributes: Attributes): Elem = if (more_attributes.isEmpty) this else Elem(markup.update_properties(more_attributes), body) def + (att: Attribute): Elem = Elem(markup + att, body) } case class Text(content: String) extends Tree def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil) def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body) def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil) val newline: Text = Text("\n") /* name space */ object Namespace { def apply(prefix: String, target: String): Namespace = new Namespace(prefix, target) } final class Namespace private(prefix: String, target: String) { def apply(name: String): String = prefix + ":" + name val attribute: XML.Attribute = ("xmlns:" + prefix, target) override def toString: String = attribute.toString } /* wrapped elements */ val XML_ELEM = "xml_elem" val XML_NAME = "xml_name" val XML_BODY = "xml_body" object Wrapped_Elem { def apply(markup: Markup, body1: Body, body2: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties), XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) def unapply(tree: Tree): Option[(Markup, Body, Body)] = tree match { case XML.Elem(Markup(XML_ELEM, (XML_NAME, name) :: props), XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) => Some(Markup(name, props), body1, body2) case _ => None } } object Root_Elem { def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body) def unapply(tree: Tree): Option[Body] = tree match { case XML.Elem(Markup(XML_ELEM, Nil), body) => Some(body) case _ => None } } /* traverse text */ def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = { def traverse(x: A, t: Tree): A = t match { case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse) case XML.Elem(_, ts) => (x /: ts)(traverse) case XML.Text(s) => op(x, s) } (a /: body)(traverse) } def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length } /* text content */ def content(body: Body): String = { val text = new StringBuilder(text_length(body)) traverse_text(body)(()) { case (_, s) => text.append(s) } text.toString } def content(tree: Tree): String = content(List(tree)) /** string representation **/ val header: String = "\n" def output_char(c: Char, s: StringBuilder) { c match { case '<' => s ++= "<" case '>' => s ++= ">" case '&' => s ++= "&" case '"' => s ++= """ case '\'' => s ++= "'" case _ => s += c } } def output_string(str: String, s: StringBuilder) { if (str == null) s ++= str else str.iterator.foreach(c => output_char(c, s)) } def string_of_body(body: Body): String = { val s = new StringBuilder def text(txt: String) { output_string(txt, s) } def elem(markup: Markup) { s ++= markup.name for ((a, b) <- markup.properties) { s += ' '; s ++= a; s += '='; s += '"'; text(b); s += '"' } } def tree(t: Tree): Unit = t match { case XML.Elem(markup, Nil) => s += '<'; elem(markup); s ++= "/>" case XML.Elem(markup, ts) => s += '<'; elem(markup); s += '>' ts.foreach(tree) s ++= "' case XML.Text(txt) => text(txt) } body.foreach(tree) s.toString } def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) /** cache **/ - def make_cache(initial_size: Int = 131071, max_string: Int = 100): Cache = - new Cache(initial_size, max_string) + object Cache + { + def make( + max_string: Int = isabelle.Cache.default_max_string, + initial_size: Int = isabelle.Cache.default_initial_size): Cache = + new Cache(max_string, initial_size) - class Cache private[XML](initial_size: Int, max_string: Int) - extends isabelle.Cache(initial_size, max_string) + val none: Cache = make(max_string = 0) + } + + class Cache private[XML](max_string: Int, initial_size: Int) + extends isabelle.Cache(max_string, initial_size) { protected def cache_props(x: Properties.T): Properties.T = { if (x.isEmpty) x else lookup(x) match { case Some(y) => y case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2)))) } } protected def cache_markup(x: Markup): Markup = { lookup(x) match { case Some(y) => y case None => x match { case Markup(name, props) => store(Markup(cache_string(name), cache_props(props))) } } } protected def cache_tree(x: XML.Tree): XML.Tree = { lookup(x) match { case Some(y) => y case None => x match { case XML.Elem(markup, body) => store(XML.Elem(cache_markup(markup), cache_body(body))) case XML.Text(text) => store(XML.Text(cache_string(text))) } } } protected def cache_body(x: XML.Body): XML.Body = { if (x.isEmpty) x else lookup(x) match { case Some(y) => y case None => x.map(cache_tree) } } // main methods - def props(x: Properties.T): Properties.T = synchronized { cache_props(x) } - def markup(x: Markup): Markup = synchronized { cache_markup(x) } - def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) } - def body(x: XML.Body): XML.Body = synchronized { cache_body(x) } - def elem(x: XML.Elem): XML.Elem = synchronized { cache_tree(x).asInstanceOf[XML.Elem] } + def props(x: Properties.T): Properties.T = + if (no_cache) x else synchronized { cache_props(x) } + def markup(x: Markup): Markup = + if (no_cache) x else synchronized { cache_markup(x) } + def tree(x: XML.Tree): XML.Tree = + if (no_cache) x else synchronized { cache_tree(x) } + def body(x: XML.Body): XML.Body = + if (no_cache) x else synchronized { cache_body(x) } + def elem(x: XML.Elem): XML.Elem = + if (no_cache) x else synchronized { cache_tree(x).asInstanceOf[XML.Elem] } } /** XML as data representation language **/ abstract class Error(s: String) extends Exception(s) class XML_Atom(s: String) extends Error(s) class XML_Body(body: XML.Body) extends Error("") object Encode { type T[A] = A => XML.Body type V[A] = PartialFunction[A, (List[String], XML.Body)] type P[A] = PartialFunction[A, List[String]] /* atomic values */ def long_atom(i: Long): String = Library.signed_string_of_long(i) def int_atom(i: Int): String = Library.signed_string_of_int(i) def bool_atom(b: Boolean): String = if (b) "1" else "0" def unit_atom(u: Unit) = "" /* structural nodes */ private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts) private def vector(xs: List[String]): XML.Attributes = xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) }) private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree = XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2) /* representation of standard types */ val tree: T[XML.Tree] = (t => List(t)) val properties: T[Properties.T] = (props => List(XML.Elem(Markup(":", props), Nil))) val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s))) val long: T[Long] = (x => string(long_atom(x))) val int: T[Int] = (x => string(int_atom(x))) val bool: T[Boolean] = (x => string(bool_atom(x))) val unit: T[Unit] = (x => string(unit_atom(x))) def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = (x => List(node(f(x._1)), node(g(x._2)))) def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3)))) def list[A](f: T[A]): T[List[A]] = (xs => xs.map((x: A) => node(f(x)))) def option[A](f: T[A]): T[Option[A]] = { case None => Nil case Some(x) => List(node(f(x))) } def variant[A](fs: List[V[A]]): T[A] = { case x => val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get List(tagged(tag, f(x))) } } object Decode { type T[A] = XML.Body => A type V[A] = (List[String], XML.Body) => A type P[A] = PartialFunction[List[String], A] /* atomic values */ def long_atom(s: String): Long = try { java.lang.Long.parseLong(s) } catch { case e: NumberFormatException => throw new XML_Atom(s) } def int_atom(s: String): Int = try { Integer.parseInt(s) } catch { case e: NumberFormatException => throw new XML_Atom(s) } def bool_atom(s: String): Boolean = if (s == "1") true else if (s == "0") false else throw new XML_Atom(s) def unit_atom(s: String): Unit = if (s == "") () else throw new XML_Atom(s) /* structural nodes */ private def node(t: XML.Tree): XML.Body = t match { case XML.Elem(Markup(":", Nil), ts) => ts case _ => throw new XML_Body(List(t)) } private def vector(atts: XML.Attributes): List[String] = atts.iterator.zipWithIndex.map( { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) = t match { case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts)) case _ => throw new XML_Body(List(t)) } /* representation of standard types */ val tree: T[XML.Tree] = { case List(t) => t case ts => throw new XML_Body(ts) } val properties: T[Properties.T] = { case List(XML.Elem(Markup(":", props), Nil)) => props case ts => throw new XML_Body(ts) } val string: T[String] = { case Nil => "" case List(XML.Text(s)) => s case ts => throw new XML_Body(ts) } val long: T[Long] = (x => long_atom(string(x))) val int: T[Int] = (x => int_atom(string(x))) val bool: T[Boolean] = (x => bool_atom(string(x))) val unit: T[Unit] = (x => unit_atom(string(x))) def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = { case List(t1, t2) => (f(node(t1)), g(node(t2))) case ts => throw new XML_Body(ts) } def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = { case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3))) case ts => throw new XML_Body(ts) } def list[A](f: T[A]): T[List[A]] = (ts => ts.map(t => f(node(t)))) def option[A](f: T[A]): T[Option[A]] = { case Nil => None case List(t) => Some(f(node(t))) case ts => throw new XML_Body(ts) } def variant[A](fs: List[V[A]]): T[A] = { case List(t) => val (tag, (xs, ts)) = tagged(t) val f = try { fs(tag) } catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) } f(xs, ts) case ts => throw new XML_Body(ts) } } } diff --git a/src/Pure/Thy/export.scala b/src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala +++ b/src/Pure/Thy/export.scala @@ -1,458 +1,458 @@ /* Title: Pure/Thy/export.scala Author: Makarius Manage theory exports: compressed blobs. */ package isabelle import scala.annotation.tailrec import scala.util.matching.Regex object Export { /* artefact names */ val DOCUMENT_ID = "PIDE/document_id" val FILES = "PIDE/files" val MARKUP = "PIDE/markup" val MESSAGES = "PIDE/messages" val DOCUMENT_PREFIX = "document/" val CITATIONS = DOCUMENT_PREFIX + "citations" val THEORY_PREFIX: String = "theory/" val PROOFS_PREFIX: String = "proofs/" def explode_name(s: String): List[String] = space_explode('/', s) def implode_name(elems: Iterable[String]): String = elems.mkString("/") /* SQL data model */ object Data { val session_name = SQL.Column.string("session_name").make_primary_key val theory_name = SQL.Column.string("theory_name").make_primary_key val name = SQL.Column.string("name").make_primary_key val executable = SQL.Column.bool("executable") val compressed = SQL.Column.bool("compressed") val body = SQL.Column.bytes("body") val table = SQL.Table("isabelle_exports", List(session_name, theory_name, name, executable, compressed, body)) def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source = "WHERE " + Data.session_name.equal(session_name) + (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) + (if (name == "") "" else " AND " + Data.name.equal(name)) } def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean = { val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name)) db.using_statement(select)(stmt => stmt.execute_query().next()) } def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] = { val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name)) db.using_statement(select)(stmt => stmt.execute_query().iterator(res => res.string(Data.name)).toList) } def read_theory_names(db: SQL.Database, session_name: String): List[String] = { val select = Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) db.using_statement(select)(stmt => stmt.execute_query().iterator(_.string(Data.theory_name)).toList) } def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] = { val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) db.using_statement(select)(stmt => stmt.execute_query().iterator(res => (res.string(Data.theory_name), res.string(Data.name))).toList) } def message(msg: String, theory_name: String, name: String): String = msg + " " + quote(name) + " for theory " + quote(theory_name) def compound_name(a: String, b: String): String = a + ":" + b def empty_entry(theory_name: String, name: String): Entry = - Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XZ.no_cache()) + Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XZ.Cache.none) sealed case class Entry( session_name: String, theory_name: String, name: String, executable: Boolean, body: Future[(Boolean, Bytes)], cache: XZ.Cache) { override def toString: String = name def compound_name: String = Export.compound_name(theory_name, name) def name_has_prefix(s: String): Boolean = name.startsWith(s) val name_elems: List[String] = explode_name(name) def name_extends(elems: List[String]): Boolean = name_elems.startsWith(elems) && name_elems != elems def text: String = uncompressed.text def uncompressed: Bytes = { val (compressed, bytes) = body.join if (compressed) bytes.uncompress(cache = cache) else bytes } def uncompressed_yxml: XML.Body = YXML.parse_body(UTF8.decode_permissive(uncompressed)) def write(db: SQL.Database) { val (compressed, bytes) = body.join db.using_statement(Data.table.insert())(stmt => { stmt.string(1) = session_name stmt.string(2) = theory_name stmt.string(3) = name stmt.bool(4) = executable stmt.bool(5) = compressed stmt.bytes(6) = bytes stmt.execute() }) } } def make_regex(pattern: String): Regex = { @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = chs match { case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) case '*' :: rest => make("[^:/]*" :: result, depth, rest) case '?' :: rest => make("[^:/]" :: result, depth, rest) case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) case '{' :: rest => make("(" :: result, depth + 1, rest) case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest) case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest) case c :: rest => make(c.toString :: result, depth, rest) case Nil => result.reverse.mkString.r } make(Nil, 0, pattern.toList) } def make_matcher(pattern: String): (String, String) => Boolean = { val regex = make_regex(pattern) (theory_name: String, name: String) => regex.pattern.matcher(compound_name(theory_name, name)).matches } def make_entry( session_name: String, args: Protocol.Export.Args, bytes: Bytes, cache: XZ.Cache): Entry = { val body = if (args.compress) Future.fork(bytes.maybe_compress(cache = cache)) else Future.value((false, bytes)) Entry(session_name, args.theory_name, args.name, args.executable, body, cache) } def read_entry( db: SQL.Database, cache: XZ.Cache, session_name: String, theory_name: String, name: String): Option[Entry] = { val select = Data.table.select(List(Data.executable, Data.compressed, Data.body), Data.where_equal(session_name, theory_name, name)) db.using_statement(select)(stmt => { val res = stmt.execute_query() if (res.next()) { val executable = res.bool(Data.executable) val compressed = res.bool(Data.compressed) val bytes = res.bytes(Data.body) val body = Future.value(compressed, bytes) Some(Entry(session_name, theory_name, name, executable, body, cache)) } else None }) } def read_entry( dir: Path, cache: XZ.Cache, session_name: String, theory_name: String, name: String): Option[Entry] = { val path = dir + Path.basic(theory_name) + Path.explode(name) if (path.is_file) { val executable = File.is_executable(path) val uncompressed = Bytes.read(path) val body = Future.value((false, uncompressed)) Some(Entry(session_name, theory_name, name, executable, body, cache)) } else None } /* database consumer thread */ def consumer(db: SQL.Database, cache: XZ.Cache): Consumer = new Consumer(db, cache) class Consumer private[Export](db: SQL.Database, cache: XZ.Cache) { private val errors = Synchronized[List[String]](Nil) private val consumer = Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")( bulk = { case (entry, _) => entry.body.is_finished }, consume = (args: List[(Entry, Boolean)]) => { val results = db.transaction { for ((entry, strict) <- args) yield { if (read_name(db, entry.session_name, entry.theory_name, entry.name)) { if (strict) { val msg = message("Duplicate export", entry.theory_name, entry.name) errors.change(msg :: _) } Exn.Res(()) } else Exn.capture { entry.write(db) } } } (results, true) }) def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = consumer.send(make_entry(session_name, args, body, cache) -> args.strict) def shutdown(close: Boolean = false): List[String] = { consumer.shutdown() if (close) db.close() errors.value.reverse } } /* abstract provider */ object Provider { def none: Provider = new Provider { def apply(export_name: String): Option[Entry] = None def focus(other_theory: String): Provider = this override def toString: String = "none" } def database_context( context: Sessions.Database_Context, sessions: List[String], theory_name: String): Provider = new Provider { def apply(export_name: String): Option[Entry] = context.read_export(sessions, theory_name, export_name) def focus(other_theory: String): Provider = this override def toString: String = context.toString } def database( db: SQL.Database, cache: XZ.Cache, session_name: String, theory_name: String): Provider = new Provider { def apply(export_name: String): Option[Entry] = read_entry(db, cache, session_name, theory_name, export_name) def focus(other_theory: String): Provider = if (other_theory == theory_name) this else Provider.database(db, cache, session_name, other_theory) override def toString: String = db.toString } def snapshot(snapshot: Document.Snapshot): Provider = new Provider { def apply(export_name: String): Option[Entry] = snapshot.exports_map.get(export_name) def focus(other_theory: String): Provider = if (other_theory == snapshot.node_name.theory) this else { val node_name = snapshot.version.nodes.theory_name(other_theory) getOrElse error("Bad theory " + quote(other_theory)) Provider.snapshot(snapshot.state.snapshot(node_name)) } override def toString: String = snapshot.toString } def directory( dir: Path, cache: XZ.Cache, session_name: String, theory_name: String): Provider = new Provider { def apply(export_name: String): Option[Entry] = read_entry(dir, cache, session_name, theory_name, export_name) def focus(other_theory: String): Provider = if (other_theory == theory_name) this else Provider.directory(dir, cache, session_name, other_theory) override def toString: String = dir.toString } } trait Provider { def apply(export_name: String): Option[Entry] def uncompressed_yxml(export_name: String): XML.Body = apply(export_name) match { case Some(entry) => entry.uncompressed_yxml case None => Nil } def focus(other_theory: String): Provider } /* export to file-system */ def export_files( store: Sessions.Store, session_name: String, export_dir: Path, progress: Progress = new Progress, export_prune: Int = 0, export_list: Boolean = false, export_patterns: List[String] = Nil) { using(store.open_database(session_name))(db => { db.transaction { val export_names = read_theory_exports(db, session_name) // list if (export_list) { (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)). sorted.foreach(progress.echo) } // export if (export_patterns.nonEmpty) { val exports = (for { export_pattern <- export_patterns.iterator matcher = make_matcher(export_pattern) (theory_name, name) <- export_names if matcher(theory_name, name) } yield (theory_name, name)).toSet for { (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1) name <- group.map(_._2).sorted entry <- read_entry(db, store.xz_cache, session_name, theory_name, name) } { val elems = theory_name :: space_explode('/', name) val path = if (elems.length < export_prune + 1) { error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems)) } else export_dir + Path.make(elems.drop(export_prune)) progress.echo("export " + path + (if (entry.executable) " (executable)" else "")) Isabelle_System.make_directory(path.dir) Bytes.write(path, entry.uncompressed) File.set_executable(path, entry.executable) } } } }) } /* Isabelle tool wrapper */ val default_export_dir: Path = Path.explode("export") val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", Scala_Project.here, args => { /* arguments */ var export_dir = default_export_dir var dirs: List[Path] = Nil var export_list = false var no_build = false var options = Options.init() var export_prune = 0 var export_patterns: List[String] = Nil val getopts = Getopts(""" Usage: isabelle export [OPTIONS] SESSION Options are: -O DIR output directory for exported files (default: """ + default_export_dir + """) -d DIR include session directory -l list exports -n no build of session -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NUM prune path of exported files by NUM elements -x PATTERN extract files matching pattern (e.g. "*:**" for all) List or export theory exports for SESSION: named blobs produced by isabelle build. Option -l or -x is required; option -x may be repeated. The PATTERN language resembles glob patterns in the shell, with ? and * (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], and variants {pattern1,pattern2,pattern3}. """, "O:" -> (arg => export_dir = Path.explode(arg)), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "l" -> (_ => export_list = true), "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "p:" -> (arg => export_prune = Value.Int.parse(arg)), "x:" -> (arg => export_patterns ::= arg)) val more_args = getopts(args) val session_name = more_args match { case List(session_name) if export_list || export_patterns.nonEmpty => session_name case _ => getopts.usage() } val progress = new Console_Progress() /* build */ if (!no_build) { val rc = progress.interrupt_handler { Build.build_logic(options, session_name, progress = progress, dirs = dirs) } if (rc != 0) sys.exit(rc) } /* export files */ val store = Sessions.store(options) export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune, export_list = export_list, export_patterns = export_patterns) }) } diff --git a/src/Pure/Thy/export_theory.scala b/src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala +++ b/src/Pure/Thy/export_theory.scala @@ -1,755 +1,755 @@ /* Title: Pure/Thy/export_theory.scala Author: Makarius Export foundational theory content. */ package isabelle import scala.collection.immutable.SortedMap object Export_Theory { /** session content **/ sealed case class Session(name: String, theory_graph: Graph[String, Option[Theory]]) { override def toString: String = name def theory(theory_name: String): Option[Theory] = if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name) else None def theories: List[Theory] = theory_graph.topological_order.flatMap(theory) } def read_session( store: Sessions.Store, sessions_structure: Sessions.Structure, session_name: String, progress: Progress = new Progress, - cache: Term.Cache = Term.make_cache()): Session = + cache: Term.Cache = Term.Cache.make()): Session = { val thys = sessions_structure.build_requirements(List(session_name)).flatMap(session => using(store.open_database(session))(db => { db.transaction { for (theory <- Export.read_theory_names(db, session)) yield { progress.echo("Reading theory " + theory) read_theory(Export.Provider.database(db, store.xz_cache, session, theory), - session, theory, cache = Some(cache)) + session, theory, cache = cache) } } })) val graph0 = (Graph.string[Option[Theory]] /: thys) { case (g, thy) => g.default_node(thy.name, Some(thy)) } val graph1 = (graph0 /: thys) { case (g0, thy) => (g0 /: thy.parents) { case (g1, parent) => g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) } } Session(session_name, graph1) } /** theory content **/ sealed case class Theory(name: String, parents: List[String], types: List[Type], consts: List[Const], axioms: List[Axiom], thms: List[Thm], classes: List[Class], locales: List[Locale], locale_dependencies: List[Locale_Dependency], classrel: List[Classrel], arities: List[Arity], constdefs: List[Constdef], typedefs: List[Typedef], datatypes: List[Datatype], spec_rules: List[Spec_Rule]) { override def toString: String = name def entity_iterator: Iterator[Entity] = types.iterator.map(_.entity) ++ consts.iterator.map(_.entity) ++ axioms.iterator.map(_.entity) ++ thms.iterator.map(_.entity) ++ classes.iterator.map(_.entity) ++ locales.iterator.map(_.entity) ++ locale_dependencies.iterator.map(_.entity) def cache(cache: Term.Cache): Theory = Theory(cache.string(name), parents.map(cache.string(_)), types.map(_.cache(cache)), consts.map(_.cache(cache)), axioms.map(_.cache(cache)), thms.map(_.cache(cache)), classes.map(_.cache(cache)), locales.map(_.cache(cache)), locale_dependencies.map(_.cache(cache)), classrel.map(_.cache(cache)), arities.map(_.cache(cache)), constdefs.map(_.cache(cache)), typedefs.map(_.cache(cache)), datatypes.map(_.cache(cache)), spec_rules.map(_.cache(cache))) } def read_theory(provider: Export.Provider, session_name: String, theory_name: String, - cache: Option[Term.Cache] = None): Theory = + cache: Term.Cache = Term.Cache.none): Theory = { val parents = if (theory_name == Thy_Header.PURE) Nil else { provider(Export.THEORY_PREFIX + "parents") match { case Some(entry) => split_lines(entry.uncompressed.text) case None => error("Missing theory export in session " + quote(session_name) + ": " + quote(theory_name)) } } val theory = Theory(theory_name, parents, read_types(provider), read_consts(provider), read_axioms(provider), read_thms(provider), read_classes(provider), read_locales(provider), read_locale_dependencies(provider), read_classrel(provider), read_arities(provider), read_constdefs(provider), read_typedefs(provider), read_datatypes(provider), read_spec_rules(provider)) - if (cache.isDefined) theory.cache(cache.get) else theory + if (cache.no_cache) theory else theory.cache(cache) } def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A = { val session_name = Thy_Header.PURE val theory_name = Thy_Header.PURE using(store.open_database(session_name))(db => { db.transaction { read(Export.Provider.database( db, store.xz_cache, session_name, theory_name), session_name, theory_name) } }) } - def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory = + def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.Cache.none): Theory = read_pure(store, read_theory(_, _, _, cache = cache)) def read_pure_proof( - store: Sessions.Store, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] = + store: Sessions.Store, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] = read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache)) /* entities */ object Kind extends Enumeration { val TYPE = Value("type") val CONST = Value("const") val AXIOM = Value("axiom") val THM = Value("thm") val PROOF = Value("proof") val CLASS = Value("class") val LOCALE = Value("locale") val LOCALE_DEPENDENCY = Value("locale_dependency") val DOCUMENT_HEADING = Value("document_heading") val DOCUMENT_TEXT = Value("document_text") val PROOF_TEXT = Value("proof_text") } sealed case class Entity( kind: Kind.Value, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long) { override def toString: String = kind.toString + " " + quote(name) def cache(cache: Term.Cache): Entity = Entity(kind, cache.string(name), cache.string(xname), cache.position(pos), id, serial) } def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) = { def err(): Nothing = throw new XML.XML_Body(List(tree)) tree match { case XML.Elem(Markup(Markup.ENTITY, props), body) => val name = Markup.Name.unapply(props) getOrElse err() val xname = Markup.XName.unapply(props) getOrElse err() val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID) val id = Position.Id.unapply(props) val serial = Markup.Serial.unapply(props) getOrElse err() (Entity(kind, name, xname, pos, id, serial), body) case _ => err() } } /* approximative syntax */ object Assoc extends Enumeration { val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value } sealed abstract class Syntax case object No_Syntax extends Syntax case class Prefix(delim: String) extends Syntax case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax def decode_syntax: XML.Decode.T[Syntax] = XML.Decode.variant(List( { case (Nil, Nil) => No_Syntax }, { case (List(delim), Nil) => Prefix(delim) }, { case (Nil, body) => import XML.Decode._ val (ass, delim, pri) = triple(int, string, int)(body) Infix(Assoc(ass), delim, pri) })) /* types */ sealed case class Type( entity: Entity, syntax: Syntax, args: List[String], abbrev: Option[Term.Typ]) { def cache(cache: Term.Cache): Type = Type(entity.cache(cache), syntax, args.map(cache.string(_)), abbrev.map(cache.typ(_))) } def read_types(provider: Export.Provider): List[Type] = provider.uncompressed_yxml(Export.THEORY_PREFIX + "types").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.TYPE, tree) val (syntax, args, abbrev) = { import XML.Decode._ triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body) } Type(entity, syntax, args, abbrev) }) /* consts */ sealed case class Const( entity: Entity, syntax: Syntax, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term], propositional: Boolean) { def cache(cache: Term.Cache): Const = Const(entity.cache(cache), syntax, typargs.map(cache.string(_)), cache.typ(typ), abbrev.map(cache.term(_)), propositional) } def read_consts(provider: Export.Provider): List[Const] = provider.uncompressed_yxml(Export.THEORY_PREFIX + "consts").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.CONST, tree) val (syntax, (typargs, (typ, (abbrev, propositional)))) = { import XML.Decode._ pair(decode_syntax, pair(list(string), pair(Term_XML.Decode.typ, pair(option(Term_XML.Decode.term), bool))))(body) } Const(entity, syntax, typargs, typ, abbrev, propositional) }) /* axioms */ sealed case class Prop( typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], term: Term.Term) { def cache(cache: Term.Cache): Prop = Prop( typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), cache.term(term)) } def decode_prop(body: XML.Body): Prop = { val (typargs, args, t) = { import XML.Decode._ import Term_XML.Decode._ triple(list(pair(string, sort)), list(pair(string, typ)), term)(body) } Prop(typargs, args, t) } sealed case class Axiom(entity: Entity, prop: Prop) { def cache(cache: Term.Cache): Axiom = Axiom(entity.cache(cache), prop.cache(cache)) } def read_axioms(provider: Export.Provider): List[Axiom] = provider.uncompressed_yxml(Export.THEORY_PREFIX + "axioms").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.AXIOM, tree) val prop = decode_prop(body) Axiom(entity, prop) }) /* theorems */ sealed case class Thm_Id(serial: Long, theory_name: String) { def pure: Boolean = theory_name == Thy_Header.PURE } sealed case class Thm( entity: Entity, prop: Prop, deps: List[String], proof: Term.Proof) { def cache(cache: Term.Cache): Thm = Thm( entity.cache(cache), prop.cache(cache), deps.map(cache.string _), cache.proof(proof)) } def read_thms(provider: Export.Provider): List[Thm] = provider.uncompressed_yxml(Export.THEORY_PREFIX + "thms").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.THM, tree) val (prop, deps, prf) = { import XML.Decode._ import Term_XML.Decode._ triple(decode_prop, list(string), proof)(body) } Thm(entity, prop, deps, prf) }) sealed case class Proof( typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], term: Term.Term, proof: Term.Proof) { def prop: Prop = Prop(typargs, args, term) def cache(cache: Term.Cache): Proof = Proof( typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), cache.term(term), cache.proof(proof)) } def read_proof( - provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] = + provider: Export.Provider, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] = { for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) } yield { val body = entry.uncompressed_yxml val (typargs, (args, (prop_body, proof_body))) = { import XML.Decode._ import Term_XML.Decode._ pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(x => x, x => x)))(body) } val env = args.toMap val prop = Term_XML.Decode.term_env(env)(prop_body) val proof = Term_XML.Decode.proof_env(env)(proof_body) val result = Proof(typargs, args, prop, proof) - cache.map(result.cache(_)) getOrElse result + if (cache.no_cache) result else result.cache(cache) } } def read_proof_boxes( store: Sessions.Store, provider: Export.Provider, proof: Term.Proof, suppress: Thm_Id => Boolean = _ => false, - cache: Option[Term.Cache] = None): List[(Thm_Id, Proof)] = + cache: Term.Cache = Term.Cache.none): List[(Thm_Id, Proof)] = { var seen = Set.empty[Long] var result = SortedMap.empty[Long, (Thm_Id, Proof)] def boxes(context: Option[(Long, Term.Proof)], prf: Term.Proof) { prf match { case Term.Abst(_, _, p) => boxes(context, p) case Term.AbsP(_, _, p) => boxes(context, p) case Term.Appt(p, _) => boxes(context, p) case Term.AppP(p, q) => boxes(context, p); boxes(context, q) case thm: Term.PThm if !seen(thm.serial) => seen += thm.serial val id = Thm_Id(thm.serial, thm.theory_name) if (!suppress(id)) { val read = if (id.pure) Export_Theory.read_pure_proof(store, id, cache = cache) else Export_Theory.read_proof(provider, id, cache = cache) read match { case Some(p) => result += (thm.serial -> (id -> p)) boxes(Some((thm.serial, p.proof)), p.proof) case None => error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")" + (context match { case None => "" case Some((i, p)) => " in proof " + i + ":\n" + p })) } } case _ => } } boxes(None, proof) result.iterator.map(_._2).toList } /* type classes */ sealed case class Class( entity: Entity, params: List[(String, Term.Typ)], axioms: List[Prop]) { def cache(cache: Term.Cache): Class = Class(entity.cache(cache), params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), axioms.map(_.cache(cache))) } def read_classes(provider: Export.Provider): List[Class] = provider.uncompressed_yxml(Export.THEORY_PREFIX + "classes").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.CLASS, tree) val (params, axioms) = { import XML.Decode._ import Term_XML.Decode._ pair(list(pair(string, typ)), list(decode_prop))(body) } Class(entity, params, axioms) }) /* locales */ sealed case class Locale( entity: Entity, typargs: List[(String, Term.Sort)], args: List[((String, Term.Typ), Syntax)], axioms: List[Prop]) { def cache(cache: Term.Cache): Locale = Locale(entity.cache(cache), typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case ((name, typ), syntax) => ((cache.string(name), cache.typ(typ)), syntax) }), axioms.map(_.cache(cache))) } def read_locales(provider: Export.Provider): List[Locale] = provider.uncompressed_yxml(Export.THEORY_PREFIX + "locales").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.LOCALE, tree) val (typargs, args, axioms) = { import XML.Decode._ import Term_XML.Decode._ triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)), list(decode_prop))(body) } Locale(entity, typargs, args, axioms) }) /* locale dependencies */ sealed case class Locale_Dependency( entity: Entity, source: String, target: String, prefix: List[(String, Boolean)], subst_types: List[((String, Term.Sort), Term.Typ)], subst_terms: List[((String, Term.Typ), Term.Term)]) { def cache(cache: Term.Cache): Locale_Dependency = Locale_Dependency(entity.cache(cache), cache.string(source), cache.string(target), prefix.map({ case (name, mandatory) => (cache.string(name), mandatory) }), subst_types.map({ case ((a, s), ty) => ((cache.string(a), cache.sort(s)), cache.typ(ty)) }), subst_terms.map({ case ((x, ty), t) => ((cache.string(x), cache.typ(ty)), cache.term(t)) })) def is_inclusion: Boolean = subst_types.isEmpty && subst_terms.isEmpty } def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] = provider.uncompressed_yxml(Export.THEORY_PREFIX + "locale_dependencies").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.LOCALE_DEPENDENCY, tree) val (source, (target, (prefix, (subst_types, subst_terms)))) = { import XML.Decode._ import Term_XML.Decode._ pair(string, pair(string, pair(list(pair(string, bool)), pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body) } Locale_Dependency(entity, source, target, prefix, subst_types, subst_terms) }) /* sort algebra */ sealed case class Classrel(class1: String, class2: String, prop: Prop) { def cache(cache: Term.Cache): Classrel = Classrel(cache.string(class1), cache.string(class2), prop.cache(cache)) } def read_classrel(provider: Export.Provider): List[Classrel] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "classrel") val classrel = { import XML.Decode._ list(pair(decode_prop, pair(string, string)))(body) } for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop) } sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String, prop: Prop) { def cache(cache: Term.Cache): Arity = Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain), prop.cache(cache)) } def read_arities(provider: Export.Provider): List[Arity] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "arities") val arities = { import XML.Decode._ import Term_XML.Decode._ list(pair(decode_prop, triple(string, list(sort), string)))(body) } for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop) } /* Pure constdefs */ sealed case class Constdef(name: String, axiom_name: String) { def cache(cache: Term.Cache): Constdef = Constdef(cache.string(name), cache.string(axiom_name)) } def read_constdefs(provider: Export.Provider): List[Constdef] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs") val constdefs = { import XML.Decode._ list(pair(string, string))(body) } for ((name, axiom_name) <- constdefs) yield Constdef(name, axiom_name) } /* HOL typedefs */ sealed case class Typedef(name: String, rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String) { def cache(cache: Term.Cache): Typedef = Typedef(cache.string(name), cache.typ(rep_type), cache.typ(abs_type), cache.string(rep_name), cache.string(abs_name), cache.string(axiom_name)) } def read_typedefs(provider: Export.Provider): List[Typedef] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs") val typedefs = { import XML.Decode._ import Term_XML.Decode._ list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body) } for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs } yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name) } /* HOL datatypes */ sealed case class Datatype( pos: Position.T, name: String, co: Boolean, typargs: List[(String, Term.Sort)], typ: Term.Typ, constructors: List[(Term.Term, Term.Typ)]) { def id: Option[Long] = Position.Id.unapply(pos) def cache(cache: Term.Cache): Datatype = Datatype( cache.position(pos), cache.string(name), co, typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), cache.typ(typ), constructors.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) })) } def read_datatypes(provider: Export.Provider): List[Datatype] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes") val datatypes = { import XML.Decode._ import Term_XML.Decode._ list(pair(properties, pair(string, pair(bool, pair(list(pair(string, sort)), pair(typ, list(pair(term, typ))))))))(body) } for ((pos, (name, (co, (typargs, (typ, constructors))))) <- datatypes) yield Datatype(pos, name, co, typargs, typ, constructors) } /* Pure spec rules */ sealed abstract class Recursion { def cache(cache: Term.Cache): Recursion = this match { case Primrec(types) => Primrec(types.map(cache.string)) case Primcorec(types) => Primcorec(types.map(cache.string)) case _ => this } } case class Primrec(types: List[String]) extends Recursion case object Recdef extends Recursion case class Primcorec(types: List[String]) extends Recursion case object Corec extends Recursion case object Unknown_Recursion extends Recursion val decode_recursion: XML.Decode.T[Recursion] = { import XML.Decode._ variant(List( { case (Nil, a) => Primrec(list(string)(a)) }, { case (Nil, Nil) => Recdef }, { case (Nil, a) => Primcorec(list(string)(a)) }, { case (Nil, Nil) => Corec }, { case (Nil, Nil) => Unknown_Recursion })) } sealed abstract class Rough_Classification { def is_equational: Boolean = this.isInstanceOf[Equational] def is_inductive: Boolean = this == Inductive def is_co_inductive: Boolean = this == Co_Inductive def is_relational: Boolean = is_inductive || is_co_inductive def is_unknown: Boolean = this == Unknown def cache(cache: Term.Cache): Rough_Classification = this match { case Equational(recursion) => Equational(recursion.cache(cache)) case _ => this } } case class Equational(recursion: Recursion) extends Rough_Classification case object Inductive extends Rough_Classification case object Co_Inductive extends Rough_Classification case object Unknown extends Rough_Classification val decode_rough_classification: XML.Decode.T[Rough_Classification] = { import XML.Decode._ variant(List( { case (Nil, a) => Equational(decode_recursion(a)) }, { case (Nil, Nil) => Inductive }, { case (Nil, Nil) => Co_Inductive }, { case (Nil, Nil) => Unknown })) } sealed case class Spec_Rule( pos: Position.T, name: String, rough_classification: Rough_Classification, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], terms: List[(Term.Term, Term.Typ)], rules: List[Term.Term]) { def id: Option[Long] = Position.Id.unapply(pos) def cache(cache: Term.Cache): Spec_Rule = Spec_Rule( cache.position(pos), cache.string(name), rough_classification.cache(cache), typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }), rules.map(cache.term(_))) } def read_spec_rules(provider: Export.Provider): List[Spec_Rule] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules") val spec_rules = { import XML.Decode._ import Term_XML.Decode._ list( pair(properties, pair(string, pair(decode_rough_classification, pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(list(pair(term, typ)), list(term))))))))(body) } for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules) yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules) } } diff --git a/src/Pure/Thy/sessions.scala b/src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala +++ b/src/Pure/Thy/sessions.scala @@ -1,1515 +1,1518 @@ /* Title: Pure/Thy/sessions.scala Author: Makarius Cumulative session information. */ package isabelle import java.io.{File => JFile} import java.nio.ByteBuffer import java.nio.channels.FileChannel import java.nio.file.StandardOpenOption import scala.collection.{SortedSet, SortedMap} import scala.collection.mutable object Sessions { /* 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_name: String = "Pure.Sessions" val UNSORTED = "Unsorted" val DRAFT = "Draft" def is_pure(name: String): Boolean = name == Thy_Header.PURE def exclude_session(name: String): Boolean = name == "" || name == DRAFT def exclude_theory(name: String): Boolean = name == root_name || name == "README" || name == "index" || name == "bib" /* ROOTS file format */ class File_Format extends isabelle.File_Format { val format_name: String = roots_name val file_ext = "" override def detect(name: String): Boolean = Thy_Header.split_file_name(name) match { case Some((_, file_name)) => file_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 """ + Outer_Syntax.quote_string(name) + """ end""" } /* base info and source dependencies */ sealed case class Base( pos: Position.T = Position.none, session_directories: Map[JFile, String] = Map.empty, global_theories: Map[String, String] = Map.empty, session_theories: List[Document.Node.Name] = Nil, document_theories: List[Document.Node.Name] = Nil, loaded_theories: Graph[String, Outer_Syntax] = Graph.string, used_theories: List[(Document.Node.Name, Options)] = Nil, load_commands: Map[Document.Node.Name, 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, sources: List[(Path, SHA1.Digest)] = Nil, session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph, errors: List[String] = Nil) { override def toString: String = "Sessions.Base(loaded_theories = " + loaded_theories.size + ", used_theories = " + used_theories.length + ")" 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 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 } sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) { override def toString: String = "Sessions.Deps(" + sessions_structure + ")" def is_empty: Boolean = session_bases.isEmpty def apply(name: String): Base = session_bases(name) def get(name: String): Option[Base] = session_bases.get(name) def imported_sources(name: String): List[SHA1.Digest] = session_bases(name).imported_sources.map(_._2) def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2) 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.pos) ).toList def check_errors: Deps = errors match { case Nil => this case errs => error(cat_lines(errs)) } } def deps(sessions_structure: Structure, progress: Progress = new Progress, inlined_files: Boolean = false, verbose: 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 = (Map("" -> sessions_structure.bootstrap) /: sessions_structure.imports_topological_order)({ case (session_bases, session_name) => progress.expose_interrupt() val info = sessions_structure(session_name) try { val deps_base = info.deps_base(session_bases) val resources = new Resources(sessions_structure, deps_base) if (verbose || list_files) { val groups = if (info.groups.isEmpty) "" else info.groups.mkString(" (", " ", ")") progress.echo("Session " + info.chapter_session + groups) } val dependencies = resources.session_dependencies(info) val overall_syntax = dependencies.overall_syntax val session_theories = dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name) val theory_files = dependencies.theories.map(_.path) dependencies.load_commands 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 loaded_files = load_commands.map({ case (name, spans) => dependencies.loaded_files(name, spans) }) val session_files = (theory_files ::: loaded_files.flatMap(_._2) ::: info.document_files.map(file => info.dir + file._1 + file._2)).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 = deps_base.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 => deps_base.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 = (Graph_Display.empty_graph /: required_subgraph.topological_order)( { case (g, session) => val a = session_node(session) val bs = required_subgraph.imm_preds(session).toList.map(session_node) ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) (graph0 /: dependencies.entries)( { case (g, entry) => val a = node(entry.name) val bs = entry.header.imports.map(node).filterNot(_ == a) ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) } val known_theories = (deps_base.known_theories /: dependencies.entries.iterator.map(entry => entry.name.theory -> entry))(_ + _) 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 = deps_base.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 parent_sessions = if (sessions_structure.build_graph.defined(session_name)) { sessions_structure.build_requirements(List(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 = deps_base.theory_qualifier(name) if (session_theories.contains(name)) { err("Redundant document theory from this session:") } else if (parent_sessions.contains(qualifier)) None else if (dependencies.theories.contains(name)) None else err("Document theory from other session not imported properly:") } }) 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 <- session_theories.iterator path = name.master_dir_path 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 <- session_theories.iterator name1 <- resources.find_theory_node(name.theory) if name.node != name1.node } yield "Incoherent theory file import:\n " + name.path + " vs. \n " + name1.path) .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 = try { info.bibtex_entries; Nil } catch { case ERROR(msg) => List(msg) } val base = Base( pos = info.pos, session_directories = sessions_structure.session_directories, global_theories = sessions_structure.global_theories, session_theories = session_theories, document_theories = document_theories, loaded_theories = dependencies.loaded_theories, used_theories = dependencies.theories_adjunct, load_commands = load_commands.toMap, known_theories = known_theories, known_loaded_files = known_loaded_files, overall_syntax = overall_syntax, imported_sources = check_sources(imported_files), 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 + (info.name -> base) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in session " + quote(info.name) + Position.here(info.pos)) } }) Deps(sessions_structure, session_bases) } /* base info */ sealed case class Base_Info( session: String, sessions_structure: Structure, errors: List[String], base: Base, infos: List[Info]) { def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors)) } def base_info(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): Base_Info = { 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) && base.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( make_info(info.options, 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)))) } } 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) Base_Info(session1, full_sessions1, deps1.errors, deps1(session1), infos1) } /* cumulative session info */ 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, 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])], meta_digest: SHA1.Digest) { def chapter_session: String = chapter + "/" + name 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 = (parent_base.known_theories /: (for { base <- imports_bases.iterator (_, entry) <- base.known_theories.iterator } yield (entry.name.theory -> entry)))(_ + _), known_loaded_files = (parent_base.known_loaded_files /: imports_bases.iterator.map(_.known_loaded_files))(_ ++ _)) } def dirs: List[Path] = dir :: directories 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 case doc => error("Bad document specification " + quote(doc)) } def document_variants: List[Presentation.Document_Variant] = { val variants = Library.space_explode(':', options.string("document_variants")). map(Presentation.Document_Variant.parse) val dups = Library.duplicates(variants.map(_.name)) if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups)) variants } def documents: List[Presentation.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: List[Text.Info[String]] = (for { (document_dir, file) <- document_files.iterator if Bibtex.is_bibtex(file.file_name) info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator } yield info).toList 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 make_info(options: Options, dir_selected: Boolean, dir: Path, chapter: String, entry: Session_Entry): Info = { try { val name = entry.name if (exclude_session(name)) 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_path = dir + Path.explode(entry.path) val directories = entry.directories.map(dir => session_path + Path.explode(dir)) val session_options = options ++ entry.options val theories = entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map({ case ((thy, pos), _) => if (exclude_theory(thy)) error("Bad theory name " + quote(thy) + 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, entry.document_files) .toString) Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path, entry.parent, entry.description, directories, session_options, entry.imports, theories, global_theories, entry.document_theories, document_files, export_files, meta_digest) } catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session entry " + quote(entry.name) + Position.here(entry.pos)) } } 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(Nil) def make(infos: List[Info]): Structure = { def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[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 /: graph.iterator) { case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _)) } } val info_graph = (Graph.string[Info] /: infos) { 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) } val build_graph = add_edges(info_graph, "parent", _.parent) val imports_graph = add_edges(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] = (Map.empty[JFile, String] /: (for { session <- imports_graph.topological_order.iterator info = info_graph.get_node(session) dir <- info.dirs.iterator } yield (info, dir)))({ 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] = (Thy_Header.bootstrap_global_theories.toMap /: (for { session <- imports_graph.topological_order.iterator info = info_graph.get_node(session) thy <- info.global_theories.iterator } yield (info, thy)))({ 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( session_positions, session_directories, global_theories, build_graph, imports_graph) } } final class Structure private[Sessions]( 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 bootstrap: Base = Base( session_directories = session_directories, global_theories = global_theories, overall_syntax = Thy_Header.bootstrap_syntax) def dest_session_directories: List[(String, String)] = for ((file, session) <- session_directories.toList) yield (File.standard_path(file), session) lazy val chapters: SortedMap[String, List[Info]] = (SortedMap.empty[String, List[Info]] /: build_graph.iterator)( { case (chs, (_, (info, _))) => chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) }) 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 check_sessions(names: List[String]) { 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) || graph.get_node(name).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 imports_graph.get_node(name).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( 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, verbose: Boolean = false): Deps = { val deps = Sessions.deps(sessions_structure.selection(selection), progress = progress, inlined_files = inlined_files, verbose = verbose) if (loading_sessions) { val selection_size = deps.sessions_structure.build_graph.size if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...") } deps } def hierarchy(session: String): List[String] = build_graph.all_preds(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 def bibtex_entries: List[(String, List[String])] = build_topological_order.flatMap(name => apply(name).bibtex_entries match { case Nil => None case entries => Some(name -> entries.map(_.info)) }) def session_chapters: List[(String, String)] = imports_topological_order.map(name => name -> apply(name).chapter) override def toString: String = imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")") } /* parser */ private val CHAPTER = "chapter" private val SESSION = "session" private val IN = "in" 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" val root_syntax: Outer_Syntax = Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN + (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) 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], 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])]) 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) } private object Parser extends Options.Parser { private val chapter: Parser[Chapter] = { val chapter_name = atom("chapter name", _.is_name) command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) } } private val session_entry: Parser[Session_Entry] = { val option = option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) } val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]") 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 in_path = $$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x } val document_theories = $$$(DOCUMENT_THEORIES) ~! rep1(position(name)) ^^ { case _ ~ x => x } val document_files = $$$(DOCUMENT_FILES) ~! ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) } val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0) val export_files = $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^ { case _ ~ (x ~ y ~ z) => (x, y, z) } command(SESSION) ~! (position(session_name) ~ (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~ (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~ ($$$("=") ~! (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~ (($$$(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)))) ^^ { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l))) => Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l) } } def parse_root(path: Path): List[Entry] = { 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, _) => 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[Info] = { var entry_chapter = UNSORTED val infos = new mutable.ListBuffer[Info] parse_root(path).foreach { case Chapter(name) => entry_chapter = name case entry: Session_Entry => infos += make_info(options, select, path.dir, 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 */ private def is_session_dir(dir: Path): Boolean = (dir + ROOT).is_file || (dir + ROOTS).is_file private def check_session_dir(dir: Path): Path = if (is_session_dir(dir)) File.pwd() + dir.expand else error("Bad session root directory: " + dir.toString) def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = { val default_dirs = Isabelle_System.components().filter(is_session_dir) for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) } yield (select, dir.canonical) } def load_structure(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, infos: List[Info] = Nil): Structure = { def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] = load_root(select, dir) ::: load_roots(select, dir) def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] = { val root = dir + ROOT if (root.is_file) List((select, root)) else Nil } def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] = { 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 roots = for { (select, dir) <- directories(dirs, select_dirs) res <- load_dir(select, check_session_dir(dir)) } yield res val unique_roots = ((Map.empty[JFile, (Boolean, Path)] /: roots) { case (m, (select, path)) => val file = path.canonical_file m.get(file) match { case None => m + (file -> (select, path)) case Some((select1, path1)) => m + (file -> (select1 || select, path1)) } }).toList.map(_._2) Structure.make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos) } /* 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 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 -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), "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) for (name <- sessions_structure.imports_topological_order) { Output.writeln(name, stdout = true) } }) /** heap file with SHA1 digest **/ private val sha1_prefix = "SHA1:" def read_heap_digest(heap: Path): Option[String] = { if (heap.is_file) { using(FileChannel.open(heap.file.toPath, StandardOpenOption.READ))(file => { val len = file.size val n = sha1_prefix.length + SHA1.digest_length if (len >= n) { file.position(len - n) val buf = ByteBuffer.allocate(n) var i = 0 var m = 0 do { m = file.read(buf) if (m != -1) i += m } while (m != -1 && n > i) if (i == n) { val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset) val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset) if (prefix == sha1_prefix) Some(s) else None } else None } else None }) } else None } def write_heap_digest(heap: Path): String = read_heap_digest(heap) match { case None => val s = SHA1.digest(heap).rep File.append(heap, sha1_prefix + s) s case Some(s) => s } /** persistent store **/ object Session_Info { val session_name = SQL.Column.string("session_name").make_primary_key // Build_Log.Session_Info val session_timing = SQL.Column.bytes("session_timing") val command_timings = SQL.Column.bytes("command_timings") val theory_timings = SQL.Column.bytes("theory_timings") val ml_statistics = SQL.Column.bytes("ml_statistics") val task_statistics = SQL.Column.bytes("task_statistics") val errors = SQL.Column.bytes("errors") val build_log_columns = List(session_name, session_timing, command_timings, theory_timings, ml_statistics, task_statistics, errors) // Build.Session_Info val sources = SQL.Column.string("sources") val input_heaps = SQL.Column.string("input_heaps") val output_heap = SQL.Column.string("output_heap") val return_code = SQL.Column.int("return_code") val build_columns = List(sources, input_heaps, output_heap, return_code) val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) } class Database_Context private[Sessions]( val store: Sessions.Store, database_server: Option[SQL.Database]) extends AutoCloseable { def xml_cache: XML.Cache = store.xml_cache def xz_cache: XZ.Cache = store.xz_cache def close { database_server.foreach(_.close) } def output_database[A](session: String)(f: SQL.Database => A): A = database_server match { case Some(db) => f(db) case None => using(store.open_database(session, output = true))(f) } def input_database[A](session: String)(f: (SQL.Database, String) => Option[A]): Option[A] = database_server match { case Some(db) => f(db, session) case None => store.try_open_database(session) match { case Some(db) => using(db)(f(_, session)) case None => None } } def read_export( sessions: List[String], theory_name: String, name: String): Option[Export.Entry] = { val attempts = database_server match { case Some(db) => sessions.view.map(session_name => Export.read_entry(db, store.xz_cache, session_name, theory_name, name)) case None => sessions.view.map(session_name => store.try_open_database(session_name) match { case Some(db) => using(db)(Export.read_entry(_, store.xz_cache, session_name, theory_name, name)) case None => None }) } attempts.collectFirst({ case Some(entry) => entry }) } def get_export( session_hierarchy: List[String], theory_name: String, name: String): Export.Entry = read_export(session_hierarchy, theory_name, name) getOrElse Export.empty_entry(theory_name, name) override def toString: String = { val s = database_server match { case Some(db) => db.toString case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ") } "Database_Context(" + s + ")" } } - def store(options: Options): Store = new Store(options) + def store(options: Options, + xml_cache: XML.Cache = XML.Cache.make(), + xz_cache: XZ.Cache = XZ.Cache.make()): Store = + new Store(options, xml_cache, xz_cache) - class Store private[Sessions](val options: Options) + class Store private[Sessions]( + val options: Options, + val xml_cache: XML.Cache, + val xz_cache: XZ.Cache) { store => override def toString: String = "Store(output_dir = " + output_dir.absolute + ")" - val xml_cache: XML.Cache = XML.make_cache() - val xz_cache: XZ.Cache = XZ.make_cache() - /* directories */ val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER") val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER") def system_heaps: Boolean = options.bool("system_heaps") val output_dir: Path = if (system_heaps) system_output_dir else user_output_dir val input_dirs: List[Path] = if (system_heaps) List(system_output_dir) else List(user_output_dir, system_output_dir) def presentation_dir: Path = if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM") else Path.explode("$ISABELLE_BROWSER_INFO") /* file names */ def heap(name: String): Path = Path.basic(name) def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db") def log(name: String): Path = Path.basic("log") + Path.basic(name) def log_gz(name: String): Path = log(name).ext("gz") def output_heap(name: String): Path = output_dir + heap(name) def output_database(name: String): Path = output_dir + database(name) def output_log(name: String): Path = output_dir + log(name) def output_log_gz(name: String): Path = output_dir + log_gz(name) def prepare_output_dir() { Isabelle_System.make_directory(output_dir + Path.basic("log")) } /* heap */ def find_heap(name: String): Option[Path] = input_dirs.map(_ + heap(name)).find(_.is_file) def find_heap_digest(name: String): Option[String] = find_heap(name).flatMap(read_heap_digest) def the_heap(name: String): Path = find_heap(name) getOrElse error("Missing heap image for session " + quote(name) + " -- expected in:\n" + cat_lines(input_dirs.map(dir => " " + dir.expand.implode))) /* database */ def database_server: Boolean = options.bool("build_database_server") def open_database_server(): SQL.Database = PostgreSQL.open_database( user = options.string("build_database_user"), password = options.string("build_database_password"), database = options.string("build_database_name"), host = options.string("build_database_host"), port = options.int("build_database_port"), ssh = options.proper_string("build_database_ssh_host").map(ssh_host => SSH.open_session(options, host = ssh_host, user = options.string("build_database_ssh_user"), port = options.int("build_database_ssh_port"))), ssh_close = true) def open_database_context(): Database_Context = new Database_Context(store, if (database_server) Some(open_database_server()) else None) def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] = { def check(db: SQL.Database): Option[SQL.Database] = if (output || session_info_exists(db)) Some(db) else { db.close; None } if (database_server) check(open_database_server()) else if (output) Some(SQLite.open_database(output_database(name))) else { (for { dir <- input_dirs.view path = dir + database(name) if path.is_file db <- check(SQLite.open_database(path)) } yield db).headOption } } def open_database(name: String, output: Boolean = false): SQL.Database = try_open_database(name, output = output) getOrElse error("Missing build database for session " + quote(name)) def clean_output(name: String): (Boolean, Boolean) = { val relevant_db = database_server && { try_open_database(name) match { case Some(db) => try { db.transaction { val relevant_db = session_info_defined(db, name) init_session_info(db, name) relevant_db } } finally { db.close } case None => false } } val del = for { dir <- (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir)) file <- List(heap(name), database(name), log(name), log_gz(name)) path = dir + file if path.is_file } yield path.file.delete val relevant = relevant_db || del.nonEmpty val ok = del.forall(b => b) (relevant, ok) } /* SQL database content */ def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = db.using_statement(Session_Info.table.select(List(column), Session_Info.session_name.where_equal(name)))(stmt => { val res = stmt.execute_query() if (!res.next()) Bytes.empty else res.bytes(column) }) def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] = Properties.uncompress( - read_bytes(db, name, column), cache = xz_cache, xml_cache = Some(xml_cache)) + read_bytes(db, name, column), cache = xz_cache, xml_cache = xml_cache) /* session info */ def init_session_info(db: SQL.Database, name: String) { db.transaction { db.create_table(Session_Info.table) db.using_statement( Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute) db.create_table(Export.Data.table) db.using_statement( Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute) db.create_table(Presentation.Data.table) db.using_statement( Presentation.Data.table.delete( Presentation.Data.session_name.where_equal(name)))(_.execute) } } def session_info_exists(db: SQL.Database): Boolean = { val tables = db.tables tables.contains(Session_Info.table.name) && tables.contains(Export.Data.table.name) } def session_info_defined(db: SQL.Database, name: String): Boolean = db.transaction { session_info_exists(db) && { db.using_statement( Session_Info.table.select(List(Session_Info.session_name), Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next()) } } def write_session_info( db: SQL.Database, name: String, build_log: Build_Log.Session_Info, build: Build.Session_Info) { db.transaction { db.using_statement(Session_Info.table.insert())(stmt => { stmt.string(1) = name stmt.bytes(2) = Properties.encode(build_log.session_timing) stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = xz_cache) stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = xz_cache) stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = xz_cache) stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = xz_cache) stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = xz_cache) stmt.string(8) = build.sources stmt.string(9) = cat_lines(build.input_heaps) stmt.string(10) = build.output_heap getOrElse "" stmt.int(11) = build.return_code stmt.execute() }) } } def read_session_timing(db: SQL.Database, name: String): Properties.T = - Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache)) + Properties.decode(read_bytes(db, name, Session_Info.session_timing), xml_cache = xml_cache) def read_command_timings(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.command_timings) def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.theory_timings) def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.ml_statistics) def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.task_statistics) def read_theories(db: SQL.Database, name: String): List[String] = read_theory_timings(db, name).flatMap(Markup.Name.unapply) def read_errors(db: SQL.Database, name: String): List[String] = Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = xz_cache) def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = { if (db.tables.contains(Session_Info.table.name)) { db.using_statement(Session_Info.table.select(Session_Info.build_columns, Session_Info.session_name.where_equal(name)))(stmt => { val res = stmt.execute_query() if (!res.next()) None else { Some( Build.Session_Info( res.string(Session_Info.sources), split_lines(res.string(Session_Info.input_heaps)), res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) }, res.int(Session_Info.return_code))) } }) } else None } } } diff --git a/src/Pure/term.scala b/src/Pure/term.scala --- a/src/Pure/term.scala +++ b/src/Pure/term.scala @@ -1,228 +1,242 @@ /* Title: Pure/term.scala Author: Makarius Lambda terms, types, sorts. Note: Isabelle/ML is the primary environment for logical operations. */ package isabelle object Term { /* types and terms */ sealed case class Indexname(name: String, index: Int = 0) { override def toString: String = if (index == -1) name else { val dot = Symbol.explode(name).reverse match { case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false case c :: _ => Symbol.is_digit(c) case _ => true } if (dot) "?" + name + "." + index else if (index != 0) "?" + name + index else "?" + name } } type Class = String type Sort = List[Class] sealed abstract class Typ case class Type(name: String, args: List[Typ] = Nil) extends Typ { override def toString: String = if (this == dummyT) "_" else "Type(" + name + (if (args.isEmpty) "" else "," + args) + ")" } case class TFree(name: String, sort: Sort = Nil) extends Typ { override def toString: String = "TFree(" + name + (if (sort.isEmpty) "" else "," + sort) + ")" } case class TVar(name: Indexname, sort: Sort = Nil) extends Typ { override def toString: String = "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")" } val dummyT: Type = Type("dummy") sealed abstract class Term { def head: Term = this match { case App(fun, _) => fun.head case _ => this } } case class Const(name: String, typargs: List[Typ] = Nil) extends Term { override def toString: String = if (this == dummy) "_" else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")" } case class Free(name: String, typ: Typ = dummyT) extends Term { override def toString: String = "Free(" + name + (if (typ == dummyT) "" else "," + typ) + ")" } case class Var(name: Indexname, typ: Typ = dummyT) extends Term { override def toString: String = "Var(" + name + (if (typ == dummyT) "" else "," + typ) + ")" } case class Bound(index: Int) extends Term case class Abs(name: String, typ: Typ, body: Term) extends Term case class App(fun: Term, arg: Term) extends Term { override def toString: String = this match { case OFCLASS(ty, c) => "OFCLASS(" + ty + "," + c + ")" case _ => "App(" + fun + "," + arg + ")" } } def dummy_pattern(ty: Typ): Term = Const("Pure.dummy_pattern", List(ty)) val dummy: Term = dummy_pattern(dummyT) sealed abstract class Proof case object MinProof extends Proof case class PBound(index: Int) extends Proof case class Abst(name: String, typ: Typ, body: Proof) extends Proof case class AbsP(name: String, hyp: Term, body: Proof) extends Proof case class Appt(fun: Proof, arg: Term) extends Proof case class AppP(fun: Proof, arg: Proof) extends Proof case class Hyp(hyp: Term) extends Proof case class PAxm(name: String, types: List[Typ]) extends Proof case class PClass(typ: Typ, cls: Class) extends Proof case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof /* type classes within the logic */ object Class_Const { val suffix = "_class" def apply(c: Class): String = c + suffix def unapply(s: String): Option[Class] = if (s.endsWith(suffix)) Some(s.substring(0, s.length - suffix.length)) else None } object OFCLASS { def apply(ty: Typ, s: Sort): List[Term] = s.map(c => apply(ty, c)) def apply(ty: Typ, c: Class): Term = App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty))) def unapply(t: Term): Option[(Typ, String)] = t match { case App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty1))) if ty == ty1 => Some((ty, c)) case _ => None } } /** cache **/ - def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache = - new Cache(initial_size, max_string) + object Cache + { + def make( + max_string: Int = Integer.MAX_VALUE, + initial_size: Int = isabelle.Cache.default_initial_size): Cache = + new Cache(initial_size, max_string) - class Cache private[Term](initial_size: Int, max_string: Int) - extends isabelle.Cache(initial_size, max_string) + val none: Cache = make(max_string = 0) + } + + class Cache private[Term](max_string: Int, initial_size: Int) + extends isabelle.Cache(max_string = max_string, initial_size = initial_size) { protected def cache_indexname(x: Indexname): Indexname = lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index)) protected def cache_sort(x: Sort): Sort = - if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string)) + if (x.isEmpty) Nil + else lookup(x) getOrElse store(x.map(cache_string)) protected def cache_typ(x: Typ): Typ = { if (x == dummyT) dummyT else lookup(x) match { case Some(y) => y case None => x match { case Type(name, args) => store(Type(cache_string(name), cache_typs(args))) case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort))) case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort))) } } } protected def cache_typs(x: List[Typ]): List[Typ] = { if (x.isEmpty) Nil else { lookup(x) match { case Some(y) => y case None => store(x.map(cache_typ)) } } } protected def cache_term(x: Term): Term = { lookup(x) match { case Some(y) => y case None => x match { case Const(name, typargs) => store(Const(cache_string(name), cache_typs(typargs))) case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ))) case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ))) case Bound(_) => store(x) case Abs(name, typ, body) => store(Abs(cache_string(name), cache_typ(typ), cache_term(body))) case App(fun, arg) => store(App(cache_term(fun), cache_term(arg))) } } } protected def cache_proof(x: Proof): Proof = { if (x == MinProof) MinProof else { lookup(x) match { case Some(y) => y case None => (x: @unchecked) match { case PBound(_) => store(x) case Abst(name, typ, body) => store(Abst(cache_string(name), cache_typ(typ), cache_proof(body))) case AbsP(name, hyp, body) => store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body))) case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg))) case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg))) case Hyp(hyp) => store(Hyp(cache_term(hyp))) case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types))) case PClass(typ, cls) => store(PClass(cache_typ(typ), cache_string(cls))) case Oracle(name, prop, types) => store(Oracle(cache_string(name), cache_term(prop), cache_typs(types))) case PThm(serial, theory_name, name, types) => store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types))) } } } } // main methods - def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) } - def sort(x: Sort): Sort = synchronized { cache_sort(x) } - def typ(x: Typ): Typ = synchronized { cache_typ(x) } - def term(x: Term): Term = synchronized { cache_term(x) } - def proof(x: Proof): Proof = synchronized { cache_proof(x) } + def indexname(x: Indexname): Indexname = + if (no_cache) x else synchronized { cache_indexname(x) } + def sort(x: Sort): Sort = + if (no_cache) x else synchronized { cache_sort(x) } + def typ(x: Typ): Typ = + if (no_cache) x else synchronized { cache_typ(x) } + def term(x: Term): Term = + if (no_cache) x else synchronized { cache_term(x) } + def proof(x: Proof): Proof = + if (no_cache) x else synchronized { cache_proof(x) } def position(x: Position.T): Position.T = - synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } + if (no_cache) x + else synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } } }