> 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.
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
isabelle-dev mailing list