[isabelle-dev] performance problems
immler at in.tum.de
Fri Sep 7 19:19:37 CEST 2018
I experienced the same issues: Importing Pure (e50312982ba0) the
following "freezes" the IDE in the sense Manuel described.
lemma "PROP P"
apply (rule ?)+
It works fine in Isabelle2018. Also note that
lemma "PROP P"
by (rule ?)+
works fine in e50312982ba0, as well.
On 9/7/2018 11:51 AM, Manuel Eberl wrote:
> I have also noted a few strange issues with the development version
> (currently e50312982ba0) these last few days, but I have not yet had the
> time to try to reproduce them.
> Basically, what happens is that occasionally, the IDE "freezes" in the
> sense that no new changes to the document are processed. I can still
> view the output of all the processed commands, but there is a certain
> position in the document underneath which all the text is red, and it
> never because not red. If I change anything in the text before that, it
> also becomes red forever.
> It seems to me that this is particularly triggered by non-terminating
> invocations of simp/auto/etc., even if I abort them after a fraction of
> a second.
> I don't think the 2018 release had this problem, but I could be wrong.
> If I find out any more precise details, I will let you know.
> On 07/09/2018 17:39, Lawrence Paulson wrote:
>> What do you suggest for these on a 16 GB machine? I attach my file.
>>> On 7 Sep 2018, at 15:01, Makarius <makarius at sketis.net
>>> <mailto:makarius at sketis.net>> wrote:
>>> If you are using the 64-bit version of Poly/ML, you should give both
>>> --minheap and --maxheap, otherwise it tends to overcommit a lot of
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev