Hi Dmitriy,
Thanks for investigating. I am really surprised that the code plugin is to blame for the
huge overhead. I don't know the details of the code plugin, but I have an idea of what it
should do: instantiate the equals type class, register the constructors as code
constructors, and declare the pattern-matching equations for case, set, rel, map and
equals as [code].
None of this should involve any fancy proof. In fact, most of the equations should have
already been proven by the free_constructors part or should be easily derived from them by
single-step resolutions. What am I missing?
Andreas
On 13/04/15 12:04, Dmitriy Traytel wrote:
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
