Email Gateway (Aug 18 2022 at 17:34): Email Gateway (Aug 18 2022 at 17:34):From: li yongjian <lyj238@gmail.com>
Dear all:
Here I want to ask some two questions on some tools on Isabelle.
Is there any proof script tranforming tool from old version to new
version.
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.
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?
best
Email Gateway (Aug 18 2022 at 17:34):From: Lars Noschinski <noschinl@in.tum.de>
On 14.04.2011 10:52, li yongjian wrote:
- Is there any proof script tranforming tool from old version to new
version.
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.
To my knowledge, there is no such tool, you need to update your theories
manually.
- 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?
The repository URL is a bit hidden under Download / repository snapshot
/ Mercurial repository:
http://isabelle.in.tum.de/repos/isabelle/
As there are often incompatible changes during development, I would
strongly suggest to use the latest release instead; unless you have a
pressing reason.
Regards, Lars
Email Gateway (Aug 18 2022 at 17:35):From: Makarius <makarius@sketis.net>
On Thu, 14 Apr 2011, li yongjian wrote:
- Is there any proof script tranforming tool from old version to new
version.
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.
- 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
http://isabelle.in.tum.de/repos/isabelle/
Makarius
Last updated: Apr 20 2024 at 01:05 UTC