[isabelle-dev] *** [SQLITE_CONSTRAINT] Abort due to constraint violation (UNIQUE constraint failed: isabelle_session_info.session_name)

[Makarius]

On 14/11/2019 18:23, Tobias Nipkow wrote:
> This is how my build of HOL fails - I am on 8d51418d4ec0.

This means that the HOL.db file in the heaps directory somehow got into
a bad state, e.g. when two build processes attempt to update it without
proper coordination.

Normally it is sufficient to force a fresh build, e.g. with option -c or -f.

In rare situations one needs to remove the bad database file manually.


	Makarius