[isabelle-dev] log file where art thou?

[Gerwin Klein]

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

> On Thu, 23 Aug 2012, Gerwin Klein wrote:
> 
>> left at least some information in the case of bad system crashes (e.g. polyml bugs).
> 
> 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. 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.

Gerwin