[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