Re: [isabelle] Questions about speed and CPU usage



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