[isabelle-dev] NEWS and INCOMPATIBILITY

Makarius makarius at sketis.net
Mon Oct 6 20:08:25 CEST 2014

On Thu, 2 Oct 2014, Florian Haftmann wrote:

> We have a tradition not to change NEWS after release, but maybe we
> should break this rule and consolidate the following accidents (3 times
> only):
> to
> This might seem ridiculous in the first instance, but when using
> andeditor with a context-sensitive completion facility there is some
> chance that these accidents get perpetuated.

I have changed that now:

changeset:   58604:13dfea1621b2
tag:         tip
user:        wenzelm
date:        Mon Oct 06 19:55:49 2014 +0200
files:       NEWS
improved spelling of formal INCOMPATIBILITY in historic versions (!) -- to 
avoid ad-hoc word completion multiply such lapses;

In recent releases we've had occasional diversions from the old rule of 
strict monotonicity in NEWS, but I always try to keep the execptions at a 

There are many running gags and bad jokes about the NEWS file, but I don't 
remember everything about its long history.  For each release, I try to 
get the new chapter into shape, and avoid damage to the cumulative ones 
from the history.  In former times, we've had occasional accidents, where 
changes that were meant for the current release where applied to older 
ones, e.g. when moving them around -- I still check such things routinely 
as part of the release procedure.

As a high-level principle, Isabelle releases are a linear progress of 
immutable versions -- there are no attempts to "amend" already published 
releases.  The traditional NEWS process imitates that at a small scale.

BTW, the Isabelle/jEdit NEWS "IDE" has made again a little step forwards:

changeset:   58542:19e062fbfea0
user:        wenzelm
date:        Sun Oct 05 13:16:24 2014 +0200
files:       src/Tools/jEdit/src/Isabelle.props 
more advanced NEWS tree structure and folding;

A remaining question is if/how spell-checking could be included as well. 
I've tried that manually for Isabelle2014, but the mixture of prose text 
with quasi-formal bits makes it hard to see anything -- too much blue 
underlining in irrelevant places.


More information about the isabelle-dev mailing list