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

[Lukas Bulwahn]

On 11/07/2012 10:41 PM, Gerwin Klein wrote:
> 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)
> 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.
I can confirm that the AVL-Tree certification errors are real and the 
timeouts occur nondeterministically even on my laptop, when running 
"afp_build -A".
Other than that, I am not aware of any other errors in the AFP.

By the way, I cannot use mira on lxbroy1 to test the current tip, as 
mira does not update the repository for some strange reason.

Lukas