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

[Lawrence Paulson]

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

> On 30 May 2023, at 21:10, Makarius <makarius at sketis.net> wrote:
> 
> 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.