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 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.

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


      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 MHonArc.