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

[Gerwin Klein]

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)

AVL-Trees FAILED
(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.

Cheers,
Gerwin