duplicate key value violates unique constraint "isabelle_build_sessions_pkey"

[Fabian Huch]

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.

(2) Make the system more robust in the face of such problems. I need to 
sit down with Makarius to discuss this.

(3) Make the scheduling aware of memory limitations. The system was 
designed such that this is possible, but it requires more work. I'll 
work on that once the immediate problems are solved.


Fabian


On 1/2/26 22:08, Makarius wrote:
> On 02/01/2026 09:15, Tobias Nipkow wrote:
>> Unfortunately the build system has hit the same problem again.
>
> I have reset everything once more, and tried "isabelle build_task -a" 
> successfully.
>
> Hopefully this is sufficient for the rest of the Christmas vacation. I 
> will be mostly unavailable at least until 07-Jan-2026.
>
>
>     Makarius
>
>