# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1720623884 -7200
# Node ID 17786f08b93e80ea89e9435d8b1026ba1791a03a
# Parent  77c78910544cbd14e3f353d1ab17b08334448548
allow updating reports via build_manager_database tool, e.g. to generate hg logs/diffs;

diff -r 77c78910544c -r 17786f08b93e src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Wed Jul 10 17:01:51 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Wed Jul 10 17:04:44 2024 +0200
@@ -1622,7 +1622,12 @@
 
   /** restore build manager database **/
 
-  def build_manager_database(options: Options, progress: Progress = new Progress): Unit = {
+  def build_manager_database(
+    options: Options,
+    sync_dirs: List[Sync.Dir] = Sync.afp_dirs(),
+    update_reports: Boolean = false,
+    progress: Progress = new Progress
+  ): Unit = {
     val store = Store(options)
     using(store.open_database()) { db =>
       db.transaction {
@@ -1634,16 +1639,44 @@
         }
       }
 
-      val results =
+      val reports =
         for {
           kind <- File.read_dir(store.finished)
           entry <- File.read_dir(store.finished + Path.basic(kind))
           id <- Value.Long.unapply(entry)
           report = store.report(kind, id)
           if report.ok
-        } yield report.result(None)
+        } yield report
+
+      val results = reports.map(report => report -> report.result(None))
+
+      if (update_reports) {
+        val isabelle_repository = Mercurial.self_repository()
+        val afp_repository =
+          sync_dirs.find(_.name == Component.AFP).getOrElse(error("Missing AFP for udpate")).hg
+
+        isabelle_repository.pull()
+        afp_repository.pull()
 
-      val state = State(finished = results.map(result => result.name -> result).toMap)
+        for ((kind, results0) <- results.groupBy(_._1.kind) if kind != User_Build.name) {
+          val results1 = results0.sortBy(_._1.id)
+          results1.foldLeft(("", "")) {
+            case ((isabelle_rev0, afp_rev0), (report, result)) =>
+              val isabelle_rev = result.isabelle_version.getOrElse("")
+              val afp_rev = result.afp_version.getOrElse("")
+
+              report.write_log(Component.Isabelle, isabelle_repository, isabelle_rev0, isabelle_rev)
+              report.write_log(Component.AFP, afp_repository, afp_rev0, afp_rev)
+              report.write_diff(
+                Component.Isabelle, isabelle_repository, isabelle_rev0, isabelle_rev)
+              report.write_diff(Component.AFP, afp_repository, afp_rev0, afp_rev)
+
+              (isabelle_rev, afp_rev)
+          }
+        }
+      }
+
+      val state = State(finished = results.map((_, result) => result.name -> result).toMap)
 
       Build_Manager.private_data.transaction_lock(db,
         create = true, label = "Build_Manager.build_manager_database") {
@@ -1661,24 +1694,31 @@
     "restore build_manager database from log files",
     Scala_Project.here,
     { args =>
+      var afp_root: Option[Path] = None
       var options = Options.init()
+      var update_reports = false
 
       val getopts = Getopts("""
 Usage: isabelle build_manager_database [OPTIONS]
 
   Options are:
+    -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -u           update reports
 
   Restore build_manager database from log files.
 """,
-        "o:" -> (arg => options = options + arg))
+        "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
+        "o:" -> (arg => options = options + arg),
+        "u" -> (_ => update_reports = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = new Console_Progress()
 
-      build_manager_database(options, progress = progress)
+      build_manager_database(options, sync_dirs = Sync.afp_dirs(afp_root),
+        update_reports = update_reports, progress = progress)
     })