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

[Martin Desharnais]

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 --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0x58AE985FE188789A.asc
Type: application/pgp-keys
Size: 3131 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210927/c9070c9c/attachment-0001.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 840 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210927/c9070c9c/attachment-0001.sig>