Re: [isabelle] What may Isabelle be doing behind my back?
On Tue, 5 Jan 2010, Andrei Popescu wrote:
I am using Isabelle2009-1 with emacs22-gtk, admittedly in a very poor
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.
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 -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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and