# HG changeset patch # User wenzelm # Date 1489778461 -3600 # Node ID 57c85c83c11bb9cb9b05700e85c14cc1c7064199 # Parent 6c1d7d5c2165cf2bba532df21769e956f0f2deec maintain persistent session info in SQLite database instead of log file; diff -r 6c1d7d5c2165 -r 57c85c83c11b src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Mar 17 19:14:11 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Fri Mar 17 20:21:01 2017 +0100 @@ -550,15 +550,19 @@ map(xml_cache.props(_)) } - def read_bytes(db: SQLite.Database, table: SQL.Table, column: SQL.Column): Bytes = - { + def read_string(db: SQLite.Database, table: SQL.Table, column: SQL.Column): String = using(db.select_statement(table, List(column)))(stmt => { val rs = stmt.executeQuery - if (!rs.next) Bytes.empty - else db.bytes(rs, column.name) + if (!rs.next) "" else db.string(rs, column.name) }) - } + + def read_bytes(db: SQLite.Database, table: SQL.Table, column: SQL.Column): Bytes = + using(db.select_statement(table, List(column)))(stmt => + { + val rs = stmt.executeQuery + if (!rs.next) Bytes.empty else db.bytes(rs, column.name) + }) def read_properties(db: SQLite.Database, table: SQL.Table, column: SQL.Column) : List[Properties.T] = uncompress_properties(read_bytes(db, table, column)) @@ -586,19 +590,13 @@ output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident) } - def find(name: String): Option[(Path, Option[String])] = - input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir => - (dir + log_gz(name), read_heap_digest(dir + Path.basic(name)))) + def find_database_heap(name: String): Option[(Path, Option[String])] = + input_dirs.find(dir => (dir + database(name)).is_file).map(dir => + (dir + database(name), read_heap_digest(dir + Path.basic(name)))) def find_database(name: String): Option[Path] = input_dirs.map(_ + database(name)).find(_.is_file) - def find_log(name: String): Option[Path] = - input_dirs.map(_ + log(name)).find(_.is_file) - - def find_log_gz(name: String): Option[Path] = - input_dirs.map(_ + log_gz(name)).find(_.is_file) - def heap(name: String): Path = input_dirs.map(_ + Path.basic(name)).find(_.is_file) getOrElse error("Unknown logic " + quote(name) + " -- no heap file found in:\n" + @@ -648,7 +646,7 @@ db.set_bytes(stmt, 5, store.compress_properties(build_log.task_statistics)) db.set_string(stmt, 6, cat_lines(build.sources)) db.set_string(stmt, 7, cat_lines(build.input_heaps)) - db.set_string(stmt, 8, build.output_heap) + db.set_string(stmt, 8, build.output_heap getOrElse "") db.set_int(stmt, 9, build.return_code) stmt.execute() }) @@ -667,21 +665,23 @@ def read_task_statistics(store: Store, db: SQLite.Database): List[Properties.T] = store.read_properties(db, table, task_statistics) - def read_build_log(store: Store, db: SQLite.Database): Option[Build_Log.Session_Info] = - using(db.select_statement(table, build_log_columns))(stmt => - { - val rs = stmt.executeQuery - if (!rs.next) None - else { - Some( - Build_Log.Session_Info( - db.string(rs, session_name.name), - store.decode_properties(db.bytes(rs, session_timing.name)), - store.uncompress_properties(db.bytes(rs, command_timings.name)), - store.uncompress_properties(db.bytes(rs, ml_statistics.name)), - store.uncompress_properties(db.bytes(rs, task_statistics.name)))) - } - }) + def read_build_log(store: Store, db: SQLite.Database, + default_name: String = "", + command_timings: Boolean = false, + ml_statistics: Boolean = false, + task_statistics: Boolean = false): Build_Log.Session_Info = + { + val name = store.read_string(db, table, session_name) + Build_Log.Session_Info( + session_name = + if (name == "") default_name + else if (default_name == "" || default_name == name) name + else error("Database from different session " + quote(name)), + session_timing = read_session_timing(store, db), + command_timings = if (command_timings) read_command_timings(store, db) else Nil, + ml_statistics = if (ml_statistics) read_ml_statistics(store, db) else Nil, + task_statistics = if (task_statistics) read_task_statistics(store, db) else Nil) + } def read_build(store: Store, db: SQLite.Database): Option[Build.Session_Info] = using(db.select_statement(table, table.columns))(stmt => @@ -693,7 +693,7 @@ Build.Session_Info( split_lines(db.string(rs, sources.name)), split_lines(db.string(rs, input_heaps.name)), - db.string(rs, output_heap.name), + db.string(rs, output_heap.name) match { case "" => None case s => Some(s) }, db.int(rs, return_code.name))) } }) diff -r 6c1d7d5c2165 -r 57c85c83c11b src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Mar 17 19:14:11 2017 +0100 +++ b/src/Pure/Tools/build.scala Fri Mar 17 20:21:01 2017 +0100 @@ -21,37 +21,45 @@ { /** auxiliary **/ + /* persistent build info */ + + sealed case class Session_Info( + sources: List[String], + input_heaps: List[String], + output_heap: Option[String], + return_code: Int) + + /* queue with scheduling information */ private object Queue { def load_timings(store: Sessions.Store, name: String): (List[Properties.T], Double) = { - val (path, text) = - store.find_log_gz(name) match { - case Some(path) => (path, File.read_gzip(path)) - case None => - store.find_log(name) match { - case Some(path) => (path, File.read(path)) - case None => (Path.current, "") - } - } + val no_timings: (List[Properties.T], Double) = (Nil, 0.0) - def ignore_error(msg: String): (List[Properties.T], Double) = - { - Output.warning("Ignoring bad log file: " + path + (if (msg == "") "" else "\n" + msg)) - (Nil, 0.0) - } - - try { - val info = Build_Log.Log_File(name, text).parse_session_info(name, command_timings = true) - val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0 - (info.command_timings, session_timing) - } - catch { - case ERROR(msg) => ignore_error(msg) - case exn: java.lang.Error => ignore_error(Exn.message(exn)) - case _: XML.Error => ignore_error("") + store.find_database(name) match { + case None => no_timings + case Some(database) => + def ignore_error(msg: String) = + { + Output.warning("Ignoring bad database: " + database + (if (msg == "") "" else "\n" + msg)) + no_timings + } + try { + using(SQLite.open_database(database))(db => + { + val build_log = + Sessions.Session_Info.read_build_log(store, db, name, command_timings = true) + val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0 + (build_log.command_timings, session_timing) + }) + } + catch { + case ERROR(msg) => ignore_error(msg) + case exn: java.lang.Error => ignore_error(Exn.message(exn)) + case _: XML.Error => ignore_error("") + } } } @@ -60,7 +68,7 @@ val graph = tree.graph val sessions = graph.keys - val timings = Par_List.map((name: String) => (name, load_timings(store, name)), sessions) + val timings = sessions.map(name => (name, load_timings(store, name))) val command_timings = Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil) val session_timing = @@ -231,49 +239,6 @@ } - /* sources and heaps */ - - sealed case class Session_Info( - sources: List[String], input_heaps: List[String], output_heap: String, return_code: Int) - - private val SOURCES = "sources: " - private val INPUT_HEAP = "input_heap: " - private val OUTPUT_HEAP = "output_heap: " - private val LOG_START = "log:" - private val line_prefixes = List(SOURCES, INPUT_HEAP, OUTPUT_HEAP, LOG_START) - - private def sources_stamp(digests: List[SHA1.Digest]): String = - digests.map(_.toString).sorted.mkString(SOURCES, " ", "") - - private def read_stamps(path: Path): Option[(String, List[String], List[String])] = - if (path.is_file) { - val stream = new GZIPInputStream(new BufferedInputStream(new FileInputStream(path.file))) - val reader = new BufferedReader(new InputStreamReader(stream, UTF8.charset)) - val lines = - { - val lines = new mutable.ListBuffer[String] - try { - var finished = false - while (!finished) { - val line = reader.readLine - if (line != null && line_prefixes.exists(line.startsWith(_))) - lines += line - else finished = true - } - } - finally { reader.close } - lines.toList - } - - if (!lines.isEmpty && lines.last.startsWith(LOG_START)) { - lines.find(_.startsWith(SOURCES)).map(s => - (s, lines.filter(_.startsWith(INPUT_HEAP)), lines.filter(_.startsWith(OUTPUT_HEAP)))) - } - else None - } - else None - - /** build with results **/ @@ -356,8 +321,8 @@ val deps = Sessions.dependencies(progress, true, verbose, list_files, check_keywords, selected_tree) - def session_sources_stamp(name: String): String = - sources_stamp(selected_tree(name).meta_digest :: deps.sources(name)) + def sources_stamp(name: String): List[String] = + (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted /* main build process */ @@ -371,7 +336,7 @@ if (clean_build) { for (name <- full_tree.graph.all_succs(selected)) { val files = - List(Path.basic(name), store.log(name), store.log_gz(name)). + List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)). map(store.output_dir + _).filter(_.is_file) if (files.nonEmpty) progress.echo("Cleaning " + name + " ...") if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete") @@ -440,11 +405,7 @@ yield Sessions.write_heap_digest(path) File.write_gzip(store.output_dir + store.log_gz(name), - terminate_lines( - session_sources_stamp(name) :: - input_heaps.map(INPUT_HEAP + _) ::: - heap_stamp.toList.map(OUTPUT_HEAP + _) ::: - List(LOG_START) ::: process_result.out_lines)) + terminate_lines(process_result.out_lines)) heap_stamp } @@ -459,6 +420,22 @@ None } + + // write database + { + val database = store.output_dir + store.database(name) + database.file.delete + + using(SQLite.open_database(database))(db => + Sessions.Session_Info.write(store, db, + build_log = + Build_Log.Log_File(name, process_result.out_lines). + parse_session_info(name, + command_timings = true, ml_statistics = true, task_statistics = true), + build = + Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc))) + } + loop(pending - name, running - name, results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info))) //}}} @@ -473,15 +450,18 @@ val (current, heap_stamp) = { - store.find(name) match { - case Some((log_gz, heap_stamp)) => - read_stamps(log_gz) match { - case Some((sources, input_heaps, output_heaps)) => + store.find_database_heap(name) match { + case Some((database, heap_stamp)) => + using(SQLite.open_database(database))( + Sessions.Session_Info.read_build(store, _)) match + { + case Some(build) => val current = - sources == session_sources_stamp(name) && - input_heaps == ancestor_heaps.map(INPUT_HEAP + _) && - output_heaps == heap_stamp.toList.map(OUTPUT_HEAP + _) && - !(do_output && heap_stamp.isEmpty) + build.sources == sources_stamp(name) && + build.input_heaps == ancestor_heaps && + build.output_heap == heap_stamp && + !(do_output && heap_stamp.isEmpty) && + build.return_code == 0 (current, heap_stamp) case None => (false, None) }