[isabelle-dev] log file where art thou?

[Gerwin Klein]

On 23/08/2012, at 4:40 PM, Makarius wrote:

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

I know, but I'm talking about sessions that run for 6h. If they take 8h, I'd like to be able to see roughly where they are stuck, preferably on the same day, so I can skip proofs to that point and investigate. Even with concurrency I can usually figure out which set of theories is currently running (and some big sessions run with -p 1 anyway to reduce memory usage).

Gerwin