Email Gateway (Aug 22 2022 at 17:17): Email Gateway (Aug 22 2022 at 17:17):From: Makarius <makarius@sketis.net>
On 18/05/18 08:54, 永不止步 wrote:
Windows 7 Flagship x64 Chinese Version
CPU is Intel i7 3.40G, just one core, 8G physical memory
This is a fairly good CPU, note that the i7 line usually has 2 or 4 cores.
8G memory is not so much: it is the minimum for medium sized Isabelle
applications. HOL/Analysis is already slightly beyond that. 16G would be
better.
When it loads my theory file, it still gets stuck and I find there are many heap memory not used,
like 1104/1956 displayed at the right-bottom of the window.I think there should be some problem with my theory file, not the problem of the memory.
That memory display is for the Java process that runs the IDE. It fills
up quickly with relatively big theories as in HOL/Analysis.
In addition to that, there is the Poly/ML prover process: in its default
configuration it can expand to approx. 3.5 GB. You can use the Windows
task manager to check its status.
When both the Java and Poly/ML process approach 4 GB, it will no longer
fit into a total of only 8 GB.. The OS and other programs also use some
memory, so the overall system becomes very slow.
I suspect that your theory contains material that uses a lot of
resources on the prover side. If you want to show me your sources
privately (not on the mailing list), I can take a closer look.
Makarius
Last updated: Apr 24 2024 at 20:16 UTC