Email Gateway (Aug 18 2022 at 15:41): Email Gateway (Aug 18 2022 at 15:41):From: Tambet <qtvali@gmail.com>
First thing is that on my computer, when Isabelle loads and processes
theories from lib, it almost hangs. It would be nice if my only goal was to
load those theories, but I would also like to read documentation meanwhile
and do notes. Is this possible to give it some numbers about how much it's
allowed to use memory, CPU and utilize hard drive speed at any given time?
It would be much better if moving mouse and opening PDF document was always
possible. It's not enough to change priority of emacs, because I would like
emacs to run full-speed meanwhile. Is there some option to make specific
processes lower-priority as much as needed so that computer works fast and
those processes use 100% of idle time, but max 50% of time I am using other
applications?
Also, can I precompile those libraries or cache that data, which is
generated and reusable? As much as I can understand it just goes through the
proving process and does something, what has zero-dependancy of the file I'm
editing; those libs also won't change often (and probably if they did, the
proofs of other files would still mostly hold). Does this feature exist?
One more speed-related question: usually the button to stop the current
activity does not work (if I run something, what takes very long, I just
have to kill emacs, which is not the best way to use a program and also
wastes a lot of time). Is there some way to easily stop things, which do not
work or were erroneously triggered?
Btw. I like the Structured Isar Proofs much more than that other one with
"apply" etc., because that actually allows me to consciously prove (at least
very simple) things whereas that other looks like randomly trying different
buttons in hope that they eventually do something [this was actually why I
switched to Isabelle after playing with Coq a few days that I saw that
manual and it's just nice]. Structured proofs is clearly at least a good
starting point, but this goal-based way is nice in many ways (I wish that
most library proofs were built in that way).
Tambet
Email Gateway (Aug 18 2022 at 15:42):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all.
I have a related Problem with the new 2009-2 release.
While 1GiB of RAM have always been enough for the 2009-1 release,
the new version very quickly allocates more than 1GiB, and starts thrashing.
Switching of "parallel proofs" makes things a bit better, but still my
computer is nearly unusable
during running larger proofs.
Have you changed any memory-related configurations in the new release, and
is it possible to set them back again?
Best Peter
Tambet wrote:
Email Gateway (Aug 18 2022 at 15:42):From: Makarius <makarius@sketis.net>
Initial heap size of Poly/ML is configured by ML_OPTIONS="-H 200", which
is the same default as for Isabelle2009-2. The options for parallel
checking are also the same.
What did change in Isabelle2009-2 is the overall bloat factor of main
Isabelle/HOL. With as little as 1 GB it is unlikely that you will be able
to process big sessions.
Makarius
Email Gateway (Aug 18 2022 at 15:42):From: Tobias Nipkow <nipkow@in.tum.de>
Since you are still learning, you might also be interested in the slides
of my Isabelle course:
http://isabelle.in.tum.de/coursematerial/PSV2009-1/index.html
It starts off with "apply" but later it introduces structured proofs
through proof patterns that may help.
Tobias
Email Gateway (Aug 18 2022 at 15:42):From: Makarius <makarius@sketis.net>
On Tue, 20 Jul 2010, Tambet wrote:
First thing is that on my computer, when Isabelle loads and processes
theories from lib, it almost hangs.
This indicates a low memory situation, i.e. the OS is swapping most of the
time. Can you give a few hardware figures? What is you OS platform
anyway?
It's not enough to change priority of emacs, because I would like emacs
to run full-speed meanwhile. Is there some option to make specific
processes lower-priority as much as needed so that computer works fast
and those processes use 100% of idle time, but max 50% of time I am
using other applications?
When running Isabelle via Proof General / Emacs, the actual Isabelle
process is already running at a low priority ("nice" level > 0). This
does not help though, if you run out of physical memory (see above) or
Emacs is too busy processing prover output (e.g. traces of some automated
proof tools like "simp" or "auto").
Also, can I precompile those libraries or cache that data, which is
generated and reusable? As much as I can understand it just goes through
the proving process and does something, what has zero-dependancy of the
file I'm editing; those libs also won't change often (and probably if
they did, the proofs of other files would still mostly hold). Does this
feature exist?
You can work with persistent sessions, see section 1.2 in the Isabelle
System manual for some basic examples. Having created such a writable
logic image, you can tell Proof General to make use of it.
This is useful for really big development, but your applications are
probably much smaller at the moment. Which library theories did you try
to load anyway?
One more speed-related question: usually the button to stop the current
activity does not work (if I run something, what takes very long, I just
have to kill emacs, which is not the best way to use a program and also
wastes a lot of time). Is there some way to easily stop things, which do
not work or were erroneously triggered?
This indicates that Emacs is busy. The Unix "top" utility will tell you.
In some denial-of-service situations on Emacs you can also send kill -INT
to the poly process.
Nothing like this should happen in small experiments with Isabelle,
though. Again it might be just a corollary of general memory shortage.
Btw. I like the Structured Isar Proofs much more than that other one
with "apply" etc., because that actually allows me to consciously prove
(at least very simple) things whereas that other looks like randomly
trying different buttons in hope that they eventually do something [this
was actually why I switched to Isabelle after playing with Coq a few
days that I saw that manual and it's just nice]. Structured proofs is
clearly at least a good starting point, but this goal-based way is nice
in many ways (I wish that most library proofs were built in that way).
Structured proofs also scale up to larger proofs, and are more efficiently
checked than old-style proof scripts. The reason why you don't see Isar
proofs everywhere is that it is usually harder to produce such nice
proofs.
Makarius
Email Gateway (Aug 18 2022 at 15:44):From: Tambet <qtvali@gmail.com>
On 21 July 2010 12:59, Tobias Nipkow <nipkow@in.tum.de> wrote:
Since you are still learning, you might also be interested in the slides
of my Isabelle course:
http://isabelle.in.tum.de/coursematerial/PSV2009-1/index.html
It starts off with "apply" but later it introduces structured proofs
through proof patterns that may help.
Yes I am. I will go into it right now :) It's clearly self-explaining.
Tobias
Thanks,
Tambet
Email Gateway (Aug 18 2022 at 15:44):From: Tambet <qtvali@gmail.com>
On 21 July 2010 10:55, Peter Lammich <peter.lammich@uni-muenster.de> wrote:
Hi all.
I have a related Problem with the new 2009-2 release.
While 1GiB of RAM have always been enough for the 2009-1 release,
the new version very quickly allocates more than 1GiB, and starts
thrashing.
Switching of "parallel proofs" makes things a bit better, but still my
computer is nearly unusable
during running larger proofs.
I am happy to report that after installing XFCE and logging in, it became
extremely fast - things I used to wait 1-20 minutes for happened in moments
or a few seconds. I can now even scroll PDF manuals when Emacs Proof
General is running, which completely changes the whole experience ;)
As KDE normal install (with no programs working) takes 530MB of memory, but
XFCE takes 370 - based on
http://www.phoronix.com/scan.php?page=article&item=linux_desktop_vitals&num=1-,
they might have such properties:
- Say that you use 200MB of memory for normal background processes -
Firefox and PDF reader.
- Say that Proof General takes some 200MB (I measured that it reaches
that point very fast).
- Then, XFCE takes 370, which means 770 in total.
- KDE takes 530, which makes 930 in total.
- http://manual.sidux.com/en/cd-content-en.htm shows that this memory
requirement of KDE can get even worse - looking recommended numbers the
difference could be as much as four times in worse case.
For me, the difference was fatal - when nothing did response before (I was
making coffee when waiting switch from Firefox window to Emacs window or
vice versa after I had ran anything proof-related for once - and this
speeddown was somewhat in effect until reboot), in XFCE it's just working.
It might also be that XFCE is better at memory management of critical things
So, maybe it works for you, too :)
[I wouldn't actually believe that the difference is so big, it was just a
last resort after replacing several other programs with more lightweight
versions and turning some less-needed functionality off]
Have you changed any memory-related configurations in the new release, and
is it possible to set them back again?
Best Peter
Tambet wrote:
First thing is that on my computer, when Isabelle loads and processes
theories from lib, it almost hangs. It would be nice if my only goal was
to
load those theories, but I would also like to read documentation
meanwhile
and do notes. Is this possible to give it some numbers about how much
it's
allowed to use memory, CPU and utilize hard drive speed at any given
time?
It would be much better if moving mouse and opening PDF document was
always
possible. It's not enough to change priority of emacs, because I would
like
emacs to run full-speed meanwhile. Is there some option to make specific
processes lower-priority as much as needed so that computer works fast
and
those processes use 100% of idle time, but max 50% of time I am using
other
applications?Also, can I precompile those libraries or cache that data, which is
generated and reusable? As much as I can understand it just goes through
the
proving process and does something, what has zero-dependancy of the file
I'm
editing; those libs also won't change often (and probably if they did,
the
proofs of other files would still mostly hold). Does this feature exist?One more speed-related question: usually the button to stop the current
activity does not work (if I run something, what takes very long, I just
have to kill emacs, which is not the best way to use a program and also
wastes a lot of time). Is there some way to easily stop things, which do
not
work or were erroneously triggered?Btw. I like the Structured Isar Proofs much more than that other one with
"apply" etc., because that actually allows me to consciously prove (at
least
very simple) things whereas that other looks like randomly trying
different
buttons in hope that they eventually do something [this was actually why
I
switched to Isabelle after playing with Coq a few days that I saw that
manual and it's just nice]. Structured proofs is clearly at least a good
starting point, but this goal-based way is nice in many ways (I wish that
most library proofs were built in that way).Tambet
Last updated: Nov 21 2024 at 12:39 UTC