[isabelle-dev] Fwd: isabelle test failed
makarius at sketis.net
Fri Jun 26 20:01:59 CEST 2015
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
date: Thu Jun 25 22:56:33 2015 +0200
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:
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.)
More information about the isabelle-dev