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

[Andreas Lochbihler]

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
>>>
>