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/Library/Library.thy or
$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
Cygwin64.


	Makarius




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