[isabelle-dev] Fwd: isabelle test failed

[Makarius]

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