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
