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

[Dmitriy Traytel]

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