[isabelle-dev] Fwd: isabelle test failed

[Dmitriy Traytel]

Oops, I didn't expect my name to appear here ;-)

The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report 
[1]. With turned off proofs the effect was a good one.

What is special about Pure.conjunction w.r.t. proof reconstruction? Is 
it something in Goal.conjunction_tac? Would you advise to use HOL's 
conjunction instead?

Dmitriy

[1] 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-April/005986.html

On 26.06.2015 20:01, 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.)
>
>
>     Makarius
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>