[isabelle-dev] Spare cycles on compute server
Alexander Krauss
krauss at in.tum.de
Thu Apr 5 10:30:06 CEST 2012
> our system administrators just told me that our Munich compute server
> (lxbroy10) still has many spare cycles, which we could use for more
> testing and other measurements.
> At the moment, there are two processes: one checking isabelle_makeall on
> the testboard, another checking AFP_fast on the testboard.
> Any suggestions what we should test more?
I've been using lxbroy10 for some importer-related benchmarks (which
require(d) lots of GBs of RAM) but were only single-threaded. With
recent improvements I'll probably be able to move back to lxbroy7-8 or
even macbroy2x...
At a later stage, benchmarking a parralelized import may be interesting,
but we are not there yet.
Alex
More information about the isabelle-dev
mailing list