[isabelle-dev] Future of isatest/afptest

[Lars Hupel]

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