[isabelle] Questions about speed and CPU usage



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.