Re: [isabelle-dev] performance problems

[Makarius]

On 07/09/18 20:22, Lawrence Paulson wrote:
> 
>> For 16 GB, I usually run Poly/ML in 32-bit mode
> 
> How do you do that?

When Isabelle/jEdit is running, you disable the Plugin Option Isabelle /
General / ML system 64 and restart the application.

Or when it is not running, you edit $ISABELLE_HOME_USER/etc/preferences
and remove ML_system_64 = "true" and then start the application.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] performance problems

[Lawrence Paulson]

> On 7 Sep 2018, at 19:18, Makarius  wrote:
> 
> I can't try it out, since theory "Explorer" is missing.

Attached. A very cool thing. 


Explorer.thy
Description: Binary data


> For 16 GB, I usually run Poly/ML in 32-bit mode

How do you do that?

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] performance problems

[Makarius]

On 07/09/18 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 > > 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.

I can't try it out, since theory "Explorer" is missing.

For 16 GB, I usually run Poly/ML in 32-bit mode, with --minheap 1500.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] performance problems

[Makarius]

On 07/09/18 17:51, Manuel Eberl wrote:
> 
> 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.

On 07/09/18 19:19, Fabian Immler wrote:
> I experienced the same issues: Importing Pure (e50312982ba0) the
> following "freezes" the IDE in the sense Manuel described.
>
> lemma "PROP P"
>   apply (rule ?)+

Thanks for reporting the problem and pinning it down precisely. See now:

changeset:   68930:fc5763d000e8
user:wenzelm
date:Fri Sep 07 19:49:26 2018 +0200
files:   src/Pure/PIDE/command.ML
description:
proper tast_context (amending 5f44ad150ed8);


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] performance problems

[Manuel Eberl]

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 > > 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-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


pEpkey.asc
Description: application/pgp-keys
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] performance problems

[Lawrence Paulson]

What do you suggest for these on a 16 GB machine? I attach my file.
Larry


On 7 Sep 2018, at 15:01, Makarius  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.

Binomial_sol.thy
Description: Binary data
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] performance problems

[Makarius]

On 06/09/18 17:14, Lawrence Paulson wrote:
> I'm facing serious performance problems with the development version and I 
> have no idea what's happening, though it may be connected with my settings. 
> At the moment I am using
> 
> JEDIT_JAVA_OPTIONS64="-Xms2048m -Xmx8192m -Xss8m"
> ML_OPTIONS="--minheap 3500"
> 
> (I'm not aware of any guidelines of what sort of settings are appropriate.)

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.

If you are using the 32-bit version, you should start with a much small
--minheap -- I usually use 1500. The maxheap is implicit by the virtual
memory boundary.


> My theory doesn't use the AFP and I have moved aside my components file, 
> which refers to afp/devel. My theory imports nothing but Complex_Main. Yet 
> still, Isabelle/jEdit takes on the order of a minute to launch, and freezes 
> (with permanent pink markup) within 5 – 20 minutes of launching. My machine 
> has 12 virtual cores and 16 GB of memory. What could I be doing wrong?

What exactly is "my theory"? Is it already in some repository?


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] performance problems

[Lawrence Paulson]

I'm facing serious performance problems with the development version and I have 
no idea what's happening, though it may be connected with my settings. At the 
moment I am using

JEDIT_JAVA_OPTIONS64="-Xms2048m -Xmx8192m -Xss8m"
ML_OPTIONS="--minheap 3500"

(I'm not aware of any guidelines of what sort of settings are appropriate.)

My theory doesn't use the AFP and I have moved aside my components file, which 
refers to afp/devel. My theory imports nothing but Complex_Main. Yet still, 
Isabelle/jEdit takes on the order of a minute to launch, and freezes (with 
permanent pink markup) within 5 – 20 minutes of launching. My machine has 12 
virtual cores and 16 GB of memory. What could I be doing wrong?

In case it's relevant
~/isabelle/Repos/src/HOL: hg id
58bf801d679a tip


Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev