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 MHonArc.