Re: [isabelle] A large mutually recursive data type



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.