Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] »strict« or »sequential« mode in Isabelle/jEdit?


view this post on Zulip Email Gateway (Aug 19 2022 at 14:12):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This should fit my purpose, thanks.

Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 14:18):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
During fine-point tuning of a huge bunch of theories (e.g.
Multivariate_Analysis / Probability in Isabelle/HOL), I am often in the
situation to incrementally adjust the sources following the error
reporting of Isabelle/jEdit (e.g. adding a simp rule and adjusting
subsequent broken proofs).

In this particular situation I experience two inconveniences with
continuous proof checking »as it is« in Isabelle/jEdit:

What works as workaround is to set the number of threads temporarily to

  1. Beside the comparably deep path through GUI elements for switching
    back and forth, parallelism (e.g. wrt. complete theories) is entirely lost.

I'm not sure how relevant this is (how do other people experience such
situations?), but maybe there is a different approach to the whole
scenaio which so far did not come to my mind.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 14:18):

From: Tobias Nipkow <nipkow@in.tum.de>
The points reported by Florian trouble me less than the following, of which
only the first relates to jedit, but both relate to maintenance:

I believe both points have been discussed already but I have no idea if I can
avoid the problem with the AFP.

Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 14:27):

From: Tobias Nipkow <nipkow@in.tum.de>
On 22/04/2014 16:09, Makarius wrote:

On Sun, 13 Apr 2014, Tobias Nipkow wrote:

You need to remove only the log file that is in the way, but that is still a bit
awkward.

Maybe you just have the default ISABELLE_BUILD_JAVA_OPTIONS, which are meant to
work on most systems without any bad surprise about JVM startup failure due to
lack of address space. (The situation is complicated by having to guess at
total heap space and individual thread stack space.)

To allow heavy-duty AFP maintenance, I use something like this in
$ISABELLE_HOME_USER/etc/settings:

ISABELLE_BUILD_JAVA_OPTIONS="-Xmx4096m -Xss1m"

or like this:

ISABELLE_BUILD_JAVA_OPTIONS="-Xmx4096m -Xss2m"

I currently have what you had sent me some time ago:

JEDIT_JAVA_OPTIONS="-Xms256m -Xmx4096m -Xss2m -Dactors.corePoolSize=8
-Dactors.enableForkJoin=false"

Is the above ISABELLE_BUILD_JAVA_OPTIONS independent to that, or does one imply
the other?

Tobias

Makarius


Last updated: Mar 28 2024 at 08:18 UTC