Re: [isabelle] Questions about speed and CPU usage
On Tue, 20 Jul 2010, Tambet wrote:
First thing is that on my computer, when Isabelle loads and processes
theories from lib, it almost hangs.
This indicates a low memory situation, i.e. the OS is swapping most of the
time. Can you give a few hardware figures? What is you OS platform
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?
When running Isabelle via Proof General / Emacs, the actual Isabelle
process is already running at a low priority ("nice" level > 0). This
does not help though, if you run out of physical memory (see above) or
Emacs is too busy processing prover output (e.g. traces of some automated
proof tools like "simp" or "auto").
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
You can work with persistent sessions, see section 1.2 in the Isabelle
System manual for some basic examples. Having created such a writable
logic image, you can tell Proof General to make use of it.
This is useful for really big development, but your applications are
probably much smaller at the moment. Which library theories did you try
to load anyway?
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?
This indicates that Emacs is busy. The Unix "top" utility will tell you.
In some denial-of-service situations on Emacs you can also send kill -INT
to the poly process.
Nothing like this should happen in small experiments with Isabelle,
though. Again it might be just a corollary of general memory shortage.
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).
Structured proofs also scale up to larger proofs, and are more efficiently
checked than old-style proof scripts. The reason why you don't see Isar
proofs everywhere is that it is usually harder to produce such nice
This archive was generated by a fusion of
Pipermail (Mailman edition) and