Re: [isabelle] 回复: help about an Isabelle IDE problem



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




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