[isabelle-dev] Global build failures of the AFP in the testboard

Lars Noschinski noschinl at in.tum.de
Thu May 16 18:09:21 CEST 2013


On 16.05.2013 00:43, Gerwin Klein wrote:
>
> On 16.05.2013, at 1:25 AM, Lars Noschinski<noschinl at in.tum.de>  wrote:
>
>> @Alex, Gerwin: Is there any reason remaining why the AFP should not use the default PolyML version?  I remember Alex and I dropped a similar override from the Isabelle tests.
>
> Not that I am aware of. The main reason there was an explicit version mention there was to keep track of what exactly was running and where it came from. We have a record of that now with the component system, so that can be dropped.

Ok. Currently the options are

-----------------------------
ML_PLATFORM=x86-linux
ML_HOME="/home/polyml/polyml-svn/x86-linux"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="-H 1000"

ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"
-----------------------------

and I would simplify this to:

-----------------------------
ML_OPTIONS="-H 1000"

ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"
-----------------------------

Since AFP tests run both on lxbroy10 (for the testboard) and lxbroy8 
(for main); should I add a special case for lxbroy10 with "--gcthreads 8"?

   -- Lars



More information about the isabelle-dev mailing list