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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
