Re: [isabelle-dev] Datatypes & Isatest failures
On Thu, 25 Sep 2014, Makarius wrote: HOL-Proofs is important in various ways: theoretically it opens the possibility for independent checking of proofs by a different system, and thus raising the level of confidence in Isabelle results; practically it indicates how close we are to the next concrete wall of resource limits. Moreover, Poly/ML 5.3.0 is still important, since it has more thorough exception trace, which is required in hard cases of ML diagnostics. We've had such unclear situations occasionally in the past, and usually managed to get things under control again, after looking 2 or 3 times more closely. Softening concrete walls has always been a routine trick in long-term Isabelle maintenance. After some experiments this morning, my impression is that there is nothing special, just a very old test machine. I have changed that in ab4b94892c4c, so lets hope for the best for tomorrow's isatest run. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Datatypes & Isatest failures
On Thu, 25 Sep 2014, Jasmin Christian Blanchette wrote: Hi Florian, Thanks for your input. 1. Increase the timeout from 3600 s to, e.g. 4800. [...] So, (1) is my opinion. Unfortunately, that didn't do the trick (cf. 7f30ec82fe40, e4d540c0dd57). The change e4d540c0dd57 was my reaction in the sense of (1) -- although I am presently not quite up-to-date concerning open threads and this particular situation. HOL-Proofs is important in various ways: theoretically it opens the possibility for independent checking of proofs by a different system, and thus raising the level of confidence in Isabelle results; practically it indicates how close we are to the next concrete wall of resource limits. Moreover, Poly/ML 5.3.0 is still important, since it has more thorough exception trace, which is required in hard cases of ML diagnostics. We've had such unclear situations occasionally in the past, and usually managed to get things under control again, after looking 2 or 3 times more closely. Softening concrete walls has always been a routine trick in long-term Isabelle maintenance. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Datatypes & Isatest failures
Hi Florian,
Thanks for your input.
>> 1. Increase the timeout from 3600 s to, e.g. 4800.
[...]
> So, (1) is my opinion.
Unfortunately, that didn't do the trick (cf. 7f30ec82fe40, e4d540c0dd57).
Judging from the log file, it would appear to me that it's an instance of
multithreading divergence, as we have sometimes witnessed. The last theory
being loaded is also the main one ("Old_Datatype.thy", loaded right after
"Main.thy" now for "HOL-Proofs.thy" -- or "Main.thy" until one week ago.) The
very last timing information is about some lemmas that are quite early in the
dependency graphs (e.g. in "Hilbert_Choice.thy"). The last timings look
reasonable, i.e. milliseconds.
Change be0f5d8d511b still appears to have been the one that triggered the issue
-- unless there has been some hardware or software changes on the server on the
same day. In principle, it should change nothing for "Main" -- it is
generalizing some code so that recursion is possible through phantom type
variables, as necessary for Imperative HOL.
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Datatypes & Isatest failures
> It doesn't seem like "subst_tac" had anything to do with it. I still have no > idea about what made "HOL-Proofs" slower on "at-poly-e" beween September 13 > and 14. The log reveals nothing special, except a truncation at the end. > (while processing "Predicate.thy"). My personal inclination would be to > disable this test for this platform -- "HOL-Proofs" isn't exactly used by > many people, and I'm not sure there's much value in running CPUs for 1 hour > each night to test it on some slow hardware and old version of Poly/ML (5.3). > > I see the following options as relatively painless ways of solving this: > > 1. Increase the timeout from 3600 s to, e.g. 4800. Could be. > 2. Make "HOL-Proofs" and dependencies "ISABELLE_FULL_TEST". Definitely not. HOL-Proofs is am important indicator whether something got utterly wrong in handling of thm values in Pure. (Or would you like JinjaThreads depend on ISABELLE_FULL_TEST also ;-)?) > 3. Introduce another condition to control whether "HOL-Proofs" should be > built. The pain of introducting another condition seems bigger to me than to raise the timeout. > Does anybody have an opinion? So, (1) is my opinion. 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] Datatypes & Isatest failures
A fantastic achievement! --lcp > On 19 Sep 2014, at 09:26, Dmitriy Traytel wrote: > >> On 17.09.2014 11:40, Jasmin Christian Blanchette wrote: >> There are only a handful of "old_datatype"s left in the AFP, and they will >> go away as soon as Dmitriy gets a chance to fix a bug in his code >> (presumably once he's back from vacation). > It is now (isabelle/7b92932ffea5) fixed, and the "old_datatype"s are gone > from the AFP (AFP/5bda5332b484). > > Dmitriy > ___ > 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
Re: [isabelle-dev] Datatypes & Isatest failures
On 17.09.2014 11:40, Jasmin Christian Blanchette wrote: There are only a handful of "old_datatype"s left in the AFP, and they will go away as soon as Dmitriy gets a chance to fix a bug in his code (presumably once he's back from vacation). It is now (isabelle/7b92932ffea5) fixed, and the "old_datatype"s are gone from the AFP (AFP/5bda5332b484). Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Datatypes & Isatest failures
Hi again, Am 17.09.2014 um 11:40 schrieb Jasmin Christian Blanchette : > 1. "HOL-Proofs" times out since September 14 on "at-poly-e". On September 13, > we had > >Timing HOL-Proofs (2 threads, 3161.882s elapsed time, 2889.329s cpu time, > 840.167s GC time, factor 0.91) >Finished HOL-Proofs (0:54:37 elapsed time, 0:48:53 cpu time, factor 0.89) > > which is close to the timeout (1 hour, I believe) but not *that* close. > Still, the failures on September 14, 15, 16, and 17 have been consistent > enough to suggest that change be0f5d8d511b (the only relevant one between > Sept. 13 and 14) is the cause, in which case I have a strong suspicion about > "subst_tac". It doesn't seem like "subst_tac" had anything to do with it. I still have no idea about what made "HOL-Proofs" slower on "at-poly-e" beween September 13 and 14. The log reveals nothing special, except a truncation at the end. (while processing "Predicate.thy"). My personal inclination would be to disable this test for this platform -- "HOL-Proofs" isn't exactly used by many people, and I'm not sure there's much value in running CPUs for 1 hour each night to test it on some slow hardware and old version of Poly/ML (5.3). I see the following options as relatively painless ways of solving this: 1. Increase the timeout from 3600 s to, e.g. 4800. 2. Make "HOL-Proofs" and dependencies "ISABELLE_FULL_TEST". 3. Introduce another condition to control whether "HOL-Proofs" should be built. Does anybody have an opinion? Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Datatypes & Isatest failures
Hi all, The good news is that the port to the new datatypes have been overall a success. There are only a handful of "old_datatype"s left in the AFP, and they will go away as soon as Dmitriy gets a chance to fix a bug in his code (presumably once he's back from vacation). Also good news: Timing information as I could see it show no big impact on the AFP, e.g. JinjaThread. Although the new package is much more efficient in its handling of nested recursion, it is generally heavier due to its reliance on local theories and on the BNF composition pipeline -- thankfully not too much heavier, as far as I could tell so far. The bad news is that we've been experiencing Isatest failures since then. Let me classify them: 1. "HOL-Proofs" times out since September 14 on "at-poly-e". On September 13, we had Timing HOL-Proofs (2 threads, 3161.882s elapsed time, 2889.329s cpu time, 840.167s GC time, factor 0.91) Finished HOL-Proofs (0:54:37 elapsed time, 0:48:53 cpu time, factor 0.89) which is close to the timeout (1 hour, I believe) but not *that* close. Still, the failures on September 14, 15, 16, and 17 have been consistent enough to suggest that change be0f5d8d511b (the only relevant one between Sept. 13 and 14) is the cause, in which case I have a strong suspicion about "subst_tac". I will investigate. Yesterday I tried something, but it had no effect. Due to the "liveness" flavor of the bug, it may still take some rounds to nail it down. (Building "HOL-Proofs" takes 4.5 minutes on my laptop, so it's not as if I could easily reproduce the problem locally.) 2. "HOL-Datatype_Examples" causes random problems on random platforms. Today there was a timeout on "at-poly-e", which I cannot really explain. 3. Freak errors, e.g. crash in "HOL-Decision_Procs". These appear unrelated to my changes, and we had those before already. Bottom line: I'm working on it. If you have ideas/suggestions on how to help this converge faster, please let me know. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
