Re: [isabelle] Isabelle2021-1-RC3: excessive Poly/ML heap requirements

On 24/11/2021 15:26, Makarius wrote:
> Can you can try this with other versions of Poly/ML? Here are some formal
> component names:
> #bundled with Isabelle2021
> polyml-test-f86ae3dc1686
> #official release after Isabelle2021
> polyml-5.8.2

I think that only these 2 alternatives are relevant for a comparison.

Generally, I do see lots of heap usage on "small" machines with only 8-24 GB,
especially on weak VM nodes. Sometimes this causes problems to built
HOL-Analysis or HOL-Data_Structures.

The question: Is this really a new problem for Isabelle2021-1 that was absent
in Isabelle2021?

Attached are some measurements for HOL-Analysis in the past 400 days: nothing
special to be seen. Here is further context

Note that this test line uses 4 threads with a "cold start", i.e. no  previous
information about the timing of proofs.


Attachment: HOL-Analysis_heap.png
Description: PNG image

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