On Thu, 25 Sep 2014, Makarius wrote:
HOL-Proofs is important in various ways: theoretically it opens the
possibility for independent checking of proofs by a different system,
and thus raising the level of confidence in Isabelle results;
practically it indicates how close we are to the next
It doesn't seem like subst_tac had anything to do with it. I still have no
idea about what made HOL-Proofs slower on at-poly-e beween September 13
and 14. The log reveals nothing special, except a truncation at the end.
(while processing Predicate.thy). My personal inclination would be to
On 17.09.2014 11:40, Jasmin Christian Blanchette wrote:
There are only a handful of old_datatypes left in the AFP, and they will go
away as soon as Dmitriy gets a chance to fix a bug in his code (presumably once he's back
from vacation).
It is now (isabelle/7b92932ffea5) fixed, and the
Hi again,
Am 17.09.2014 um 11:40 schrieb Jasmin Christian Blanchette
jasmin.blanche...@gmail.com:
1. HOL-Proofs times out since September 14 on at-poly-e. On September 13,
we had
Timing HOL-Proofs (2 threads, 3161.882s elapsed time, 2889.329s cpu time,
840.167s GC time, factor 0.91)
Hi all,
The good news is that the port to the new datatypes have been overall a
success. There are only a handful of old_datatypes left in the AFP, and they
will go away as soon as Dmitriy gets a chance to fix a bug in his code
(presumably once he's back from vacation). Also good news: Timing
