[isabelle-dev] datatype takes minutes, but timing panel shows 10s

[Dmitriy Traytel]

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-dev at in.tum.de
>>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>>>>
>>>>
>>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150414/1ffd439a/attachment-0002.html>