duplicate key value violates unique constraint "isabelle_build_sessions_pkey"

[Makarius]

On 14/01/2026 21:22, Makarius wrote:
> 
> See now:
> 
> changeset:   83825:3ed2781b1cc5
> user:        wenzelm
> date:        Wed Jan 14 13:09:47 2026 +0100
> files:       src/Pure/PIDE/document_status.scala src/Tools/jEdit/src/ 
> timing_dockable.scala
> description:
> more frugal persistent data, notably for batch builds --- proposed by Fabian 
> Huch, after Java heap measurements (see also 3f6280aedbcc, a110e7e24e55, 
> 9cc5d77d505c);
> 
> It is your original change, with my explanation from the history. I've added a 
> few more changes on top, but they don't make a fundamental difference.
> 
> Note that I did not repeat any performance measurements. I want to do this 
> eventually, also to see if other problems are present.

I have now done some measurements with "isabelle build -o threads=8 -j2 -a -f" 
on my Linux box (16 cores), using the included patch for the Isabelle/Scala 
implementation of "isabelle build".

The Scala/Java process uses these settings:

    ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g 
-Xss16m -XX:+UseZGC -XX:+ZGenerational -XX:SoftMaxHeapSize=2g"

Attached is raw data from the parent of 3ed2781b1cc5 (1), and from 
3ed2781b1cc5 (2). The diagram.png is from gnuplot:

    plot '1.dat' using 1:2 smooth sbezier title "1 heap_size" noenhanced, 
'1.dat' using 1:3 smooth sbezier title "1 heap_used" noenhanced, '2.dat' using 
1:2 smooth sbezier title "2 heap_size" noenhanced, '2.dat' using 1:3 smooth 
sbezier title "2 heap_used" noenhanced


Conclusion: There is nothing interesting to be seen here. The change hardly 
makes a difference.

It could mean that occurrences of Document_ID.Command and Command are in 
1-to-1 correspondence on the heap, i.e. no stored Command is later updated/copied.

Or it could mean that I've got something wrong in the experimental setup.


	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1768688093 -3600
#      Sat Jan 17 23:14:53 2026 +0100
# Node ID 47a0e444953d84ede2a918fe52356b9eee89015e
# Parent  3ed2781b1cc5844cc87a642a872cb82f1c6c2aa0
test

diff -r 3ed2781b1cc5 -r 47a0e444953d src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Wed Jan 14 13:09:47 2026 +0100
+++ b/src/Pure/Build/build_process.scala	Sat Jan 17 23:14:53 2026 +0100
@@ -1337,6 +1337,8 @@
     }
   }
 
+  val t0 = Time.now()
+
   def run(): Build.Results = {
     val vacuous =
       synchronized_database("Build_Process.init") {
@@ -1362,7 +1364,11 @@
               build_send(Build_Process.private_data.channel_ready)
             }
           }
-          while(!build_action()) {}
+          while(!build_action()) { }
+          val t = Time.now() - t0
+          val mem = Java_Statistics.memory_status()
+          File.append(Path.explode("a.dat"),
+            t.toString + " " + mem.heap_size.MiB + " " + mem.heap_used.MiB + "\n")
         }
       }
       finally {
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 1.dat.xz
Type: application/x-xz
Size: 23232 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260117/fb6ceaed/attachment-0002.xz>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 2.dat.xz
Type: application/x-xz
Size: 23300 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260117/fb6ceaed/attachment-0003.xz>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: diagram.png
Type: image/png
Size: 86526 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260117/fb6ceaed/attachment-0001.png>