duplicate key value violates unique constraint "isabelle_build_sessions_pkey"

[Fabian Huch]

On 1/6/26 12:46, Fabian Huch wrote:
> There are two problems here:
>
> - the underlying problem is that the Isabelle/Scala process uses up a 
> lot more memory than it used to, causing OOM errors.
>
> - the build infrastructure cannot handle build processes that have 
> abnormally terminated.
>
>
> To address this, we can:
>
> (1) tune memory settings and investigate into why we're using up so 
> much more JVM memory than before -- I'll look into that first.

I checked and tuned the system:

- we had a rogue Isabelle process on one of the nodes that refused to 
terminate, eating up ~30GiB of that machine's RAM

- I reduced the maximal number of concurrent jobs on our lower-memory 
machines (which have 64GiB each)

This worked fine for the past week; however the memory consumption of 
the JVM process is still abnormally high.

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. I would propose to only keep the Document_ID.Command here, see 
the attached patch.


Fabian
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260113/547fd409/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: node_status_memory.patch
Type: text/x-patch
Size: 3440 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260113/547fd409/attachment.bin>