Hi Andreas,
the code plugin defines a new constant (copy of op =) that is used as
equality.
datatype x = A | B
export_code equal_x_inst.equal_x in SML
To get it executable (#constructors)^2 equations are proved in a
backward fashion (I'm sure it could be easilly done in a forward fashion
as well). However, this code goes back to Stefan and Florian, and we
didn't attempt to optimize it when integrating it with the new package.
But isn't the performance now (894d6d863823 ) already acceptable?
Dmitriy
On 14.04.2015 08:10, Andreas Lochbihler wrote:
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
