[isabelle-dev] NEWS: significantly reduced ML heap usage

Makarius makarius at sketis.net
Tue May 30 22:10:23 CEST 2023


Here are some more measurements to show the quite significant effect on 
locale-laden applications.

This is (1) current Isabelle/f3d19c8445ec + AFP/d34609a6a678 versus (2) 
Isabelle2022 + afp-2022/2458cc9f2178 on the rather heavy session Padic_Ints.

The whole stack of contributing sessions is shown below, with shrink factor:

HOL 1.56
HOL-Library 1.43
HOL-Computational_Algebra 1.80
HOL-Algebra 4.03
Padic_Ints 5.18
Padic_Field 12.5
ALL 2.87 (1.45 GiB / 0.50 GiB)


This is isabelle build -o parallel_proofs=0 to shrink the heap a bit more.

Timing did not change significantly:

(1)
Finished HOL (0:06:13 elapsed time, 0:10:31 cpu time, factor 1.69)
Finished HOL-Library (0:04:11 elapsed time, 0:11:14 cpu time, factor 2.69)
Finished HOL-Computational_Algebra (0:01:14 elapsed time, 0:02:22 cpu time, 
factor 1.91)
Finished HOL-Algebra (0:04:39 elapsed time, 0:10:42 cpu time, factor 2.30)
Finished Padic_Ints (0:03:23 elapsed time, 0:07:18 cpu time, factor 2.16)
Finished Padic_Field (0:12:49 elapsed time, 0:21:32 cpu time, factor 1.68)

(2)
Finished Pure (0:00:14 elapsed time, 0:00:14 cpu time, factor 0.97)
Finished HOL (0:06:05 elapsed time, 0:11:26 cpu time, factor 1.88)
Finished HOL-Library (0:03:58 elapsed time, 0:10:30 cpu time, factor 2.65)
Finished HOL-Computational_Algebra (0:01:08 elapsed time, 0:02:11 cpu time, 
factor 1.92)
Finished HOL-Algebra (0:04:20 elapsed time, 0:10:06 cpu time, factor 2.33)
Finished Padic_Ints (0:02:51 elapsed time, 0:05:34 cpu time, factor 1.95)
Finished Padic_Field (0:14:34 elapsed time, 0:24:42 cpu time, factor 1.70)


	Makarius



More information about the isabelle-dev mailing list