Status update: > 2) virtual machines provided by LRZ > > LRZ offers cloud hosting of virtual machines. We could get an > allowance of 32 cores, although one single machine can only have 8 at > most (e.g. we could run 4 virtual machines with 8 cores each). This > severely constrains how we can run AFP tests. We would need to run > the "slow" AFP sessions seperately. I managed to get the elapsed time > for a "non-slow" AFP build down to about 3-4 hours, which is still a > lot, but since we could have 4 machines in parallel it wouldn't be a > big problem. This is also the reason why I ran the AFP in > single-threaded mode: to squeeze the last bit of performance out of > the machines. It turns out that under similar conditions, these > machines already run about 20% faster than the currently fastest > machine we have (lxbroy10). I haven't yet checked the elapsed time of > the "slow" sessions on one of these machines, but I suspect it's > going to be around 4 hours, too.
Thanks to our local sysops and the LRZ, I have obtained significant resources as written above (8 VMs with 8 cores each). I will configure these to run AFP (non-slow) on every push over the next one or two weeks. > 3) dedicated hardware with plenty of cores and RAM to be bought by > our chair This option is still pending, and not mutually exclusive with 2). Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
