[isabelle-dev] NEWS and INCOMPATIBILITY
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
> 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:
date: Mon Oct 06 19:55:49 2014 +0200
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:
date: Sun Oct 05 13:16:24 2014 +0200
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