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
https://isabelle.sketis.net/devel/build_status/macOS_10.15_Catalina_4_threads/index.html#session_HOL-Analysis

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


	Makarius

Attachment: HOL-Analysis_heap.png
Description: PNG image



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