Email Gateway (Mar 19 2024 at 12:22): Email Gateway (Mar 19 2024 at 12:22):From: Fabian Huch <huch@in.tum.de>
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
Cheers!
Fabian
Email Gateway (Mar 19 2024 at 12:31):From: Fabian Huch <huch@in.tum.de>
Not yet as we're still experimenting with it.
The first is the distribution, the second the AFP without slow sessions
(which is what is run on the testboard), an the third the AFP with slow
and very slow sessions.
Fabian
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 19 2024 at 18:38):From: Makarius <makarius@sketis.net>
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.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 20 2024 at 13:15):From: Fabian Huch <huch@in.tum.de>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 22 2024 at 14:54):From: Tobias Nipkow <nipkow@in.tum.de>
Very nice! Thank you Fabian! Looking forward to a release version.
Tobias
Last updated: Apr 28 2024 at 08:19 UTC