[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

Manuel Eberl eberlm at in.tum.de
Fri Aug 31 23:23:14 CEST 2018

It works on both my work laptop and my private desktop PC.

The work laptop is an Intel i7 something (I cannot recall the exact
model off the top of my head) and the desktop is an AMD Ryzen 1800X.
Both run with an up-to-date Arch Linux.

At least on the desktop, I tried it with both the 32 and 64 bit ML
system, and both worked.


On 31/08/2018 23:04, Makarius wrote:
> On 31/08/18 22:00, Manuel Eberl wrote:
>> What puzzles me the most is the fact that this behaviour seems to depend
>> on the underlying hardware, and it appears to be 100% reproducible on
>> machines where it does happen. If this is a race condition, it must be
>> one of the strangest one I have ever seen (note that it even happens in
>> single-threaded mode).
>> Perhaps it might also be of interest to try this with different versions
>> of Poly/ML, just to make sure it's not an issue with the underlying ML
>> environment.
> I see the same effect with Poly/ML 5.6 from Isabelle2017: a quite
> different environment compared to Isabelle2018.
> It requires the included change, and the following in
> $ISABELLE_HOME_USER/etc/settings:
>   init_component "$HOME/.isabelle/contrib/polyml-5.6-1"
> Moreover, it probably requires this adhoc Unix environment variable:
>   export LD_LIBRARY_PATH=$HOME/.isabelle/contrib/polyml-5.6-1/x86-linux
> This is Ubuntu 16.04.5 LTS on Intel(R) Xeon(R) CPU E5-2620 v3 @ 2.40GHz.
> What is actually your system where it happens to work?
> 	Makarius

More information about the isabelle-dev mailing list