# HG changeset patch
# User wenzelm
# Date 1678045274 -3600
# Node ID 790085b1002f18b55a231e49793fed5a26041db6
# Parent  e3ed231fa2140393ff5348831fd8405899f01bf4
more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;

diff -r e3ed231fa214 -r 790085b1002f src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Mar 05 19:33:01 2023 +0100
+++ b/src/Pure/General/sql.scala	Sun Mar 05 20:41:14 2023 +0100
@@ -321,6 +321,8 @@
 
     def rebuild(): Unit = ()
 
+    def now(): Date
+
 
     /* types */
 
@@ -434,6 +436,8 @@
     override def is_server: Boolean = false
     override def rebuild(): Unit = using_statement("VACUUM")(_.execute())
 
+    override def now(): Date = Date.now()
+
     def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
 
     def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
@@ -507,6 +511,13 @@
     override def toString: String = name
     override def is_server: Boolean = true
 
+    override def now(): Date = {
+      val now = SQL.Column.date("now")
+      using_statement("SELECT NOW() as " + now.ident)(
+        stmt => stmt.execute_query().iterator(_.date(now)).nextOption
+      ).getOrElse(error("Failed to get current date/time from database server " + toString))
+    }
+
     def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_postgresql(T)
 
     // see https://jdbc.postgresql.org/documentation/head/8-date-time.html
diff -r e3ed231fa214 -r 790085b1002f src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Mar 05 19:33:01 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sun Mar 05 20:41:14 2023 +0100
@@ -264,9 +264,13 @@
     }
 
     object Serial {
+      val uuid = Generic.uuid.make_primary_key
+      val stamp = SQL.Column.date("stamp")
       val serial = SQL.Column.long("serial")
 
-      val table = make_table("serial", List(serial))
+      val table = make_table("serial", List(uuid, stamp, serial))
+
+      val serial_max = serial.copy(expr = "MAX(" + serial.ident + ")")
     }
 
     object Progress {
@@ -325,15 +329,21 @@
           List(name, hostname, numa_node, rc, out, err, timing_elapsed, timing_cpu, timing_gc))
     }
 
-    def get_serial(db: SQL.Database): Long =
-      db.using_statement(Serial.table.select())(stmt =>
-        stmt.execute_query().iterator(_.long(Serial.serial)).nextOption.getOrElse(0L))
+    def get_serial(db: SQL.Database, uuid: String = ""): Long =
+      db.using_statement(
+        Serial.table.select(List(Serial.serial_max),
+          sql = SQL.where(Generic.sql_equal(uuid = uuid)))
+      )(stmt => stmt.execute_query().iterator(_.long(Serial.serial)).nextOption.getOrElse(0L))
 
-    def set_serial(db: SQL.Database, serial: Long): Unit =
-      if (get_serial(db) != serial) {
-        db.using_statement(Serial.table.delete())(_.execute())
+    def set_serial(db: SQL.Database, uuid: String, stamp: Date, serial: Long): Unit =
+      if (get_serial(db, uuid = uuid) != serial) {
+        db.using_statement(
+          Serial.table.delete(sql = SQL.where(Generic.sql_equal(uuid = uuid)))
+        )(_.execute())
         db.using_statement(Serial.table.insert()) { stmt =>
-          stmt.long(1) = serial
+          stmt.string(1) = uuid
+          stmt.date(2) = stamp
+          stmt.long(3) = serial
           stmt.execute()
         }
       }
@@ -584,7 +594,7 @@
       val serial0 = get_serial(db)
       val serial = if (changed.exists(identity)) State.inc_serial(serial0) else serial0
 
-      set_serial(db, serial)
+      set_serial(db, uuid, db.now(), serial)
       state.set_serial(serial)
     }
   }
@@ -647,7 +657,7 @@
       val state1 = _state.inc_serial.progress_serial()
       for (db <- _database) {
         Build_Process.Data.write_progress(db, state1.serial, message, build_context.uuid)
-        Build_Process.Data.set_serial(db, state1.serial)
+        Build_Process.Data.set_serial(db, build_context.uuid, db.now(), state1.serial)
       }
       body
       _state = state1