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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
