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

Makarius makarius at sketis.net
Fri May 17 17:24:50 CEST 2013


On Thu, 16 May 2013, Lars Noschinski wrote:

> -----------------------------
> 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"?

lxbroy10 has 4 CPU modules with 6 cores each, with relatively low memory 
bandwidth between them. So if you want to go into such details, you could 
say "--gcthreads 6".  Actual phyisical measurements would be required for 
more than just rules of thumb.

Alternatively, you could just make a general default of "--gcthreads 4" 
for all machines as decent approximation.


 	Makarius



More information about the isabelle-dev mailing list