--- a/src/Pure/Admin/build_log.scala Thu Nov 02 14:10:08 2023 +0000
+++ b/src/Pure/Admin/build_log.scala Thu Nov 02 14:10:16 2023 +0000
@@ -1070,23 +1070,31 @@
val consumer =
Consumer_Thread.fork[Log_File]("build_log_database")(
+ limit = 1,
consume = { log_file =>
+ val t0 = progress.start.time
+ val t1 = progress.now().time
+
private_data.transaction_lock(db, label = "build_log_database") {
try { status.foreach(_.update(log_file)) }
catch { case exn: Throwable => add_error(log_file.name, exn) }
}
+
+ val t2 = progress.now().time
+
+ progress.echo(verbose = true, msg =
+ "Log " + quote(log_file.name) + " (" +
+ (t1 - t0).message_hms + " start time, " +
+ (t2 - t1).message + " elapsed time)")
+
true
- },
- limit = 1
- )
+ })
try {
for (file <- files.iterator if status.exists(_.required(file))) {
- val log_name = Log_File.plain_name(file)
- progress.echo("Log " + quote(log_name), verbose = true)
Exn.result { Log_File.read(file, cache = cache.compress) } match {
case Exn.Res(log_file) => consumer.send(log_file)
- case Exn.Exn(exn) => add_error(log_name, exn)
+ case Exn.Exn(exn) => add_error(Log_File.plain_name(file), exn)
}
}
}
@@ -1198,14 +1206,8 @@
if (vacuum) db.vacuum()
progress.echo("Updating database " + db + " ...")
- val errors0 = store.write_info(db, log_files, progress = progress)
-
val errors =
- if (ml_statistics) {
- progress.echo("Updating database " + db + " (ML statistics) ...")
- store.write_info(db, log_files, ml_statistics = true, errors = errors0)
- }
- else errors0
+ store.write_info(db, log_files, ml_statistics = ml_statistics, progress = progress)
if (errors.isEmpty) {
for (path <- snapshot) {
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Nov 02 14:10:08 2023 +0000
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Nov 02 14:10:16 2023 +0000
@@ -19,6 +19,7 @@
val main_dir: Path = Path.explode("~/cronjob")
val main_state_file: Path = main_dir + Path.explode("run/main.state")
val build_release_log: Path = main_dir + Path.explode("run/build_release.log")
+ val build_log_database_log: Path = main_dir + Path.explode("run/build_log_database.log")
val current_log: Path = main_dir + Path.explode("run/main.log") // owned by log service
val cumulative_log: Path = main_dir + Path.explode("log/main.log") // owned by log service
@@ -368,7 +369,7 @@
" -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
" -e ISABELLE_SWIPL=/usr/local/bin/swipl",
args = "-a -d '~~/src/Benchmarks'")),
- List(remote_build_studio1, remote_build_studio1),
+ List(remote_build_studio1),
List(
Remote_Build("macOS, quick_and_dirty", "mini2",
options = "-m32 -M4 -t quick_and_dirty -p pide_session=false",
@@ -379,7 +380,7 @@
options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"),
active = () => false)),
- List(remote_build_mini3, remote_build_mini3, remote_build_mini3),
+ List(remote_build_mini3),
List(
Remote_Build("Windows", "vmnipkow9", historic = true, history = 90,
components_base = "/cygdrive/d/isatest/contrib",
@@ -626,6 +627,8 @@
val main_start_date = Date.now()
File.write(main_state_file, main_start_date.toString + " " + log_service.hostname)
+ val build_log_database_progress = new File_Progress(build_log_database_log, verbose = true)
+
run(main_start_date,
Logger_Task("isabelle_cronjob", logger =>
run_now(
@@ -638,6 +641,7 @@
Logger_Task("build_log_database",
logger =>
Build_Log.build_log_database(logger.options, build_log_dirs,
+ progress = build_log_database_progress,
vacuum = true, ml_statistics = true,
snapshot = Some(isabelle_devel + Path.explode("build_log.db")))))),
PAR(
--- a/src/Pure/System/progress.scala Thu Nov 02 14:10:08 2023 +0000
+++ b/src/Pure/System/progress.scala Thu Nov 02 14:10:16 2023 +0000
@@ -182,6 +182,9 @@
}
class Progress {
+ def now(): Date = Date.now()
+ val start: Date = now()
+
def verbose: Boolean = false
final def do_output(message: Progress.Message): Boolean = !message.verbose || verbose
@@ -243,18 +246,20 @@
class Console_Progress(override val verbose: Boolean = false, stderr: Boolean = false)
extends Progress {
- override def output(message: Progress.Message): Unit =
+ override def output(message: Progress.Message): Unit = synchronized {
if (do_output(message)) {
Output.output(message.output_text, stdout = !stderr, include_empty = true)
}
+ }
override def toString: String = super.toString + ": console"
}
class File_Progress(path: Path, override val verbose: Boolean = false)
extends Progress {
- override def output(message: Progress.Message): Unit =
+ override def output(message: Progress.Message): Unit = synchronized {
if (do_output(message)) File.append(path, message.output_text + "\n")
+ }
override def toString: String = super.toString + ": " + path.toString
}
@@ -274,6 +279,9 @@
extends Progress {
database_progress =>
+ override def now(): Date = db.now()
+ override val start: Date = now()
+
if (UUID.unapply(context_uuid).isEmpty) {
error("Bad Database_Progress.context_uuid: " + quote(context_uuid))
}
@@ -305,7 +313,6 @@
val java = ProcessHandle.current()
val java_pid = java.pid
val java_start = Date.instant(java.info.startInstant.get)
- val now = db.now()
stmt.string(1) = _agent_uuid
stmt.string(2) = context_uuid
@@ -313,8 +320,8 @@
stmt.string(4) = hostname
stmt.long(5) = java_pid
stmt.date(6) = java_start
- stmt.date(7) = now
- stmt.date(8) = now
+ stmt.date(7) = start
+ stmt.date(8) = start
stmt.date(9) = None
stmt.long(10) = 0L
})