[isabelle] A large mutually recursive data type



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.