Re: [isabelle-dev] Fwd: isabelle test failed
Something exceptional has happened: isatest finished successfully, without any problems of the various (old) testing machines. See also http://isabelle.in.tum.de/devel Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: isabelle test failed
On Mon, 13 Jul 2015, Makarius wrote: Hopefully we can not return to isatest runs that work routinely. But we also need to revisit the actual problem eventually. This should read as Hopefully we can *now* return ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: isabelle test failed
On Fri, 26 Jun 2015, Makarius wrote: On Fri, 26 Jun 2015, Larry Paulson wrote: HOL-Proofs, etc., have been failing for several days now. Last time I checked, it was simply a timeout. Presumably some change to rewriting is to blame. It may be similar to the AFP failure that I fixed yesterday. Is anyone familiar with this entry? I've made some manual tests just yesterday and then produced the following change: changeset: 60574:915da29bf5d9 user:wenzelm date:Thu Jun 25 22:56:33 2015 +0200 files: Admin/isatest/settings/at64-poly description: more heap -- hoping for more stability of HOL-Proofs; The isatest from tonight did not see that yet, because I pushed it too late after midnight. Maybe the next test run works. The deeper reason why HOL-Proofs takes much longer now is this: The first bad revision is: changeset: 60046:894d6d863823 user:traytel date:Mon Apr 13 13:03:41 2015 +0200 summary: call Goal.prove only once for a quadratic number of theorems I did not find time yet, to look more closely what is behind that. Generally, proof term performance is bad for massive amounts of goals with Pure.conjunction. I've had a discussion about that around 2008 with Stefan Berghofer, but he could not explain it, nor improve the situation. More generally, HOL-Proofs always serves as a reminder of invisible concrete walls concerning limited CPU resources. Growth cannot just continue forever, one day it will come to a grinding halt. (Despite that triviality, I have already some ideas to reduce resource usage once again, so that the meltdown might be postponed.) After more manual tests, the conclusion is that there is presently no hope to finish HOL-Proofs on x86_64 platform in reasonable time. This temporary defeat is formalized here: changeset: 60713:5240b2ed5189 tag: tip user:wenzelm date:Mon Jul 13 11:05:50 2015 +0200 summary: refrain from testing HOL-Proofs for x86_64-linux: takes more than 4h; Hopefully we can not return to isatest runs that work routinely. But we also need to revisit the actual problem eventually. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: isabelle test failed
On Fri, 26 Jun 2015, Makarius wrote: On Fri, 26 Jun 2015, Larry Paulson wrote: HOL-Proofs, etc., have been failing for several days now. Last time I checked, it was simply a timeout. Presumably some change to rewriting is to blame. It may be similar to the AFP failure that I fixed yesterday. Is anyone familiar with this entry? I've made some manual tests just yesterday and then produced the following change: changeset: 60574:915da29bf5d9 user:wenzelm date:Thu Jun 25 22:56:33 2015 +0200 files: Admin/isatest/settings/at64-poly description: more heap -- hoping for more stability of HOL-Proofs; The isatest from tonight did not see that yet, because I pushed it too late after midnight. Maybe the next test run works. The deeper reason why HOL-Proofs takes much longer now is this: The first bad revision is: changeset: 60046:894d6d863823 user:traytel date:Mon Apr 13 13:03:41 2015 +0200 summary: call Goal.prove only once for a quadratic number of theorems I did not find time yet, to look more closely what is behind that. There is another rather profane performance problem in the test machine lxbroy2: a strange process is sucking up CPU cycles for a long time. As evasive maneuver I've moved the crontab to lxbroy3 (see 22830a64358f). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: isabelle test failed
On Fri, 26 Jun 2015, Larry Paulson wrote: HOL-Proofs, etc., have been failing for several days now. Last time I checked, it was simply a timeout. Presumably some change to rewriting is to blame. It may be similar to the AFP failure that I fixed yesterday. Is anyone familiar with this entry? I've made some manual tests just yesterday and then produced the following change: changeset: 60574:915da29bf5d9 user:wenzelm date:Thu Jun 25 22:56:33 2015 +0200 files: Admin/isatest/settings/at64-poly description: more heap -- hoping for more stability of HOL-Proofs; The isatest from tonight did not see that yet, because I pushed it too late after midnight. Maybe the next test run works. The deeper reason why HOL-Proofs takes much longer now is this: The first bad revision is: changeset: 60046:894d6d863823 user:traytel date:Mon Apr 13 13:03:41 2015 +0200 summary: call Goal.prove only once for a quadratic number of theorems I did not find time yet, to look more closely what is behind that. Generally, proof term performance is bad for massive amounts of goals with Pure.conjunction. I've had a discussion about that around 2008 with Stefan Berghofer, but he could not explain it, nor improve the situation. More generally, HOL-Proofs always serves as a reminder of invisible concrete walls concerning limited CPU resources. Growth cannot just continue forever, one day it will come to a grinding halt. (Despite that triviality, I have already some ideas to reduce resource usage once again, so that the meltdown might be postponed.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: isabelle test failed
Oops, I didn't expect my name to appear here ;-) The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report [1]. With turned off proofs the effect was a good one. What is special about Pure.conjunction w.r.t. proof reconstruction? Is it something in Goal.conjunction_tac? Would you advise to use HOL's conjunction instead? Dmitriy [1] https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-April/005986.html On 26.06.2015 20:01, Makarius wrote: On Fri, 26 Jun 2015, Larry Paulson wrote: HOL-Proofs, etc., have been failing for several days now. Last time I checked, it was simply a timeout. Presumably some change to rewriting is to blame. It may be similar to the AFP failure that I fixed yesterday. Is anyone familiar with this entry? I've made some manual tests just yesterday and then produced the following change: changeset: 60574:915da29bf5d9 user:wenzelm date:Thu Jun 25 22:56:33 2015 +0200 files: Admin/isatest/settings/at64-poly description: more heap -- hoping for more stability of HOL-Proofs; The isatest from tonight did not see that yet, because I pushed it too late after midnight. Maybe the next test run works. The deeper reason why HOL-Proofs takes much longer now is this: The first bad revision is: changeset: 60046:894d6d863823 user:traytel date:Mon Apr 13 13:03:41 2015 +0200 summary: call Goal.prove only once for a quadratic number of theorems I did not find time yet, to look more closely what is behind that. Generally, proof term performance is bad for massive amounts of goals with Pure.conjunction. I've had a discussion about that around 2008 with Stefan Berghofer, but he could not explain it, nor improve the situation. More generally, HOL-Proofs always serves as a reminder of invisible concrete walls concerning limited CPU resources. Growth cannot just continue forever, one day it will come to a grinding halt. (Despite that triviality, I have already some ideas to reduce resource usage once again, so that the meltdown might be postponed.) Makarius ___ 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] Fwd: isabelle test failed
On Sat, 27 Jun 2015, Dmitriy Traytel wrote: Oops, I didn't expect my name to appear here ;-) The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report [1]. With turned off proofs the effect was a good one. What is special about Pure.conjunction w.r.t. proof reconstruction? Is it something in Goal.conjunction_tac? Would you advise to use HOL's conjunction instead? I don't know if there is a difference between Pure and HOL. We could ask Stefan Berghofer, or just check empirically. The question arose first in 2007/2008 when Alex Krauss introduced many multi-goals in the function package. I can't say on the spot if/how that was addressed, or rather worked-around. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Fwd: isabelle test failed
This may be similar to the recent AFP failure: /mnt/home/isatest/isadist/Isabelle_15-Oct-2011/lib/scripts/run-polyml: line 77: 13186 Aborted $POLY -q $ML_OPTIONS HOL-MicroJava FAILED (see also /home/isatest/isabelle-at64-poly/heaps/polyml-5.2.1_x86_64-linux/log/HOL-MicroJava) Does anyone see a problem with updating that test to use poly-5.4.1? Cheers, Gerwin Begin forwarded message: From: isat...@macbroy28.informatik.tu-muenchen.de (Account Isatest) Date: 15 October 2011 5:01:01 PM AEDT To: kle...@cse.unsw.edu.au Subject: isabelle test failed Test for platform at64-poly failed. Log file attached. [...] 3:12:31 elapsed time, 4:33:07 cpu time, factor 1.41 Logics HOL FAILED! --- test FAILED --- Sat Oct 15 03:37:05 CEST 2011 --- macbroy24 Have a nice day, isatest ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: isabelle test failed
On Sat, 15 Oct 2011, Gerwin Klein wrote: This may be similar to the recent AFP failure: /mnt/home/isatest/isadist/Isabelle_15-Oct-2011/lib/scripts/run-polyml: line 77: 13186 Aborted $POLY -q $ML_OPTIONS HOL-MicroJava FAILED (see also /home/isatest/isabelle-at64-poly/heaps/polyml-5.2.1_x86_64-linux/log/HOL-MicroJava) Does anyone see a problem with updating that test to use poly-5.4.1? In principle you are the one main responsible for isatest, although I did most of the recent updates. The collective isatest/settings somehow need to cover the officially Poly/ML versions: isatest/settings/afp-poly: ML_SYSTEM=polyml-5.4.0 isatest/settings/at64-poly: ML_SYSTEM=polyml-5.2.1 isatest/settings/at-poly: ML_SYSTEM=polyml-5.3.0 isatest/settings/at-poly-test: ML_SYSTEM=polyml-5.4.2 isatest/settings/at-sml-dev-e:ML_SYSTEM=smlnj isatest/settings/cygwin-poly-e: ML_SYSTEM=polyml-5.4.2 isatest/settings/mac-poly: ML_SYSTEM=polyml-5.2.1 isatest/settings/mac-poly64-M2: ML_SYSTEM=polyml-5.4.0 isatest/settings/mac-poly64-M4: ML_SYSTEM=polyml-5.4.2 isatest/settings/mac-poly64-M8: ML_SYSTEM=polyml-5.4.2 isatest/settings/mac-poly-M2: ML_SYSTEM=polyml-5.4.0 isatest/settings/mac-poly-M4: ML_SYSTEM=polyml-5.4.0 isatest/settings/mac-poly-M8: ML_SYSTEM=polyml-5.4.0 Here 5.4.2 means some SVN version according to the accidental state of /home/polyml/polyml-svn at TUM. I now realize that I've missed the release of polyml-5.4.1 from this summer, otherwise I had shipped that with the Isabelle release. So for the moment the main obstable for switching at64-poly to 5.4.1 is the lack of an installation in /home/polyml which I will produce soon. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: isabelle test failed
On Sat, 15 Oct 2011, Makarius wrote: So for the moment the main obstable for switching at64-poly to 5.4.1 is the lack of an installation in /home/polyml which I will produce soon. See now Isabelle/22ff7e226946. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: isabelle test failed
On 16/10/2011, at 2:02 AM, Makarius wrote: On Sat, 15 Oct 2011, Makarius wrote: So for the moment the main obstable for switching at64-poly to 5.4.1 is the lack of an installation in /home/polyml which I will produce soon. See now Isabelle/22ff7e226946. Thanks. I'd have been happy to update it, I was just asking if anyone is relying on at-poly pointing to 5.4.1. In any case, this looks all good now. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
