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.
Cheers,
Andreas
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-...@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
