Re: [isabelle] Engineering Workstation for Isabelle



On 07/04/2019 00:45, Makarius wrote:
> On 07/04/2019 00:03, Makarius wrote:
> 
> here are more measurements in turbo mode (CPU up to
> 4.9GHz, fan noise approx. 46dB at 1m distance, 43dB at 2m distance).

> 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

For completeness, here is the same test with 3.6GHz (no turbo, no noise):

  ISABELLE_BUILD_OPTIONS="threads=8"

  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 Pure (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.99)
Finished HOL (0:02:10 elapsed time, 0:06:47 cpu time, factor 3.13)
Finished HOL-Analysis (0:03:22 elapsed time, 0:18:44 cpu time, factor 5.55)
Finished HOL-Library (0:00:56 elapsed time, 0:05:08 cpu time, factor 5.43)
Finished HOL-Computational_Algebra (0:00:35 elapsed time, 0:01:45 cpu
time, factor 2.95)
Finished HOL-Algebra (0:00:39 elapsed time, 0:03:36 cpu time, factor 5.51)
Finished HOL-Probability (0:00:32 elapsed time, 0:03:16 cpu time, factor
6.04)
Finished HOL-Number_Theory (0:00:28 elapsed time, 0:02:13 cpu time,
factor 4.63)
Finished HOLCF (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.47)
Finished ZF (0:00:06 elapsed time, 0:00:22 cpu time, factor 3.27)
Finished HOL-Word (0:00:05 elapsed time, 0:00:25 cpu time, factor 4.23)
0:09:31 elapsed time, 0:42:53 cpu time, factor 4.50


	Makarius




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