Email Gateway (Sep 27 2021 at 16:23): Email Gateway (Sep 27 2021 at 16:23):From: Makarius <makarius@sketis.net>
We are slowly moving towards the next Isabelle release, a second one this
year: this special situation happens every few years, because the distance
between releases is constant at 8-10 months. (I always try to shorten the
interval a bit, but rarely manage.)
The overall plan is like this:
* Sun 03-Oct-2021: rough RC0 as "preview"
* 01-Nov-2021: official RC1
* total of 4-6 RCs for consolidation
* final immutable release before 15-Dec-2021
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
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 27 2021 at 16:54):From: Martin Desharnais <martin.desharnais@posteo.de>
Dean Isabelle devs,
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.
There is an asymmetry between the first and second release in a given
year (e.g. Isabelle2021 vs Isabelle2021-1).
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
OpenPGP_0x58AE985FE188789A.asc
OpenPGP_signature
Email Gateway (Sep 27 2021 at 17:32):From: Makarius <makarius@sketis.net>
On 27/09/2021 18:54, Martin Desharnais wrote:
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?
This is always a very unusual situation, one of big crisis of the state. There
would be at least two possibilities to address it:
* Use the older tag scheme to make an amendment, e.g. Isabelle2021-Dec is
superseded by Isabelle2021-Dec-1.
* Delay the amendment long enough to allocate new month name, e.g.
Isabelle2021-Dec is superseded by Isabelle2022-Jan.
An> lengthy solution would be to use ISO 8601 dates (e.g.
Isabelle2021-12-01) but
is aesthetically disputable.
We already have that for non-releases, using a different date standard, e.g.
see current Isabelle_27-Sep-2021 from
https://isabelle.sketis.net/devel/release_snapshot
Playing with the endless possibilities of date formats, one could also imagine
Isabelle_Dec-2021 (and thus Isabelle_Dec-2021-1 for an amendment that is never
meant to happen under normal circumstances).
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 27 2021 at 17:37):From: Lawrence Paulson <lp15@cam.ac.uk>
Apple would add a suffix like S or SE. Or maybe Isabelle 2021 Pro? :grinning:
Larry Paulson
Email Gateway (Sep 27 2021 at 17:51):From: Makarius <makarius@sketis.net>
Now that scheme is really from the 1990s.
Did you know that an early candidate for the Isar proof language was actually
"IsaPro"? It would have meant "Intelligible semi-automated Proving".
As the inventor of the original Isabelle release naming scheme, do you have
any inclinations to change anything, or keep the status-quo? For example:
Isabelle2021-1 (December 2021)
Isabelle2021-Dec
Isabelle2021-December
Isabelle_Dec-2021
Isabelle_December-2021
The last two would also amend an old misunderstanding of mine: You always had
something like Isabelle93.tar.gz but the name was intended to be "Isabelle 93"
with the space, right?. I've got that wrong, and discovered only 10 years later.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 27 2021 at 23:31):From: Gerwin Klein <kleing@unsw.edu.au>
I'm actually pretty happy with the current scheme (eg. 2021-1).
If there is a serious issue within the same month, we can increase the number, and in practice it happens extremely rarely, so there is not much room for confusion. As long as the year remains accurate, the scheme is pretty straightforward.
I'd also be fine with Isabelle2021-Dec, although that is harder to order automatically. The current scheme is somewhat order compatible with the old (and confusing) Isabelle-94-6 scheme. None of these are very strong arguments.
Cheers,
Gerwin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 28 2021 at 10:20):From: Lawrence Paulson <lp15@cam.ac.uk>
Any name needs to be reasonably compact: in papers, authors regularly refer to the precise version of Isabelle used. I wouldn't recommend any of the longer names suggested. Something like Isabelle2021A would work.
Larry
Email Gateway (Sep 29 2021 at 09:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
Any name needs to be reasonably compact: in papers, authors regularly
refer to the precise version of Isabelle used.
that observation is important.
In my view the current schema has the following weaknesses:
None of these is pressing enough to change the current schema, but if we
change the schema, they should be addressed.
Personally I'd go with sth. like
Isabelle-2021-Dec
Since the name is supposed to appear in print, a dash seems more
suitable than an underscore. This is in accordance with programming
environments appearing in big major version series often referred to as
jdk-8, jdk-11, jdk-17 etc.
Although Isabelle-2021-Dec is more verbose than e. g. Isabelle-2021a, I
guess the exact release name is typically quoted at most twice in a
typical paper.
I have some sympathy for Isabelle-2021a but it has the disadvantage that
it is not symmetric: both Isabelle-2021 and Isabelle-2021a refer to
proper »full« releases and Isabelle-2021a is not a »minor« or »patch«
release of Isabelle-2021.
Cheers,
Florian
OpenPGP_signature
Email Gateway (Sep 29 2021 at 10:09):From: Martin Desharnais <martin.desharnais@posteo.de>
Hi all,
Note that this suggestion, while very readable, cannot be correctly
sorted by the lexicographical order used by many tools (e.g. ls, sort).
I am not certain what the perceived problem with two numeric identifiers
is. Something like Isabelle-2021-02 and Isabelle-2021-12 looks readable
to me. This is well known from the Ubuntu naming scheme (e.g. Ubuntu
21.04, Ubuntu 21.10).
Regards,
Martin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 29 2021 at 20:26):From: Christian Sternagel <c.sternagel@gmail.com>
On Wed, Sep 29, 2021, 12:09 Martin Desharnais <martin.desharnais@posteo.de>
wrote:
Hi all,
In my view the current schema has the following weaknesses: * No separator between »Isabelle« and year (an imitation of CaMlCaSe). * Two numeric identifiers side by side.
None of these is pressing enough to change the current schema, but if we
change the schema, they should be addressed.Personally I'd go with sth. like
Isabelle-2021-Dec
Note that this suggestion, while very readable, cannot be correctly
sorted by the lexicographical order used by many tools (e.g. ls, sort).I am not certain what the perceived problem with two numeric identifiers
is. Something like Isabelle-2021-02 and Isabelle-2021-12 looks readable
to me. This is well known from the Ubuntu naming scheme (e.g. Ubuntu
21.04, Ubuntu 21.10).
Apropos Ubuntu naming scheme: Most version numbers I am aware of use dots
as separator. Moreover, there is a difference between the version number
and the name of the thing. How about
Isabelle 2021
Isabelle 2021.01
Isabelle 2021.02
...
(where the version is only the part after the space and maybe the first one
should be "Isabelle 2021.00")?
Just my 2 cents.
cheers
Chris
Regards,
Martin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 29 2021 at 21:02):From: Makarius <makarius@sketis.net>
Traditionally the year belongs to the name, because the saying is "we release
a new system each time that is loosely based on the old one". So strictly
speaking, there is no version number.
But in recent years, I rarely used that narrative anymore, for two reasons:
(1) Isabelle has become so huge and consolidated, that the changes for each
newly released system are relatively small.
(2) The Lean Prover guys have somewhat abused this attitude, and released
quite incompatible new systems each time: 2 ~> 3, now 3 ~> 4 (it still remains
to be seen how Mathlib manages to jump over that gulf).
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 14 2021 at 15:27):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
late to the party, and just an unsolicited comment from the sidelines,
but I would strongly suggest to heed this warning:
Less strongly I’d like to point out that using calendar-based YY.MM or
YYYY.MM release names have become quite common (Ubuntu and Nixpkg come
to mind; I am sure I saw it elsewhere too). In addition to the common
convention of using dashes to separate name and version, and dots in
the version number, and the fact that Isabelle so far uses four-digit
years, this would point towards
Isabelle-2021.02
Isabelle-2021.12
Isabelle-2022.05
Cheers,
Joachim
PS: I must admit I always have to think twice to put September and
August into the right order, and don’t have that problem with 08 and 09
Last updated: Apr 20 2024 at 01:05 UTC