Stream: Mirror: Isabelle Development Mailing List

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

Email Gateway (May 30 2023 at 10:15):

From: Makarius <makarius@sketis.net>
* General *

• ML heap usage and stored heap size has been significantly reduced,
  especially for applications with a lot of definitions in a 'locale' or
  'class' context. The shrink factor is usually in the range 1.1 .. 2.0,
  but a factor 3 .. 10 has been seen in unusual situations. This often
  allows big applications to return to the "small" 64_32 memory model with
  its hard limit of 16 GiB, and thus reduce the heap size by another
  factor 1.8.

This refers to current f3d19c8445ec: many changesets are leading towards this
great improvement. The key point is actually rather small:

changeset: 78048:f16067da45ef
user: wenzelm
date: Mon May 15 14:13:58 2023 +0200
files: src/Pure/Isar/proof_context.ML src/Pure/assumption.ML
src/Pure/variable.ML
description:
avoid capture of inner/outer context and thus reduce heaps sizes by 20..40%
(see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);

That factor 1.2 .. 1.4 was merely for HOL and HOL-Analysis. Better factors are
seen here:

HOL-Algebra 3.6
HOL-Probability 1.6

Category3 5.2
MonoidalCategory 7.6

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (May 30 2023 at 20:11):

From: Makarius <makarius@sketis.net>
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

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (May 31 2023 at 10:53):

From: Lawrence Paulson <lp15@cam.ac.uk>
These are tremendous improvements! Many thanks.

As you know, people are relying more and more locales to structure elaborate definition hierarchies, so we need this. And I gather that the users of certain other systems have to put up with major performance issues once a proof is more than a couple of dozen lines long.

Larry

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Apr 28 2024 at 12:28 UTC