Re: [isabelle] provers used by sledgehammer

On Fri, 20 Jul 2012, Tobias Nipkow wrote:

Am 20/07/2012 16:43, schrieb Makarius:
On Fri, 20 Jul 2012, Tobias Nipkow wrote:

It is customary to continue maintaining a tool until the replacement is ready
for prime time. Currently jedit is not at the point (and PG still works). I
expect that PG will be kept in a working state until key jedit problems like
"Workaround: Cut/paste larger parts or reload buffer" and the absence of menus
(which force people to remember and type commands) have been eliminated.

So who is continuing the maintenance of Proof General?  It won't continue to
work magically without doing anything.

By default the person who introduced the tool in the first place or the one who is responsible for the change that stops it functioning. That is you, I should think.

Odd. I am not responsible for Apple changing Mac OS every 1-2 years, Linux distributors changing Emacs versions, Emacs changing, PG itself changing upstream etc. The few Isabelle changes that have ever affected some PG version in the past are negligible compared to that, and are usually quick and easy to repair if people report them quickly and constructively.

It seems I have done maintainence too efficiently in the past, so that it was almost invisible, and one could think systems just work on their own and continue indefinitely.

Change is sometimes annyoing, but part of the normal software life-cycle. An alternative to that is embalming of old versions in stasis: just last year I've taken a stock Isabelle2005 release and made it work again with XEmacs 21.x in the classic manner, with 100% of its nastalgic look and feel, even real "X-Symbol" and the bitmap fonts of that time. But that just showed again that there is subjective bit rot as well: what was fine 10 years ago is hardly bearable today. Even the most conservative PG user would not want to continue 10 years with the same old version.


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