Email Gateway (Feb 25 2026 at 01:49): Email Gateway (Feb 25 2026 at 01:49):From: Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk>
I’m sorry if a form of this question has been discussed multiple times during Isabelle’s past decades of evolution, but nevertheless: wouldn’t it be nice if Isabelle releases followed a best-practice major/minor versioning discipline, so that we could normally rely on minor-version releases to make only backwards-compatible changes?
To be clear, I’m not proposing to change Isabelle’s whole version numbering system, in particular the tradition of using a year as more-or-less a “major” version number and suffixes like “-1” for incremental updates within a year. I see nothing wrong with that tradition. Rather, I’m just suggesting that it would be nice if we could rely on incompatible changes mostly being reserved for “major” year-number releases like Isabelle2026, and for “minor” releases like “Isabelle2025-1” to avoid such compatibility-breaking changes.
I’ll briefly relate an incident in which the Isabelle2025-1 release in particular “bit” me and a group of undergraduate students in the past couple months. In late December I was evaluating applications for undergraduate summer internships in my lab at EPFL, including quite a few candidates to work with Isabelle/HOL on our Grounded Arithmetic or GA project (https://bford.info/pub/lang/ga/). As part of the evaluation process I gave these candidates a “challenge problem” involving actually using Isabelle2025 for some nontrivial theorem-proving in a subset of the GA code base. But soon a few of these candidates started noticing strange behavior: proving stuff was “too easy” and the proofs that sledgehammer found always referred to a particular locale assumption. A couple candidates noticed that there was an outright inconsistency: Isabelle was allowing proofs of anything within the relevant locale. But I knew that the locale’s assumptions were consistent, as the code base also successfully instantiated that locale.
Upon debugging this behavior and suspecting Isabelle version issues, I finally saw that Isabelle2025-1 had been released only days before I assigned this challenge problem. Indeed, a look through the Isabelle2025-1 change log quickly revealed the problem (to me, not to the candidates, most of whom were completely new to Isabelle and mostly new to proof assistants in general):
" - Removed predicate single_valuedp. Use predicate right_unique instead. INCOMPATIBILITY.”
The locale assumption I mentioned above was of the form “single_valuedp R” for a concrete single-valued predicate-relation R, but to the candidates who had accidentally downloaded and used Isabelle2025-1 instead of Isabelle2025, the ‘single_valuedp’ was being interpreted as a function variable rather than a constant, and implicitly universally quantified, so the locale assumption was in effect that all predicates were true of R. Oops.
I’ll be the first to admit that this incident was partly my fault, for not watching the Isabelle mailing list closely at that time and noticing that an Isabelle2025-1 had just been released, and in turn failing to warn the challenge problem candidates not to use that brand-new version. But especially given that “Isabelle2025” had been stable and unchanged through almost all of the year 2025, I was not anticipating a new variant also called more-or-less “Isabelle2025" being released only in the last few weeks of 2025, let alone that release including major compatibility-breaking changes like the complete removal of long-stable standard constants from Main.
I also have no argument against this particular change; “right_unique” is a perfectly fine name too. But I’m just suggesting that it would be nice if compatibility-breaking changes like this could be scheduled for the next “major” Isabelle release that increases the year number, i.e., Isabelle2026. (I had carefully instructed the candidates to download and use “Isabelle2025” and no other version; I only didn’t know at the time that an “Isabelle2025-1” had just gone up.).
As a result of this breaking change slipped into Isabelle2025-1, quite a few sharp and eager potential new Isabelle users were not only extremely confused but lost in some cases days of effort to this versioning issue until I had the time to debug the problem for them.
As a related issue with the Isabelle home page, it is fairly non-obvious exactly how to find and download prior Isabelle releases — even recently-prior releases like Isabelle2025. It would be nice if pointers to the websites of at least a few prior versions (especially including the original “base version” for a given year) were readily accessible from the home page for those looking for exactly a particular version. Upon debugging the above issue, I had to resort to manual URL-editing to find and point the candidates to the “old” Isabelle2025 website so they could download the correct version.
Just a few versioning thoughts, FWIW.
Thanks
Bryan
Email Gateway (Feb 25 2026 at 09:40):From: Fabian Huch <huch@in.tum.de>
I think you are misunderstanding the versioning scheme -- Isabelle2025-1
is not a 'minor' release, it is simply the second release in the year
2025 (this happens regularly since the release cycle is a bit shorter
than one year). Releases are always immutable and will not be changed.
For the naming of the second release in one year, there hasn't been a
better proposal than adding a number postfix.
We did have a second special Isabelle2025-2 release over Isabelle2025-1,
where an important problem was solved. An argument can be made that such
special releases could be named differently.
Fabian
On 2/25/26 02:48, Bryan Alexander Ford (via cl-isabelle-users Mailing
List) wrote:
I’m sorry if a form of this question has been discussed multiple times
during Isabelle’s past decades of evolution, but nevertheless:
wouldn’t it be nice if Isabelle releases followed a best-practice
major/minor versioning discipline, so that we could normally rely on
minor-version releases to make only backwards-compatible changes?To be clear, I’m not proposing to change Isabelle’s whole version
numbering system, in particular the tradition of using a year as
more-or-less a “major” version number and suffixes like “-1” for
incremental updates within a year. I see nothing wrong with that
tradition. Rather, I’m just suggesting that it would be nice if we
could rely on incompatible changes mostly being reserved for “major”
year-number releases like Isabelle2026, and for “minor” releases like
“Isabelle2025-1” to avoid such compatibility-breaking changes.I’ll briefly relate an incident in which the Isabelle2025-1 release in
particular “bit” me and a group of undergraduate students in the past
couple months. In late December I was evaluating applications for
undergraduate summer internships in my lab at EPFL, including quite a
few candidates to work with Isabelle/HOL on our Grounded Arithmetic or
GA project (https://bford.info/pub/lang/ga/). As part of the
evaluation process I gave these candidates a “challenge problem”
involving actually using Isabelle2025 for some nontrivial
theorem-proving in a subset of the GA code base. But soon a few of
these candidates started noticing strange behavior: proving stuff was
“too easy” and the proofs that sledgehammer found always referred to a
particular locale assumption. A couple candidates noticed that there
was an outright inconsistency: Isabelle was allowing proofs of
anything within the relevant locale. But I knew that the locale’s
assumptions were consistent, as the code base also successfully
instantiated that locale.Upon debugging this behavior and suspecting Isabelle version issues, I
finally saw that Isabelle2025-1 had been released only days before I
assigned this challenge problem. Indeed, a look through the
Isabelle2025-1 change log quickly revealed the problem (to me, not to
the candidates, most of whom were completely new to Isabelle and
mostly new to proof assistants in general):" - Removed predicate single_valuedp. Use predicate right_unique
instead. INCOMPATIBILITY.”The locale assumption I mentioned above was of the form
“single_valuedp R” for a concrete single-valued predicate-relation R,
but to the candidates who had accidentally downloaded and used
Isabelle2025-1 instead of Isabelle2025, the ‘single_valuedp’ was being
interpreted as a function variable rather than a constant, and
implicitly universally quantified, so the locale assumption was in
effect that all predicates were true of R. Oops.I’ll be the first to admit that this incident was partly my fault, for
not watching the Isabelle mailing list closely at that time and
noticing that an Isabelle2025-1 had just been released, and in turn
failing to warn the challenge problem candidates not to use that
brand-new version. But especially given that “Isabelle2025” had been
stable and unchanged through almost all of the year 2025, I was not
anticipating a new variant also called more-or-less “Isabelle2025"
being released only in the last few weeks of 2025, let alone that
release including major compatibility-breaking changes like the
complete removal of long-stable standard constants from Main.I also have no argument against this particular change; “right_unique”
is a perfectly fine name too. But I’m just suggesting that it would
be nice if compatibility-breaking changes like this could be scheduled
for the next “major” Isabelle release that increases the year number,
i.e., Isabelle2026. (I had carefully instructed the candidates to
download and use “Isabelle2025” and no other version; I only didn’t
know at the time that an “Isabelle2025-1” had just gone up.).As a result of this breaking change slipped into Isabelle2025-1, quite
a few sharp and eager potential new Isabelle users were not only
extremely confused but lost in some cases days of effort to this
versioning issue until I had the time to debug the problem for them.As a related issue with the Isabelle home page, it is fairly
non-obvious exactly how to find and download prior Isabelle releases —
even recently-prior releases like Isabelle2025. It would be nice if
pointers to the websites of at least a few prior versions (especially
including the original “base version” for a given year) were readily
accessible from the home page for those looking for exactly a
particular version. Upon debugging the above issue, I had to resort
to manual URL-editing to find and point the candidates to the “old”
Isabelle2025 website so they could download the correct version.Just a few versioning thoughts, FWIW.
Thanks
Bryan
Email Gateway (Feb 25 2026 at 10:50):From: Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk>
Ok, but my point remains that “Isabelle2025-1” sounds like it should be a minor release, probably to anyone not already entrenched in the Isabelle community (certainly to me, and I have actually used Isabelle on and off intermittently since around 2001).
And your answer also does not address my main suggestion that regardless of tradition, maybe it would be a “good thing” if Isabelle did have some sort of major/minor versioning distinction, however the naming works. If only for the simple reason that that’s a standard best practice for software engineering and maintenance practically everywhere now, for good reasons. (see my experience above for just one of innumerable types of undesirable situations that having major/minor versioning practice is good at preventing.)
Bryan
On Feb 25, 2026, at 10:40, Fabian Huch <huch@in.tum.de> wrote:
I think you are misunderstanding the versioning scheme -- Isabelle2025-1 is not a 'minor' release, it is simply the second release in the year 2025 (this happens regularly since the release cycle is a bit shorter than one year). Releases are always immutable and will not be changed.
For the naming of the second release in one year, there hasn't been a better proposal than adding a number postfix.
We did have a second special Isabelle2025-2 release over Isabelle2025-1, where an important problem was solved. An argument can be made that such special releases could be named differently.
Fabian
On 2/25/26 02:48, Bryan Alexander Ford (via cl-isabelle-users Mailing List) wrote:
I’m sorry if a form of this question has been discussed multiple times during Isabelle’s past decades of evolution, but nevertheless: wouldn’t it be nice if Isabelle releases followed a best-practice major/minor versioning discipline, so that we could normally rely on minor-version releases to make only backwards-compatible changes?To be clear, I’m not proposing to change Isabelle’s whole version numbering system, in particular the tradition of using a year as more-or-less a “major” version number and suffixes like “-1” for incremental updates within a year. I see nothing wrong with that tradition. Rather, I’m just suggesting that it would be nice if we could rely on incompatible changes mostly being reserved for “major” year-number releases like Isabelle2026, and for “minor” releases like “Isabelle2025-1” to avoid such compatibility-breaking changes.
I’ll briefly relate an incident in which the Isabelle2025-1 release in particular “bit” me and a group of undergraduate students in the past couple months. In late December I was evaluating applications for undergraduate summer internships in my lab at EPFL, including quite a few candidates to work with Isabelle/HOL on our Grounded Arithmetic or GA project (https://bford.info/pub/lang/ga/). As part of the evaluation process I gave these candidates a “challenge problem” involving actually using Isabelle2025 for some nontrivial theorem-proving in a subset of the GA code base. But soon a few of these candidates started noticing strange behavior: proving stuff was “too easy” and the proofs that sledgehammer found always referred to a particular locale assumption. A couple candidates noticed that there was an outright inconsistency: Isabelle was allowing proofs of anything within the relevant locale. But I knew that the locale’s assumptions were consistent, as the code base also successfully instantiated that locale.
Upon debugging this behavior and suspecting Isabelle version issues, I finally saw that Isabelle2025-1 had been released only days before I assigned this challenge problem. Indeed, a look through the Isabelle2025-1 change log quickly revealed the problem (to me, not to the candidates, most of whom were completely new to Isabelle and mostly new to proof assistants in general):
" - Removed predicate single_valuedp. Use predicate right_unique instead. INCOMPATIBILITY.”
The locale assumption I mentioned above was of the form “single_valuedp R” for a concrete single-valued predicate-relation R, but to the candidates who had accidentally downloaded and used Isabelle2025-1 instead of Isabelle2025, the ‘single_valuedp’ was being interpreted as a function variable rather than a constant, and implicitly universally quantified, so the locale assumption was in effect that all predicates were true of R. Oops.
I’ll be the first to admit that this incident was partly my fault, for not watching the Isabelle mailing list closely at that time and noticing that an Isabelle2025-1 had just been released, and in turn failing to warn the challenge problem candidates not to use that brand-new version. But especially given that “Isabelle2025” had been stable and unchanged through almost all of the year 2025, I was not anticipating a new variant also called more-or-less “Isabelle2025" being released only in the last few weeks of 2025, let alone that release including major compatibility-breaking changes like the complete removal of long-stable standard constants from Main.
I also have no argument against this particular change; “right_unique” is a perfectly fine name too. But I’m just suggesting that it would be nice if compatibility-breaking changes like this could be scheduled for the next “major” Isabelle release that increases the year number, i.e., Isabelle2026. (I had carefully instructed the candidates to download and use “Isabelle2025” and no other version; I only didn’t know at the time that an “Isabelle2025-1” had just gone up.).
As a result of this breaking change slipped into Isabelle2025-1, quite a few sharp and eager potential new Isabelle users were not only extremely confused but lost in some cases days of effort to this versioning issue until I had the time to debug the problem for them.
As a related issue with the Isabelle home page, it is fairly non-obvious exactly how to find and download prior Isabelle releases — even recently-prior releases like Isabelle2025. It would be nice if pointers to the websites of at least a few prior versions (especially including the original “base version” for a given year) were readily accessible from the home page for those looking for exactly a particular version. Upon debugging the above issue, I had to resort to manual URL-editing to find and point the candidates to the “old” Isabelle2025 website so they could download the correct version.
Just a few versioning thoughts, FWIW.
Thanks
Bryan
Email Gateway (Feb 25 2026 at 10:51):From: Lawrence Paulson <lp15@cam.ac.uk>
On 25 Feb 2026, at 01:48, Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk> wrote:
I’m sorry if a form of this question has been discussed multiple times during Isabelle’s past decades of evolution, but nevertheless: wouldn’t it be nice if Isabelle releases followed a best-practice major/minor versioning discipline, so that we could normally rely on minor-version releases to make only backwards-compatible changes?
During the 1990s, we did make a distinction between major and minor releases. But for most software, minor releases are bug fixes, and we don't get that many bugs to fix. These days, all of our releases should be considered as major.
Unfortunately, I in particular have been careless about upwards compatibility, due to the gradual growth of Isabelle's user base from a handful of researchers to what it is today. At least the person who had made that change had bothered to document it, which is more than I remember to do. But we do have quite an elaborate release process with multiple release candidates, and that is the right time to look out for and report incompatibilities.
Almost all prior releases can be found here: https://www.cl.cam.ac.uk/~lp15/archive/
Larry
Email Gateway (Feb 25 2026 at 12:52):From: Fabian Huch <huch@in.tum.de>
On 2/25/26 11:50, Bryan Alexander Ford wrote:
Ok, but my point remains that “Isabelle2025-1” sounds like it should be a minor release, probably to anyone not already entrenched in the Isabelle community (certainly to me, and I have actually used Isabelle on and off intermittently since around 2001).
And your answer also does not address my main suggestion that regardless of tradition, maybe it would be a “good thing” if Isabelle did have some sort of major/minor versioning distinction, however the naming works.
So what scheme are you proposing? Year-number "major" releases doesn't
work as I explained.
Fabian
Email Gateway (Feb 25 2026 at 14:27):From: Makarius <makarius@sketis.net>
On 25/02/2026 02:48, Bryan Alexander Ford (via cl-isabelle-users Mailing List)
wrote:
I’m sorry if a form of this question has been discussed multiple times during
Isabelle’s past decades of evolution, but nevertheless: wouldn’t it be nice if
Isabelle releases followed a best-practice major/minor versioning discipline,
so that we could normally rely on minor-version releases to make only
backwards-compatible changes?
I do agree that Isabelle release names are confusing, but I still have no
better idea than continuing the tradition started by Larry Paulson.
Even worse, I now tend to read "best practice" as "bad habits", because it
does not quite work out in reality. Looking through the list of contributing
components of Isabelle (see Admin/components/main in the repository), there is
a zoo of funny version schemes, and none of them can be relied upon. Every
version needs to be treated as a fresh and unique thing, without upgrade or
downgrade order.
For example, the Scala project with X.Y.Z versioning scheme superficially
looks accurate, with major.minor.patch releases, but it isn't. The Scala guys
do de-facto major releases on an increment of the last digit!
The best I've seen so far are Java releases: they rarely case a problem, but
the release and version scheme is very complicated. Luckily, it can be ignored.
As a related issue with the Isabelle home page, it is fairly non-obvious
exactly how to find and download prior Isabelle releases — even recently-prior
releases like Isabelle2025. It would be nice if pointers to the websites of
at least a few prior versions (especially including the original “base
version” for a given year) were readily accessible from the home page for
those looking for exactly a particular version.
There is https://isabelle.in.tum.de/download_past.html with a link to it on
the "Installation" part of the website. Not really obvious, but it has been
there for almost 2 decades, so "old habits" will work here.
Makarius
Email Gateway (Feb 25 2026 at 14:32):From: Makarius <makarius@sketis.net>
On 25/02/2026 11:51, Lawrence Paulson wrote:
These days, all of our releases should be considered as major.
Yes, indeed.
The only exception are the "emergency releases" Isabelle2013-2 (December 2013)
and Isabelle2025-2 (January 2026). They don't have a specific naming scheme,
because emergencies are so exceptional.
But we do have quite an elaborate release process with multiple release candidates, and that is the right time to look out for and report incompatibilities.
Definitely.
The timetable for Isabelle2026 (October 2026) is already available:
https://sketis.net/2025/plan-for-isabelle2026-october-2026
Makarius
Email Gateway (Feb 26 2026 at 21:54):From: Makarius <makarius@sketis.net>
On 25/02/2026 15:27, Makarius wrote:
Even worse, I now tend to read "best practice" as "bad habits", because it
does not quite work out in reality.
This guy makes a long and entertaining story out of it:
https://hynek.me/articles/semver-will-not-save-you
I would say the answer to all uncertainty about versions is to be explicit,
and refer to https://isabelle.in.tum.de/website-Isabelle2025-2 as a constant,
and not to https://isabelle.in.tum.de as a variable ("the latest release"), or
even worse "the latest repository version that only I know, but won't tell".
Makarius
Email Gateway (Feb 27 2026 at 06:55):From: "Achim D. Brucker" <adbrucker@0x5f.org>
I would say the answer to all uncertainty about versions is to be
explicit, and refer to
https://isabelle.in.tum.de/website-Isabelle2025-2 as a constant, and
not to https://isabelle.in.tum.de as a variable ("the latest
release"), or even worse "the latest repository version that only I
know, but won't tell".This is what I do in the documentation in my projects and, e.g., also
when submitting artefacts for evaluations (in particular when a new
Isabelle release is happening during the review period). Overall, this
really works well!
The only minor suggestion/request I have is that we have a similar
stable link for the AFP. Either on the AFP website itself (the last AFP
release that works with a specific Isabelle version) or that the
(archived) Isabelle website for old releases contains a link to the
latest AFP archive that works with this specific Isabelle release. This
would really be useful for ensuring re-usability of artefacts.
Best,
Achim
PS: Yes, I do store my local archives and provide them usually to
reviewers as well. Still, having a public archive for older releases
would be helpful, also when trying to "revive" works of colleagues.
Last updated: Mar 14 2026 at 08:38 UTC