<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Hi Andreas,<br>
<br>
the code plugin defines a new constant (copy of op =) that is used
as equality.<br>
<br>
datatype x = A | B<br>
export_code equal_x_inst.equal_x in SML<br>
<br>
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.<br>
<br>
But isn't the performance now (894d6d863823
<meta name="qrichtext" content="1">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css">
p, li { white-space: pre-wrap; }
</style>) already acceptable?<br>
<br>
Dmitriy<br>
<br>
On 14.04.2015 08:10, Andreas Lochbihler wrote:<br>
</div>
<blockquote cite="mid:552CAF65.9090301@inf.ethz.ch" type="cite">Hi
Dmitriy,
<br>
<br>
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].
<br>
<br>
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?
<br>
<br>
Andreas
<br>
<br>
On 13/04/15 12:04, Dmitriy Traytel wrote:
<br>
<blockquote type="cite">Hi Andreas,
<br>
<br>
I've investigated this a bit and the slowdown happens in the
code plugin in the
<br>
instantiation of the equal type class (i.e. datatype (plugins
del: code) is more precise
<br>
than the advice below). The number of theorems proved there is
quadratic (>8000 in your
<br>
case).
<br>
<br>
But it is still not hopeless: those 8000 theorems are proved one
after each other calling
<br>
Goal.prove for each of them. It is much faster to form the
(balanced) conjunction, call
<br>
Goal.prove (which does among other things type checking) once,
and then destroy the
<br>
conjunction. I'm currently testing this on testboard
<br>
(<a class="moz-txt-link-freetext" href="http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010">http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010</a>).
<br>
<br>
Cheers,
<br>
Dmitriy
<br>
<br>
On 09.04.2015 16:11, Andreas Lochbihler wrote:
<br>
<blockquote type="cite">Hi Dmitriy and Jasmin,
<br>
<br>
Thanks for the hint with plugins. That really speeds things
up. I also suspect that the
<br>
timing panel does not include the forked proof tactics.
<br>
<br>
Cheers,
<br>
Andreas
<br>
<br>
On 09/04/15 15:55, Dmitriy Traytel wrote:
<br>
<blockquote type="cite">Hi Andreas,
<br>
<br>
rather than going dirty, try:
<br>
<br>
datatype (plugins only:) family ...
<br>
<br>
It seems that here we are "lucky" and the slowdown is caused
by one of the plugins. (We'll
<br>
investigate which one.)
<br>
<br>
Cheers,
<br>
Dmitriy
<br>
<br>
PS: Your datatype reminded me of another one, which allows
(or allowed) proving False in a
<br>
different theorem prover ;-)
<br>
<a class="moz-txt-link-freetext" href="https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html">https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html</a>
<br>
<br>
On 09.04.2015 15:44, Jasmin Blanchette wrote:
<br>
<blockquote type="cite">Hi Andreas,
<br>
<br>
<blockquote type="cite">In Isabelle2014, processing this
datatype declaration takes about one minute. So what
<br>
has happened in between? (The Isabelle2014 timing panel
is also way off with 8 seconds.)
<br>
</blockquote>
Thanks for your report. What happened in between is that
we generate more theorems. I
<br>
suspect one or a few of them have tactics that scale
poorly (e.g. cubic) in the number
<br>
of constructors.
<br>
<br>
As for the timing panel, I suspect it does not take into
consideration the time spent in
<br>
tactics with multithreading on, but I’m not an expert
there.
<br>
<br>
We’ll look into this. You could try “quick_and_dirty”
around that particular datatype to
<br>
make things more tolerable in the meantime.
<br>
<br>
Cheers,
<br>
<br>
Jasmin
<br>
<br>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
<br>
</blockquote>
<br>
</blockquote>
</blockquote>
<br>
</blockquote>
</blockquote>
<br>
</body>
</html>