[isabelle-dev] AFP: Session AVL-Trees broken

Gerwin Klein 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 ...
*** Timeout
(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")
(real error)

Running BDD ...
*** Timeout
Running Circus ...
*** Timeout
Running Stream-Fusion ...
*** Timeout
Running Tycon ...
*** Timeout
Running Valuation ...
*** Timeout
Running Girth_Chromatic ...
*** Timeout
Running Abortable_Linearizable_Modules ...
*** Timeout
Running AutoFocus-Stream ...
*** Timeout
Running PCF ...
*** Timeout
Running Shivers-CFA ...
*** Timeout
Running Markov_Models ...
*** Timeout
Running WorkerWrapper ...
*** Timeout

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 mailing list