[isabelle-dev] log file where art thou?

Makarius makarius at sketis.net
Thu Aug 23 16:40:09 CEST 2012


On Thu, 23 Aug 2012, Makarius wrote:

> The main information was the progress of the theory loader, I usually 
> had something like "tail -f ... | grep Loading", but this is of limited 
> use since the main source of non-termination are proofs, and they come 
> later without correlation to what the theory loader said before.
>
> When redoing the build tool from scratch some weeks ago, I've already 
> considered to include some more formal progress in accordance to the 
> underlying model of Isabelle since 2008.

Another hint concerning progress: the "Prover Session" panel in 
Isabelle/jEdit has a very useful overview of the whole session.  Dark 
purple indicates hot spots where the system is running or potentially 
non-terminating.  Double-clicking on a theory node opens the corresponding 
file in the editor.


 	Makarius



More information about the isabelle-dev mailing list