Re: [isabelle] Questions about speed and CPU usage



On 21 July 2010 10:55, Peter Lammich <peter.lammich at 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
- because KDE obviously lets even things needed to move mouse cursor be
written to swap (maybe to have those fancy jumping full-colored cursors).

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.