On 11/07/2012 10:41 PM, Gerwin Klein wrote:
On 08/11/2012, at 8:26 AM, Florian
Haftmann<[email protected]> 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
