[isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171108/acbf4dc6/attachment-0002.html>