Email Gateway (Aug 18 2022 at 19:08): Email Gateway (Aug 18 2022 at 19:08):From: Makarius <makarius@sketis.net>
On Wed, 15 Feb 2012, Jeremy Dawson wrote:
Makarius is right in guessing that I'm referring to Isabelle2005 - it
was when I started to convert all my proofs from Isabelle 2005 to 2007 I
seemed to be spending a lot of time on it when I would rather be doing
useful work.
The huge gap between Isabelle2005 and Isabelle2007 is in fact exceptional.
There were 25 months between the two releases, and actually Isabelle2006
missing. In 2007 it was still unclear if we would recover again to a sane
state.
The transition Isabelle2005 -> Isabelle2007/2008 also marks the point
where really ancient customs from the late 1990-ies were finally given up,
with a delay of 5-10 years.
Taking both together, there has been definitely a loss of Isabelle
applications from the past, those that did not manage the jump into the
current century.
From Isabelle2007 on we have followed a more disciplined release schedule,
with a limited amount of pain caused by incompatibilities, as before
Isabelle2005. So applications that follow the stepping stones of each
official release now should be quite at easy to port.
Here it greatly helps to sort out old/legacy things before making a
step forwards, and not to make too many steps at the same time.
I gather things have got worse since then, in terms of incompatibilities
between versions of Isabelle and therefore the prospects of users making
use of other users' work
Yes, by sticking to very old versions of Isabelle, other people will
hardly be able to re-use such work. I reckon that the interval of
relevant Isabelle releases consists of the 2-3 last ones. It is also
important to refrain from offering things "for the latest snapshot, which
is the one on my laptop". The probability that two people have the same
"latest versions" and can thus share some work is approximately 0.
Here is an arbitrary example for a project that relates a range of
versions of both itself and Isabelle in a nice way:
http://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html
Another way is to wrap things up as an article for AFP, following the
guidelines by its editors. Porting is than mostly auto-magically.
Makarius
Last updated: Apr 19 2024 at 08:19 UTC