duplicate key value violates unique constraint "isabelle_build_sessions_pkey"

[Makarius]

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

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.


	Makarius