<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<title></title>
</head>
<body>
<div name="messageBodySection">
<div dir="auto">Apple would add a suffix like S or SE. Or maybe Isabelle 2021 Pro? ðŸ˜€</div>
</div>
<div name="messageSignatureSection"><br>
<div dir="auto">Larry Paulson</div>
</div>
<div name="messageReplySection">On 27 Sep 2021, 17:54 +0100, Martin Desharnais <martin.desharnais@posteo.de>, wrote:<br>
<blockquote type="cite" style="border-left-color: grey; border-left-width: thin; border-left-style: solid; margin: 5px 5px;padding-left: 10px;">
Dean Isabelle devs,<br>
<br>
<blockquote type="cite">The remaining question right now is if we want to venture at a change of the<br>
release naming scheme. According to the existing scheme, it would be<br>
"Isabelle2021-1 (December 2021)". Afterwards there would be "Isabelle2022<br>
(October 2022)".<br>
<br>
Some decades ago, Larry treated the year like a major version number, with<br>
occasional bumps added via -1, -2, -3. E.g. see the long and successful series<br>
of Isabelle94-n, even with a few releases lost in time and space:<br>
https://isabelle.in.tum.de/download_past.html<br>
<br>
After 2011, this scheme no longer made any sense: So many great things were<br>
already present in the Isabelle corpus, that made it hard to justify a major<br>
release number increase again. So instead of being stuck with 2011<br>
indefinitely (which was after addition of PIDE), and merely have variations<br>
2011-1, 2011-2, 2011-3, 2011-4, ..., we followed a modified scheme where the<br>
year is always that of the calender and tags -1, -2 distinguish multiple<br>
releases per year.<br>
<br>
[3 releases actually did happen in 2013, because Isabelle2013-1 (November<br>
2013) had serious problems in PIDE that had to be addressed in Isabelle2013-2<br>
(December 2013). Like in the Roman Empire or the Habsburg Empire, a "3 Emporer<br>
year" is actually something very bad, and to be avoided at all cost.]<br>
<br>
<br>
In summary we could venture at a slight reform as follows:<br>
<br>
* Releases are always named after the calender year + month of final<br>
appearance, lets say "Isabelle2021-Dec" for the coming release: Following the<br>
naming scheme for months "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul",<br>
"Aug", "Sep", "Oct", "Nov", "Dec" that is used in other places of Isabelle<br>
already. An alternative is to spell out the month, e.g. Isabelle2021-December.<br>
<br>
* This year + month scheme would continue uniformly in the future,<br>
independently of the number of releases per year. So after "Isabelle2021-Dec"<br>
would come something like "Isabelle2022-Oct".<br>
<br>
* The explanatory add-on like "(December 2021)" disappears, being now<br>
redundant. IIRC correctly, I had proposed this to Larry on the occasion of<br>
"Isabelle94-7 (November 1996)" to make it look a bit less confusing to our<br>
growing user community.<br>
<br>
<br>
How is the feeling for this idea after so much text, which only scratches many<br>
delicate points of our long history?<br>
<br>
What name should it be?<br>
<br>
Isabelle2021-1 (December 2021)<br>
Isabelle2021-Dec<br>
Isabelle2021-December<br>
</blockquote>
<br>
I am not entirely sure what the problem with the current naming scheme<br>
are. I think it would help to explicitly state the actual deficits that<br>
should/could be addressed. Based on that, it would be easier to evaluate<br>
and compare suggestions for new schemes.<br>
<br>
Here is what I can think of.<br>
<br>
1. There is an asymmetry between the first and second release in a given<br>
year (e.g. Isabelle2021 vs Isabelle2021-1).<br>
2. To an uninitiated user, it may not be entirely clear which one of is<br>
the most recent (e.g. Isabelle2021-1 may be wrongly interpreted as some<br>
kind of prerelease).<br>
<br>
Out of Makarius's suggestions, I personally like the fact that the three<br>
letter months always lead to versions having the same number of<br>
characters, which also imply that they have same physical length in<br>
monospace fonts. Using month numbers would also share this<br>
characteristic (e.g. Isabelle2021-12 or Isabelle2021.12).<br>
<br>
However, one advantage of the current scheme is its fine granularity.<br>
Three emperors in a year are certainly to be avoided at all cost, but it<br>
cannot be excluded entirely. The naming scheme should have a solution in<br>
such situation. What would happen if a critical bug was discovered in<br>
Isabelle2021-Dec? An lengthy solution would be to use ISO 8601 dates<br>
(e.g. Isabelle2021-12-01) but is aesthetically disputable.<br>
<br>
Regards,<br>
Martin<br>
<br>
</blockquote>
</div>
</body>
</html>