Re: [isabelle] Proof by analogy and proof stability in Isabelle
On Fri, 30 Apr 2010, Brian Huffman wrote:
On occasion I have had significant amounts of trouble getting old proof
scripts to work again. The process is most difficult with theories that
were developed for older versions of Isabelle: Porting a proof directly
from Isabelle 2005 to 2009 can be much more difficult than continuously
adapting the same proof to a series of development snapshots. I would
suspect that most users have to deal with these large version-jumps more
often than the developers do.
Jumping over several Isabelle releases at the same time is indeed very
hard. Users can avoid that by following the official release schedule --
the distances between Isabelle2007 -- Isabelle2008 -- Isabelle2009 --
Isabelle2009-1 are not too big.
Isabelle2005 -- Isabelle2007 is in fact a counter example, with 25 months
between the releases and the result being rather unstable. At that time
it was not completely clear if we would ever recover from a continously
"intermediate" state, and join the fate of notorious projects such as
SML/NJ or the STIX fonts.
Anyway, one should distinguish between really large libraries and the
underlying system infrastructure. A library could well be developed in a
Wikipedia style, and people in Nijmegen are working on that, for example.
This archive was generated by a fusion of
Pipermail (Mailman edition) and