[isabelle-dev] log file where art thou?

[Gerwin Klein]

On 25/08/2012, at 10:43 AM, Makarius wrote:

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

On a 10 year regression test time frame, JVM failures are fairly common, somewhere between OS and poly problems. Definitely worth having log files or other evidence survive them.


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

Sure, it's far from perfect and it might not work on Windows. It's still regularly provided me with valuable information in the past. Like a black box in a plane, it doesn't tell you everything, but it gives you some evidence to work with.


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

I'd have no problem with that.


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

Don't worry, I'll get to it when I return from leave in about 1 week. At the moment I'm restricted to writing annoying emails :-)

Gerwin