duplicate key value violates unique constraint "isabelle_build_sessions_pkey"

[Fabian Huch]

On 1/13/26 13:54, Makarius wrote:
> On 13/01/2026 11:26, Fabian Huch wrote:
>>
>> Looking at memory snapshots of the build, one of the reasons is the 
>> recent incorporation of Node_Status into the progress: 
>> command_timings are stored as
>>
>> command_timings:Map[Command, Command_Timings]
>>
>> and the command (in the key) contains large markups, e.g. in 
>> init_markups, during the lifetime of these timings: up to ~1GiB 
>> during the build of the distribution, likely significantly more in an 
>> AFP build.
> Thanks for the measurements. I've already suspected a problem exactly 
> there, but did not know how to do memory profiling on the JVM.
>
> Can you give some hints on how to do that?
>
I usually do this by analyzing multiple heap dumps of the JVM during the 
run. Those can be generated either from within the JVM, like so:

def dump_heap(file: Path, include_live: Boolean =true): Unit = {
   val mxBean = java.lang.management.ManagementFactory.getPlatformMXBean(
     classOf[com.sun.management.HotSpotDiagnosticMXBean])
   mxBean.dumpHeap(file.absolute.implode, include_live)
}

or by instructing the JVM from the outside, e.g. via 'jmap 
-dump:format=b,file=heap.hprof <pid>'

These heap dumps can then be analyzed with tools such as Eclipse MAT or 
JProfiler, in particular by:

- looking at histograms of object classes and their shallow heap 
size/retained heap size, e.g. here you see that command markups retain 
~1GiB of heap:

- analyzing the memory graph through tree views, e.g. here you can see 
what why the command markups are retained (there is a delayed event to 
update the progress, where the largest Command key has ~16MiB init_markups):

However, I couldn't get MAT to ignore the weak references of our XML 
cache (displayed as object with largest retained heap); this makes it 
far less useful here.

Perhaps this is possible by tinkering with the options, but I don't know 
how -- I used to work with JProfiler, but that is commercial.


Fabian
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260113/64d8fcee/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: xVNQjnDCttesdZ9N.png
Type: image/png
Size: 81410 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260113/64d8fcee/attachment-0002.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: IWTyC0NJNa2j0viE.png
Type: image/png
Size: 178775 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260113/64d8fcee/attachment-0003.png>