[isabelle-dev] log file where art thou?

[Makarius]

On Fri, 24 Aug 2012, Gerwin Klein wrote:

>> This should work: when the process has terminated in any way, the log 
>> should appear.  Where did you see it differently?
>
> No, I haven't encountered it yet. This may work just fine for polyml 
> crashes, because polyml is running on the inner level.
>
> It'll fail at the level of whatever process does the logging, though. 
> Maybe that level is much more robust, but anything that can fail will 
> fail eventually.

That is the JVM process, which is for quite some time already the standard 
layer for Isabelle system management.  This introduces certain biases how 
things are done, which are slightly different from the traditional 
bash/perl system glueing from the past.  The JVM can fail (I've seen 
that), but distrusting it like that sounds like the proverbial insurance 
against impacts of meteors.

Moreover, shared file system operations are critical by themselves. 
We've had so many NFS issues at TUM, far more than the JVM ever crashing. 
(The NFS arrangement of logs etc. is one of the main weaknesses of 
isatest.)  And on Windows shared files have a completely different 
semantics.  So this is not something you do just by default: one process 
writing another process reading to see what's happening.


> If it's easy to do I don't see why we should not stream 
> log files. Otherwise why have log files at all?
>
> I agree that multithreading makes the log files less valuable than they 
> were. Maybe they can be made more valuable again, though. For instance, 
> each log line could have thread number and time stamp -- then they can 
> be analysed better afterwards.

When I left the build/log aspect in a certain state some weeks ago, I've 
put exactly that question on my TODO list: Why have log files at all? 
There could be better ways to keep a record of the run of a session, 
including formal markup for loading into another session.

What you call thread number and time stamp above is conceptually already 
there in Isabelle for a long time, as part of the interactive document 
model of the Prover IDE -- although it is not as physical as threads or 
stamps.

Having incremental logs back as a retro feature on the spot would mean I 
have to spend time on that now, and later to dismantle it again, because 
it is something like a legacy feature.


Anyway.  How about getting the AFP build process up to date now? I have 
done most of your work already.


 	Makarius