[isabelle-dev] Fwd: isabelle test failed

[Makarius]

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