[isabelle-dev] log file where art thou?

[Makarius]

On Thu, 23 Aug 2012, Lawrence Paulson wrote:

> Agree. I often looked at these. Though they can be confusing in the presence of multi-threading.

Right. I used to look at them until 5 years ago, when sequentialism was 
discontinued.  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.  I did not get to that so far, 
because other things sucked up a lot of time (such as doc-src and AFP, 
which are both not fully finished yet).


> On 23 Aug 2012, at 14:20, Gerwin Klein wrote:
>
>> I'd be quite keen to get the old behaviour back.

That is the wrong attitude.

I've invested a lot of time to get beyond the state of the art from 16 
years ago.  Since it is based on completely different technology it is 
natural that certain accidental behaviour from the past is no longer 
available by other accidental side conditions.


 	Makarius