maintain "uuid" column in session build database, to identity the original build process uniquely;
implicit upgrade of PostgreSQL database, while SQLite is initially removed and created afresh;

--- a/NEWS	Thu Aug 25 12:29:42 2022 +0200
+++ b/NEWS	Thu Aug 25 15:30:21 2022 +0200
@@ -245,6 +245,10 @@
 Isabelle repository: a regular download of the distribution will not
 work!
 
+* The session build database now maintains an additional "uuid" column
+to identity the original build process uniquely. Thus other tools may
+dependent symbolically on a particular build instance.
+
 * External Isabelle tools implemented as .scala scripts are no longer
 supported. INCOMPATIBILITY, instead provide a proper Isabelle/Scala
 module with etc/build.props and "services" for a suitable class instance

--- a/src/Pure/General/sql.scala	Thu Aug 25 12:29:42 2022 +0200
+++ b/src/Pure/General/sql.scala	Thu Aug 25 15:30:21 2022 +0200
@@ -409,6 +409,8 @@
 /** PostgreSQL **/
 
 object PostgreSQL {
+  type Source = SQL.Source
+
   val default_port = 5432
 
   lazy val init_jdbc: Unit = Class.forName("org.postgresql.Driver")

--- a/src/Pure/ROOT.ML	Thu Aug 25 12:29:42 2022 +0200
+++ b/src/Pure/ROOT.ML	Thu Aug 25 15:30:21 2022 +0200
@@ -364,3 +364,4 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML";
+

--- a/src/Pure/Thy/sessions.scala	Thu Aug 25 12:29:42 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Aug 25 15:30:21 2022 +0200
@@ -10,6 +10,7 @@
 import java.nio.ByteBuffer
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption
+import java.sql.SQLException
 
 import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.collection.mutable
@@ -1191,9 +1192,14 @@
     val input_heaps = SQL.Column.string("input_heaps")
     val output_heap = SQL.Column.string("output_heap")
     val return_code = SQL.Column.int("return_code")
-    val build_columns = List(sources, input_heaps, output_heap, return_code)
+    val uuid = SQL.Column.string("uuid")
+    val build_columns = List(sources, input_heaps, output_heap, return_code, uuid)
 
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
+
+    val augment_table: PostgreSQL.Source =
+      "ALTER TABLE IF EXISTS " + table.ident +
+        " ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql)
   }
 
   def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
@@ -1350,6 +1356,9 @@
         db.create_table(Session_Info.table)
         db.using_statement(
           Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute())
+        if (db.isInstanceOf[PostgreSQL.Database]) {
+          db.using_statement(Session_Info.augment_table)(_.execute())
+        }
 
         db.create_table(Export.Data.table)
         db.using_statement(
@@ -1382,7 +1391,8 @@
       build: Build.Session_Info
     ): Unit = {
       db.transaction {
-        db.using_statement(Session_Info.table.insert()) { stmt =>
+        val table = Session_Info.table
+        db.using_statement(table.insert()) { stmt =>
           stmt.string(1) = name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
           stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.xz)
@@ -1394,6 +1404,7 @@
           stmt.string(9) = cat_lines(build.input_heaps)
           stmt.string(10) = build.output_heap getOrElse ""
           stmt.int(11) = build.return_code
+          stmt.string(12) = build.uuid
           stmt.execute()
         }
       }
@@ -1422,17 +1433,21 @@
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = {
       if (db.tables.contains(Session_Info.table.name)) {
-        db.using_statement(Session_Info.table.select(Session_Info.build_columns,
+        db.using_statement(Session_Info.table.select(Nil,
           Session_Info.session_name.where_equal(name))) { stmt =>
           val res = stmt.execute_query()
           if (!res.next()) None
           else {
+            val uuid =
+              try { Option(res.string(Session_Info.uuid)).getOrElse("") }
+              catch { case _: SQLException => "" }
             Some(
               Build.Session_Info(
                 res.string(Session_Info.sources),
                 split_lines(res.string(Session_Info.input_heaps)),
                 res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
-                res.int(Session_Info.return_code)))
+                res.int(Session_Info.return_code),
+                uuid))
           }
         }
       }

--- a/src/Pure/Tools/build.scala	Thu Aug 25 12:29:42 2022 +0200
+++ b/src/Pure/Tools/build.scala	Thu Aug 25 15:30:21 2022 +0200
@@ -21,7 +21,8 @@
     sources: String,
     input_heaps: List[String],
     output_heap: Option[String],
-    return_code: Int
+    return_code: Int,
+    uuid: String
   ) {
     def ok: Boolean = return_code == 0
   }
@@ -356,7 +357,7 @@
                   if (process_result.timeout) build_log.error("Timeout") else build_log,
                 build =
                   Session_Info(sources_stamp(build_deps, session_name), input_heaps, heap_digest,
-                    process_result.rc)))
+                    process_result.rc, UUID.random().toString)))
 
             // messages
             process_result.err_lines.foreach(progress.echo)