<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1"><br>
<br>
<blockquote type="cite"><font size="+1">You could try with a
fresh build of Poly/ML:</font></blockquote>
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.</font></p>
<p>
<blockquote type="cite"><font size="+1">It should be sufficient to
remove the is_pure() here:</font></blockquote>
<font size="+1">That does indeed seem to make the problem go away
completely. At least I got about 50 consecutive builds without
any crashes now.</font></p>
<p><font size="+1">Manuel</font><br>
</p>
<br>
<div class="moz-cite-prefix">On 2017-11-08 15:35, Makarius wrote:<br>
</div>
<blockquote type="cite"
cite="mid:d6967b56-bdd7-b48e-742c-fe30948b769b@sketis.net">
<pre wrap="">On 08/11/17 09:21, Manuel Eberl wrote:
</pre>
<blockquote type="cite">
<pre wrap="">
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;
</pre>
</blockquote>
<pre wrap="">
</pre>
<blockquote type="cite">
<pre wrap="">Does Poly/ML 5.7.1 contain any changes that could plausibly cause this
bad behaviour to go away?
</pre>
</blockquote>
<pre wrap="">
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
</pre>
</blockquote>
<br>
</body>
</html>