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

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

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: Mar 04 2024 at 10:08 UTC