[isabelle-dev] AFP: Session AVL-Trees broken
kleing at cse.unsw.edu.au
Wed Nov 7 22:41:32 CET 2012
On 08/11/2012, at 8:26 AM, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> Am 07.11.2012 22:22, schrieb Gerwin Klein:
>> If I run sessions manually, they work fine, but they fail in the cron job with timeout (even small ones like Separation_Algebra).
> In the case of AVL-Trees, it fails interactively (i.e. fails in the
> stricter sense), at proofs seeming inherently difficult.
There are bound to be some real errors in the noise after some time..
On this one we got:
Building Refine_Monadic ...
(but manages to finish the larger JinjaThreads)
(see also /home/isatest/afp/isabelle-afp-poly/heaps/polyml-5.5.0_x86-darwin/log/AVL-Trees)
*** Bad certificate cache: missing certificate
*** At command "by" (line 169 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/AVL-Trees/AVL.thy")
Running BDD ...
Running Circus ...
Running Stream-Fusion ...
Running Tycon ...
Running Valuation ...
Running Girth_Chromatic ...
Running Abortable_Linearizable_Modules ...
Running AutoFocus-Stream ...
Running PCF ...
Running Shivers-CFA ...
Running Markov_Models ...
Running WorkerWrapper ...
I can see no reason why any of these would have to time out, and they don't on other machines (I've only tried some, though, not all).
Could it be an artefact of time measurement on macbroy 2 or something like that? Too many jobs in parallel? It doesn't seem to be very deterministic either, there are different sessions failing at different times.
More information about the isabelle-dev