duplicate key value violates unique constraint "isabelle_build_sessions_pkey"

[Fabian Huch]

On 1/17/26 23:34, Makarius wrote:
> 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.

Hm. I had measured a small number of samples (since heap snapshots are 
expensive and large) before and after the change and looked at the heap 
composition. But it is possible that the (consistently) lower heap size 
was coincidental, and the extended lifetime of these Command markups did 
not actually matter -- I'll have to figure out how to properly deal with 
our opaque cache in MAT.

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

One problem with this experimental setup is that current heap size is 
not a good metric for such a high-throughput application (most memory 
used would actually be dead).

Also, the smoothing hides what is going on, e.g. when the heap limit is 
hit (cf. plot for 1 below). I would rather use the MXBeans of the 
garbage collector to obtain GC events and plot a proper peak-to-peak curve.


Fabian
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260119/d697dece/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: eY93XwRiR134kXXF.png
Type: image/png
Size: 249332 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260119/d697dece/attachment-0001.png>