[isabelle-dev] log file where art thou?
makarius at sketis.net
Sat Aug 25 10:43:04 CEST 2012
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
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.
More information about the isabelle-dev