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) 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
