Re: [isabelle] tools on Isabelle.
On Thu, 14 Apr 2011, li yongjian wrote:
1. Is there any proof script tranforming tool from old version to new
Isabelle has been updated very quickly. But it does not support the
old version of proof scripts. For instance, constdefs command is not
supported by the new version. I want to ask whether a tool is available
to transfer the old proof script into new one supported by the new
version of Isabelle.
There is a 6-10 months release cycle. Legacy features like 'constdefs'
usually take 1-3 releases from the first indication that they are
discontinued (by issuing certain warnings) to removal. This gives more
than 1-2 years to update existing theories. This typically becomes
unconfortable when NEWS about changes and legacy warnings are ignored for
a long time, and you are forced to convert in the last moment, when old
features are finally deleted.
2. Mercurial repository.
Isabelle's development uses Mercury as version control tool.
Now is it possible to download the most recent version of some materials?
Is it readable for a user who is not a developper?
What command to use?
"Using" the repository version is quite adventurous. You need to make
yourself an expert of the build process, and the only guarantee is that
there will be really many changes in a short time. If you need your
thrill every morning instead of working productively, you can start with
README_REPOSITORY and Admin/makedist from
This archive was generated by a fusion of
Pipermail (Mailman edition) and