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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
