Victor Gomes
2016-03-11 10:26:25 UTC
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
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