[isabelle-dev] Towards the next release --- and release naming scheme

[Lawrence Paulson]

Apple would add a suffix like S or SE. Or maybe Isabelle 2021 Pro? 😀

Larry Paulson
On 27 Sep 2021, 17:54 +0100, Martin Desharnais <martin.desharnais at posteo.de>, wrote:
Dean Isabelle devs,

The remaining question right now is if we want to venture at a change of the
release naming scheme. According to the existing scheme, it would be
"Isabelle2021-1 (December 2021)". Afterwards there would be "Isabelle2022
(October 2022)".

Some decades ago, Larry treated the year like a major version number, with
occasional bumps added via -1, -2, -3. E.g. see the long and successful series
of Isabelle94-n, even with a few releases lost in time and space:
https://isabelle.in.tum.de/download_past.html

After 2011, this scheme no longer made any sense: So many great things were
already present in the Isabelle corpus, that made it hard to justify a major
release number increase again. So instead of being stuck with 2011
indefinitely (which was after addition of PIDE), and merely have variations
2011-1, 2011-2, 2011-3, 2011-4, ..., we followed a modified scheme where the
year is always that of the calender and tags -1, -2 distinguish multiple
releases per year.

[3 releases actually did happen in 2013, because Isabelle2013-1 (November
2013) had serious problems in PIDE that had to be addressed in Isabelle2013-2
(December 2013). Like in the Roman Empire or the Habsburg Empire, a "3 Emporer
year" is actually something very bad, and to be avoided at all cost.]


In summary we could venture at a slight reform as follows:

* Releases are always named after the calender year + month of final
appearance, lets say "Isabelle2021-Dec" for the coming release: Following the
naming scheme for months "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul",
"Aug", "Sep", "Oct", "Nov", "Dec" that is used in other places of Isabelle
already. An alternative is to spell out the month, e.g. Isabelle2021-December.

* This year + month scheme would continue uniformly in the future,
independently of the number of releases per year. So after "Isabelle2021-Dec"
would come something like "Isabelle2022-Oct".

* The explanatory add-on like "(December 2021)" disappears, being now
redundant. IIRC correctly, I had proposed this to Larry on the occasion of
"Isabelle94-7 (November 1996)" to make it look a bit less confusing to our
growing user community.


How is the feeling for this idea after so much text, which only scratches many
delicate points of our long history?

What name should it be?

Isabelle2021-1 (December 2021)
Isabelle2021-Dec
Isabelle2021-December

I am not entirely sure what the problem with the current naming scheme
are. I think it would help to explicitly state the actual deficits that
should/could be addressed. Based on that, it would be easier to evaluate
and compare suggestions for new schemes.

Here is what I can think of.

1. There is an asymmetry between the first and second release in a given
year (e.g. Isabelle2021 vs Isabelle2021-1).
2. To an uninitiated user, it may not be entirely clear which one of is
the most recent (e.g. Isabelle2021-1 may be wrongly interpreted as some
kind of prerelease).

Out of Makarius's suggestions, I personally like the fact that the three
letter months always lead to versions having the same number of
characters, which also imply that they have same physical length in
monospace fonts. Using month numbers would also share this
characteristic (e.g. Isabelle2021-12 or Isabelle2021.12).

However, one advantage of the current scheme is its fine granularity.
Three emperors in a year are certainly to be avoided at all cost, but it
cannot be excluded entirely. The naming scheme should have a solution in
such situation. What would happen if a critical bug was discovered in
Isabelle2021-Dec? An lengthy solution would be to use ISO 8601 dates
(e.g. Isabelle2021-12-01) but is aesthetically disputable.

Regards,
Martin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210927/be449d02/attachment.htm>