Windows 7 Flagship x64 Chinese Version
CPU is Intel i7 3.40G, just one core, 8G physical memory
I have increased heap memory to 4096M，when I import "$ISABELLE_HOME/src/HOL/Analysis/Analysis.thy" into a new theory file,
though it's very slow, but it doesn't get stuck and finishes importing.
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.
Anyway, I appreciate your reply. Thank you.
------------------ 原始邮件 ------------------
发件人: "Makarius"<makarius at sketis.net>;
发送时间: 2018年5月15日(星期二) 晚上10:55
收件人: "永不止步"<121171528 at qq.com>;"cl-isabelle-users"<cl-isabelle-users at lists.cam.ac.uk>;
主题: Re: [isabelle] help about an Isabelle IDE problem
On 08/05/18 03:57, 永不止步 wrote:
> I'm a new user of Isabelle and I met a strange problem when I wrote theory files. The system always gets stuck when it processes some thy file, and there are no warnings, no errors. It seems the system is just not responding. CPU usage is about 40-50%, memory is about 1.5G-3G. I have tried windows64 version 2016-1 and 2017, there's the same problem. The following is the screeshot
This is odd and normally should not happen -- unless there is a huge
waste of resources somewhere.
* What is your Windows version?
* How many CPU cores do you have?
* How many GB memory do you have?
Does this it also happen with existing library theories? E.g. from
$ISABELLE_HOME/src/HOL/Analysis/Analysis.thy (which is rather big).
The latter might require more Java resources. For Isabelle2017 on
Windows 64, you can edit $ISABELLE_HOME/Isabelle2017.l4j.ini and grant
more heap space, e.g. replace "-Xmx2560m" by "-Xmx4096m". Restart the
Isabelle application afterwards: Isabelle/jEdit has a Java heap
indicator in the right-bottom corner.
You can also try https://isabelle.sketis.net/devel/release_snapshot as
an early preview of Isabelle2018 -- it has updated versions of Poly/ML
and Java 8, which could make a difference.
Unfortunately, Sledgehammer and some other tools will not work in this
snapshot: Jasmin Blanchette still needs to update various components to
This archive was generated by a fusion of
Pipermail (Mailman edition) and