[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