Email Gateway (Aug 18 2022 at 14:28): Email Gateway (Aug 18 2022 at 14:28):From: Andrei Popescu <uuomul@yahoo.com>
I am using Isabelle2009-1 with emacs22-gtk, admittedly in a very poor environment:
Ubuntu 8.10
Intel(R) Core(TM) 2 CPU T5500 @ 1.66 Ghz
Memory: 493.2 MiB
Free disk space: 69 MiB
(I only use Ubuntu on a small disk partition)
The problem is that occasionally Isabelle takes a very long time while performing operations such as moving to a new theory or theorem or digesting a new definition, and I don't know what she is really doing then. (By a long time, I mean minutes, and sometimes tens of minutes.)
This tends to occur more often when I am trying to process whole buffers, when Isabelle takes 10-15-minute breaks from time to time.
I also noticed that when I set AutoQuickCheck, AutoSolve and ParallelProofs off, such problems occur less often, but still do.
Also, the problem seems to increase with the size of the graph of theories on which the current theory depends on, but has a large degree of randomness. I did not have these problems with the previous release.
A related problem is that trying to run a (large-enough) session takes forever.
I shall eventually get a better computer system, but until then I would really like to survive with what I have here. (Notice also that my disk status does not really allow me to install new things.) Help!
Best regards,
Andrei
Email Gateway (Aug 18 2022 at 14:31):From: Tobias Nipkow <nipkow@in.tum.de>
AutoQuickCheck and AutoSolve only come into effect when you execute a
theory step by step. If you load a whole theory, they are disabled.
Tobias
Andrei Popescu wrote:
Email Gateway (Aug 18 2022 at 14:33):From: Makarius <makarius@sketis.net>
I would say this is just a consequence the natural growth of a system over
time, which is also known as "bloat". The long delays might be due to
swapping virtual memory on hard disk. Using "top" in a text terminal
should tell you if the main fault is due to Isabelle itself (cf. the
"poly" process) or Proof General (cf. the "emacs" process).
You can recover some disk space as follows:
* Reduce Isabelle2009-1/contrib/polyml-5.3.0 to the bare minimum,
keeping only the x86-linux subdirectory (saves about 70 MB).
* Rebuild the HOL logic image without proof terms, or build the more
frugal HOL-Main image instead, like this:
Isabelle2009-1/build HOL
or
Isabelle2009-1/build HOL -m HOL-Main
This should save 20-40 MB; see the Isabelle2009-1/heaps directory.
You can also delete the Pure image after building, to save a few MBs.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC