[isabelle-dev] Isabelle release

Alexander Krauss krauss at in.tum.de
Fri Jan 7 10:05:18 CET 2011

Hi all,

(must add my 2ct, too)	

Concerning the content of the next release:

Brian wrote:
> What exactly makes it "major"? Judging by the NEWS file, it looks
> like 2009-2 introduced about as many new features as the upcoming
> release will. Is there any new feature in particular that is
> considered a "major" change?

There are certainly many interesting things: Coercions, partial_function
(though that is still lacking induction rules so it's a bit unfinished),
smt in sledgehammer, big HOLCF cleanup etc. But I find it impossible to
assign a 'major' predicate consistently. And what is major
for one user is irrelevant for the other.

I have the same feeling as Gerwin concerning release naming. When
Isabelle 2009-2 came out, several users asked me about the name and I
found it hard to give them a consistent answer.

Also, in this particular situation, having an Isabelle 2010 release in
January looks a bit like "they didn't make their planned release date" :-)

Larry wrote:
> I'm afraid that I originated the custom of not always linking the
> release name to the calendar year. The idea was to indicate that the
> new release consisted of little more than patches from the previous
> one.

Larry, would you say that this is still adequate given how Isabelle 
evolves today? Are we talking 'just patches' here, given the changes 
mentioned above (plus countless small improvements everywhere as usual)? 
Or what is it? To me it is just the next small step in a sequence, and 
after 10 years we look back and are surprised about the 'major' changes 
that happened.

Michael wrote:
> Or dispense with year numbers entirely.
> Even Microsoft gave up on that idea for Windows.

But then we need a Marketing division to come up with a new name every 8 
months :-}. Year numbers are very comfortable.

More information about the isabelle-dev mailing list