Email Gateway (Aug 19 2022 at 14:12): 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
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:
The prover tries to work hard to give early feedback on the current
focus of the edit panel, e.g. leaving proofs unfinished in earlier
theories and so on. Thus the (expected) spots of problems get reported
quite late, and, after adjusting those spots, a lot of material which
follows afterwards has to be re-checked.
If existing proofs degenerate into non-termination, the risk is that
these spots will consume a lot of resources and turn Isabelle/jEdit
little reactive until the spots are identified and interrupted by hard
edits.
What works as workaround is to set the number of threads temporarily to
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
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:
Finding the error locations can be troublesome in big theories; somtimes the
presence of an error (in red) is only visible in the theory panel.
Adjusting the AFP frequently leads me into the follwing situation: I run
"afp_build -A"; there is an error in some entry; I fix the error; I restart
"afp_build -A"; isabelle (more precisely java) dies with some out of memory
error right away, sometimes blaming it on a corrupt log file. At this point I
need to remove all log files and rerun everything.
I believe both points have been discussed already but I have no idea if I can
avoid the problem with the AFP.
Tobias
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:
- Adjusting the AFP frequently leads me into the follwing situation: I run
"afp_build -A"; there is an error in some entry; I fix the error; I restart
"afp_build -A"; isabelle (more precisely java) dies with some out of memory
error right away, sometimes blaming it on a corrupt log file. At this point I
need to remove all log files and rerun everything.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: Nov 21 2024 at 12:39 UTC