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


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 feature exist?

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


	Makarius






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