Re: [isabelle] Engineering Workstation for Isabelle



On 07/04/2019 00:03, Makarius wrote:
> 
> Here are some adhoc numbers from "isabelle build -g main" (approximately
> at Isabelle2019-RC0):
> 
>   ISABELLE_BUILD_OPTIONS="threads=6"
> 
>   ML_PLATFORM="x86_64_32-linux"
>   ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.8/x86_64_32-linux"
>   ML_SYSTEM="polyml-5.8"
>   ML_OPTIONS="--minheap 1500"
> 
> Finished HOL (0:02:12 elapsed time, 0:06:43 cpu time, factor 3.05)
> Finished HOL-Analysis (0:04:09 elapsed time, 0:18:37 cpu time, factor 4.48)
> Finished HOL-Library (0:01:05 elapsed time, 0:05:01 cpu time, factor 4.60)
> Finished HOL-Computational_Algebra (0:00:36 elapsed time, 0:01:44 cpu
> time, factor 2.89)
> Finished HOL-Algebra (0:00:40 elapsed time, 0:03:33 cpu time, factor 5.24)
> Finished HOL-Probability (0:00:39 elapsed time, 0:03:14 cpu time, factor
> 4.94)
> Finished HOL-Number_Theory (0:00:30 elapsed time, 0:02:11 cpu time,
> factor 4.33)
> 
> I will try this again tomorrow, with all 8 cores, and also with this
> hot/noisy turbo mode.

That is now, so here are more measurements in turbo mode (CPU up to
4.9GHz, fan noise approx. 46dB at 1m distance, 43dB at 2m distance).


First with ISABELLE_BUILD_OPTIONS="threads=6":

$ isabelle build -g main -f
Finished Pure (0:00:10 elapsed time, 0:00:10 cpu time, factor 0.99)
Finished HOL (0:01:43 elapsed time, 0:05:18 cpu time, factor 3.08)
Finished HOL-Analysis (0:03:19 elapsed time, 0:14:55 cpu time, factor 4.50)
Finished HOL-Library (0:00:53 elapsed time, 0:04:06 cpu time, factor 4.62)
Finished HOL-Computational_Algebra (0:00:28 elapsed time, 0:01:22 cpu
time, factor 2.93)
Finished HOL-Algebra (0:00:32 elapsed time, 0:02:52 cpu time, factor 5.33)
Finished HOL-Probability (0:00:30 elapsed time, 0:02:37 cpu time, factor
5.11)
Finished HOL-Number_Theory (0:00:23 elapsed time, 0:01:45 cpu time,
factor 4.40)
Finished HOLCF (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.43)
Finished ZF (0:00:05 elapsed time, 0:00:17 cpu time, factor 3.21)
Finished HOL-Word (0:00:04 elapsed time, 0:00:19 cpu time, factor 4.15)
0:08:27 elapsed time, 0:34:02 cpu time, factor 4.02


Now with ISABELLE_BUILD_OPTIONS="threads=8", attempting to saturate this
8-core CPU:

$ isabelle build -g main -f

Finished Pure (0:00:10 elapsed time, 0:00:10 cpu time, factor 0.99)
Finished HOL (0:01:44 elapsed time, 0:05:33 cpu time, factor 3.20)
Finished HOL-Analysis (0:02:54 elapsed time, 0:16:08 cpu time, factor 5.56)
Finished HOL-Library (0:00:49 elapsed time, 0:04:29 cpu time, factor 5.41)
Finished HOL-Computational_Algebra (0:00:28 elapsed time, 0:01:26 cpu
time, factor 3.01)
Finished HOL-Algebra (0:00:32 elapsed time, 0:03:02 cpu time, factor 5.62)
Finished HOL-Probability (0:00:27 elapsed time, 0:02:48 cpu time, factor
6.21)
Finished HOL-Number_Theory (0:00:23 elapsed time, 0:01:51 cpu time,
factor 4.72)
Finished HOLCF (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.50)
Finished ZF (0:00:05 elapsed time, 0:00:18 cpu time, factor 3.22)
Finished HOL-Word (0:00:04 elapsed time, 0:00:20 cpu time, factor 4.22)
0:07:56 elapsed time, 0:36:25 cpu time, factor 4.59


Such test times << 10min of the main library sessions are very important
when exploring changes on Pure or basic HOL.

More serious library maintenance (against AFP) requires a server-class
multicore monster: e.g. 2 * 20 cores (Intel) or 8 * 8 cores (AMD). This
results in approx. 45..90..120 min total build time for everything. The
server scenario also explains the ANNOUNCE entry of Isabelle2019-RC0:

* Update to current Java 11 and Poly/ML 5.8 with better scalability.

Since we are still moving forward on both legs, AFP applications can
still grow, and we continue to live and prosper.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.