# HG changeset patch # User paulson # Date 1698934216 0 # Node ID c1bd24ca22b6e4e8708384220e9cae884b839806 # Parent 9ce8bf038444c5660fe8f28be194d948311723f0# Parent fb6828831ef1bc1c57ede4624ef08f02bd076f6b merged diff -r fb6828831ef1 -r c1bd24ca22b6 src/Pure/Admin/build_log.scala --- 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) { diff -r fb6828831ef1 -r c1bd24ca22b6 src/Pure/Admin/isabelle_cronjob.scala --- 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( diff -r fb6828831ef1 -r c1bd24ca22b6 src/Pure/System/progress.scala --- 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 })