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

Dmitriy Traytel traytel at in.tum.de
Thu Apr 9 15:55:37 CEST 2015

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.)


PS: Your datatype reminded me of another one, which allows (or allowed) 
proving False in a different theorem prover ;-)

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