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
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
On 17.09.2014 11:40, Jasmin Christian Blanchette wrote: There are only a handful of old_datatypes 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_datatypes 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 jasmin.blanche...@gmail.com: 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_datatypes 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
