[isabelle-dev] 20 years of AFP

[Fabian Huch]

On 3/19/24 19:37, Makarius wrote:
> On 19/03/2024 13:21, Fabian Huch wrote:
>> Today marks 20 years of AFP -- to celebrate, here are a few timings 
>> with the new parallel build (Isabelle/08b83f91a1b2 and 
>> AFP/b61f72e5cba6):
>>
>> build -a
>> 0:08:47 elapsed time, 3:02:23 cpu time, factor 20.75
>>
>> build -A: -X slow -a
>> 0:43:11 elapsed time, 72:49:01 cpu time, factor 101.17
>>
>> build -A: -a
>> 2:07:56 elapsed time, 87:35:19 cpu time, factor 41.08
>
> That is really great.
>
> I was merely postulating < 10min for the Isabelle distribution (build 
> -a) and < 45min for non-slow AFP (build -A: -X slow -a) for several 
> years --- now that has become real. An a nominal speedup factor > 100 
> looks great.
>
> Fabian, you should also say a few words about the build cluster that 
> is used here.

Right -- the hardware used is 4 i9-12900K workstations (one of those 
CPUs costs about ~400$), plus a bulk of 10 slow machines.

Even with only the four workstations, the AFP can be built in an hour, 
and the time for AFP+very slow does not even change much.


Fabian