Hi Andreas,
I've investigated this a bit and the slowdown happens in the code plugin
in the instantiation of the equal type class (i.e. datatype (plugins
del: code) is more precise than the advice below). The number of
theorems proved there is quadratic (>8000 in your case).
But it is still not hopeless: those 8000 theorems are proved one after
each other calling Goal.prove for each of them. It is much faster to
form the (balanced) conjunction, call Goal.prove (which does among other
things type checking) once, and then destroy the conjunction. I'm
currently testing this on testboard
(http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010).
Cheers,
Dmitriy
On 09.04.2015 16:11, Andreas Lochbihler wrote:
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
