[isabelle-dev] datatype takes minutes, but timing panel shows 10s

Andreas Lochbihler andreas.lochbihler at inf.ethz.ch
Thu Apr 9 16:11:32 CEST 2015

Hi Dmitriy and Jasmin,

Thanks for the hint with plugins. That really speeds things up. I also suspect that the 
timing panel does not include the forked proof tactics.


On 09/04/15 15:55, Dmitriy Traytel wrote:
> Hi Andreas,
> rather than going dirty, try:
> datatype (plugins only:) family ...
> It seems that here we are "lucky" and the slowdown is caused by one of the plugins. (We'll
> investigate which one.)
> Cheers,
> Dmitriy
> PS: Your datatype reminded me of another one, which allows (or allowed) proving False in a
> different theorem prover ;-)
> https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html
> On 09.04.2015 15:44, Jasmin Blanchette wrote:
>> Hi Andreas,
>>> In Isabelle2014, processing this datatype declaration takes about one minute. So what
>>> has happened in between? (The Isabelle2014 timing panel is also way off with 8 seconds.)
>> Thanks for your report. What happened in between is that we generate more theorems. I
>> suspect one or a few of them have tactics that scale poorly (e.g. cubic) in the number
>> of constructors.
>> As for the timing panel, I suspect it does not take into consideration the time spent in
>> tactics with multithreading on, but I’m not an expert there.
>> We’ll look into this. You could try “quick_and_dirty” around that particular datatype to
>> make things more tolerable in the meantime.
>> Cheers,
>> Jasmin
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list