[isabelle-dev] performance problems

[Fabian Immler]

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.

Fabian

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.
> 
> Manuel
> 
> 
> On 07/09/2018 17:39, Lawrence Paulson wrote:
>> What do you suggest for these on a 16 GB machine? I attach my file.
>> Larry
>>
>>> 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 
>>> memory.
>>
>>
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>