Re: [isabelle] Proof by analogy and proof stability in Isabelle



On Fri, Apr 30, 2010 at 6:21 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> I would be surprised if proof stability was the leading issue with users. I certainly do not recall losing much time in the course of a proof development to patching up failing proofs, even though (unlike most ordinary users surely) I invariably use potentially unstable development snapshots.

I would suggest that using incremental development snapshots actually
makes patching up your proofs *easier*.

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.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.