Re: [isabelle] A large mutually recursive data type



Hi Dmitriy,

Thanks for the answer. I have also tried Isabelle2013-2 (which I believe uses the old Isabelleâs package) with no success, although I didnât wait much longer.

Please find attached the isabelle theory with the concrete datatype.
Cheers,

Victor

Attachment: Cabs.thy
Description: Binary data




> On 11 Mar 2016, at 11:07, Dmitriy Traytel <traytel at inf.ethz.ch> wrote:
> 
> Hi Victor,
> 
> Isabelleâs new package for datatypes works quite differently from HOL4âs package (and from Isabelleâs old package which was much closer to HOL4âs).
> 
> The new package is known to be slower for mutual types, than the old construction. It is much faster for nested recursion (in ââa tree = Node âa "âa tree listâ âa tree is nested in âa list) though, such that in most applications we saw so far the new package was actually faster. I donât think we ever tried it with more than 15 mutually recursive types.
> 
> Iâm quite curious to see you concrete datatype to say if it still might be feasible. (I donât see any attachment in your mail.)
> 
> Cheers,
> Dmitriy
> 
> 
>> On 10 Mar 2016, at 18:35, Victor Gomes <vb358 at cam.ac.uk> wrote:
>> 
>> Dear Isabelle experts,
>> 
>> As part of the Cerberus project, a formalisation of the de-facto C semantics, I was trying to import the model into Isabelle/HOL.
>> 
>> One of the first files (attached a simplified version) contains a very large mutually recursive data type (with 30 different types, around 5 or 10 constructors each).
>> After a few minutes waiting a response from Isabelle, I realised there was no hope to try to wait in JEdit.
>> Therefore, I decided to build an Isabelle heap file.
>> 
>> Isabelle took around 40 min to give me the following error:
>> ISABELLE_BUILD_OPTIONS=""
>> 
>> ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"
>> 
>> ML_PLATFORM="x86-darwin"
>> ML_HOME="/Applications/Isabelle2016.app/Contents/Resources/Isabelle2016/contrib/polyml-5.6-1/x86-darwin"
>> ML_SYSTEM="polyml-5.6"
>> ML_OPTIONS="-H 500"
>> 
>> Session Pure/Pure
>> Session HOL/HOL (main)
>> Session Unsorted/isabelle_generated
>> Building isabelle_generated ...
>> isabelle_generated: theory Cabs
>> Run out of store - interrupting threads
>> Run out of store - interrupting threads
>> Failed to recover - exiting
>> isabelle_generated FAILED
>> 
>> 
>> Since the default ML_OPTIONS is â-H 500â, I increased it to â-H 4000â and gave Isabelle another try.
>> This time I waited for 4 hoursâ at that point I gave up.
>> 
>> Iâve decided to give HOL4 a try and the same datatype was handled by HOL4 in minutes (around 2 min, I think).
>> I know Isabelle is quite heavy (for good reasons) compared to HOL4, but the difference is astonishing.
>> I was wondering if there is any optimisation issue in the Isabelle datatype package.
>> 
>> Isabelle probably produces a lot more lemmas "for free" when defining a datatype, but a slowdown in processing seems to be the price you pay. 
>> 
>> The main question is: 
>> Is there any hope of definitions like this being practicable within Isabelle/HOL in the future?
>> 
>> Note that:
>> - My machine is a MacBook Pro 2015 16GB
>> - Iâve used Isabelle 2016
>> - The version of polyml used in both cases (Isabelle and HOL4) are the same, polyml-5.6.
>> 
>> Best wishes,
>> Victor
>> 
> 



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.