[isabelle-dev] Fwd: isabelle test failed
makarius at sketis.net
Thu Jul 2 23:33:07 CEST 2015
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
> changeset: 60574:915da29bf5d9
> user: wenzelm
> date: Thu Jun 25 22:56:33 2015 +0200
> files: Admin/isatest/settings/at64-poly
> 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).
More information about the isabelle-dev