[isabelle-dev] AFP devel broken (was AFP: Session AVL-Trees broken)
Maybe related: since at least 2 days I get an "Error 404" whenever I want to browse the theories of entries in the development version of the AFP. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP: Session AVL-Trees broken
On 08/11/2012, at 8:50 AM, Lukas Bulwahn wrote: > On 11/07/2012 10:41 PM, Gerwin Klein wrote: >> 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". Interesting, is your laptop swapping when the sessions fail? My guess is that this is a symptom of the machine being overloaded. When I was testing, I was running sessions one at a time, not in parallel, so I wouldn't have seen any issues with too many parallel jobs or similar. Does anyone know what the timeout measures? Elapsed real time or time spent on that session? The solution may be to just increase timeouts. On the other hand, this whole thing used to work just fine and started to go haywire 2012-10-19, then the log files are cut off in the middle at HOL-Probability (probably nonterminating, I guess these sessions should get a timeout too, the old setup was cumulative), HOL-Probality worked on 2012-10-26 (but then timeouts), then again stuck at HOL-Probability, and since 2012-10-28 mostly timeouts. Also: 13h elapsed time for 4:50h cpu time on 2012-10-30 and 9h elapsed time for 5:26h cpu time yesterday. These should be the other way around. It definitely looks like the machine is way overloaded. The afp test assumes it has the machine to itself and runs at 6:28 in the morning. It should be finished after about 3h. Looking at isatest logs, it looks like that test now reaches long into that time (mac-poly64-M8-2012-11-07-macbroy2 finished 7:32 and mac-poly-M8-2012-11-07-macbroy2 at 9:14, mac-poly-M4-2012-11-07-macbroy2 at 8:28). These seem to be starting way later than usual. I can either move the afp test to later, or whoever now feels in charge of isatest should have a look at moving that back to an earlier time. E.g. on 2012-10-15 when afp-test was still fine, mac-poly64-M8-2012-10-15-macbroy2 finished at 4:11 am. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP: Session AVL-Trees broken
On 11/07/2012 10:41 PM, Gerwin Klein wrote: On 08/11/2012, at 8:26 AM, Florian Haftmann 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP: Session AVL-Trees broken
On 08/11/2012, at 8:26 AM, Florian Haftmann 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP: Session AVL-Trees broken
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. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP: Session AVL-Trees broken
If I run sessions manually, they work fine, but they fail in the cron job with timeout (even small ones like Separation_Algebra). This has been going on for a while. Does anyone have an idea what's going on? Is there something else running on macbroy2 at the same time that takes a lot of resources? Cheers, Gerwin On 08/11/2012, at 7:32 AM, Florian Haftmann wrote: > Anybody any ideas what went wrong!? > > Florian > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] AFP: Session AVL-Trees broken
Anybody any ideas what went wrong!? Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
