Email Gateway (Nov 24 2021 at 14:26): Email Gateway (Nov 24 2021 at 14:26):From: Makarius <makarius@sketis.net>
What is your OS version?
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
#approximations of polyml-5.9 for Isabelle2021-1
polyml-5.9-960de0cd0795
polyml-5.9-5d4caa8f7148
polyml-5.9-cc80e2b43c38
polyml-5.9-610a153b941d
Makarius
Email Gateway (Nov 27 2021 at 21:30):From: Makarius <makarius@sketis.net>
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
HOL-Analysis_heap.png
Email Gateway (Nov 28 2021 at 13:42):From: Makarius <makarius@sketis.net>
So how is the situation with these Poly/ML versions?
#bundled with Isabelle2021
polyml-test-f86ae3dc1686
#official release after Isabelle2021
polyml-5.8.2
We need some tangible empirical results to proceed.
Makarius
Email Gateway (Nov 30 2021 at 09:28):From: Matthew Torrence <matthew.torrence@twosixtech.com>
Some further details that were discovered from the Zulip:
The problem is that Auto quickcheck is evaluating 2^129 in nats, with
successor arithmetic, and is running out of memory. Importing
"HOL-Library.Code_Target_Numeral", or disabling auto quickcheck solves the
problem.
It does seem a bit odd though that this is the way auto quickcheck acts
when it encounters such arithmetic, instead of catching itself and giving
up...
Email Gateway (Nov 30 2021 at 10:56):From: Makarius <makarius@sketis.net>
Great, that is a tangible empirical situation.
I have turned it into the following example:
theory Scratch
imports Main
begin
definition test :: "nat"
where "test = 1000"
lemma "test = test + 1"
quickcheck a
end
Thus it is possible to add digits to the numeral and see how auto quickcheck
reacts -- while watching the ML heap in the Monitor panel. Afterwards the
explicit quickcheck command can be activated by removing the bad argument "a"
and not touching anything else.
The reason for the appearance of non-timeout is this change from Isabelle2019
(June 2019):
https://isabelle-dev.sketis.net/rISABELLE1bea05713dde
"""
physical vs. logical events, the latter takes GC time into account;
Timeout.apply is based on logical ML time;
"""
Attached is a change for Isabelle2021-1-RC4 that returns to physical timeout
specifically for quickcheck / try / auto_try.
I do hope that we can afford this isolated last-minute change on
Isabelle2021-1, for something that has been present in the past 3 releases.
Makarius
ch-physical_timeout
Email Gateway (Nov 30 2021 at 11:03):From: Makarius <makarius@sketis.net>
Side-remark: the Monitor panel already provides the buttons "GC" and "Sharing"
for the ML heap (since Isabelle2021).
Since the monitoring now works via an external process, it remains active
during GC ("ML cleanup").
Makarius
Last updated: Jul 15 2022 at 23:21 UTC