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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
