> You could try with a fresh build of Poly/ML: Okay, I rebuilt Poly/ML (not libsha1 and libgmp though; apparently your build script does not build those). The crashes still occured though. I think I did everything correctly, because when I delete the files that the compilation created, isabelle build fails immediately with some ML-related error message, so it must have been using them.
> It should be sufficient to remove the is_pure() here: That does indeed seem to make the problem go away completely. At least I got about 50 consecutive builds without any crashes now. Manuel On 2017-11-08 15:35, Makarius wrote: > On 08/11/17 09:21, Manuel Eberl wrote: >> After a lengthy bisection, I found that the first revision where no >> crashes occur is this one: >> >> changeset: 66920:aefaaef29c58 >> user: wenzelm >> date: Thu Oct 26 13:44:41 2017 +0200 >> summary: use Poly/ML 5.7.1 test version as default; >> Does Poly/ML 5.7.1 contain any changes that could plausibly cause this >> bad behaviour to go away? > One side-condition that has also changed is the build platform: for the > various Poly/ML 5.6 Isabelle components it was still Ubuntu 10.04 LTS, > for current Poly/ML 5.7.1 test versions it is Ubuntu 12.04 LTS. > > Sometimes there are problems in the C/C++ compiler that disappear over > time. You could try with a fresh build of Poly/ML: the README in the > component contains brief instructions how to operate on the included src > directory. > > > Makarius
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev