Email Gateway (Nov 27 2025 at 11:23): Email Gateway (Nov 27 2025 at 11:23):From: Makarius <makarius@sketis.net>
My original plan was to publish the next release candidate yesterday, but I
was too busy elsewhere and a few notable points are still open. It will happen
within a few days.
We are already > 3 weeks into the official release process, and the
isabelle-dev repository is still blocked. I usually try to keep that state of
uncertainty at approx. 2 weeks (which is already quite a lot). Sometimes
people get uneasy to push changes that are for the next release onto it.
The fork of isabelle-dev vs. isabelle-release should have happened for RC2,
but without AFP moving as well, it would merely cause even more confusion. So
what is the current plan AFP? We have again a situation of "several weeks
delay for no particular reasons", do we?
Makarius
Email Gateway (Nov 27 2025 at 11:23):From: Makarius <makarius@sketis.net>
My original plan was to publish the next release candidate yesterday, but I
was too busy elsewhere and a few notable points are still open. It will happen
within a few days.
We are already > 3 weeks into the official release process, and the
isabelle-dev repository is still blocked. I usually try to keep that state of
uncertainty at approx. 2 weeks (which is already quite a lot). Sometimes
people get uneasy to push changes that are for the next release onto it.
The fork of isabelle-dev vs. isabelle-release should have happened for RC2,
but without AFP moving as well, it would merely cause even more confusion. So
what is the current plan AFP? We have again a situation of "several weeks
delay for no particular reasons", do we?
Makarius
Email Gateway (Nov 27 2025 at 21:48):From: Gerwin Klein via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
On 27 Nov 2025, at 22:20, Makarius <makarius@sketis.net> wrote:
My original plan was to publish the next release candidate yesterday, but I was too busy elsewhere and a few notable points are still open. It will happen within a few days.
We are already > 3 weeks into the official release process, and the isabelle-dev repository is still blocked. I usually try to keep that state of uncertainty at approx. 2 weeks (which is already quite a lot). Sometimes people get uneasy to push changes that are for the next release onto it.
There's no reason why there should be urgency to add new features for after the current release into the repo right now. It’s easy in distributed version control to wait with such merges. It’s good that we have the fork process, but that should be a safety feature, not an excuse for chaos.
The fork of isabelle-dev vs. isabelle-release should have happened for RC2, but without AFP moving as well, it would merely cause even more confusion. So what is the current plan AFP? We have again a situation of "several weeks delay for no particular reasons", do we?
I’ve been busy elsewhere as well, but we can do the AFP fork soon. Let me announce it for Mon, we’ll see if that sparks the usual last minute panic requests.
Cheers,
Gerwin
This email and any files transmitted with it may contain confidential information. If you believe you have received this email or any of its contents in error, please notify me immediately by return email and destroy this email. Do not use, disseminate, forward, print or copy any contents of an email received in error.
Email Gateway (Nov 28 2025 at 12:08):From: Makarius <makarius@sketis.net>
On 27/11/2025 22:48, Gerwin Klein wrote:
On 27 Nov 2025, at 22:20, Makarius <makarius@sketis.net> wrote:
The fork of isabelle-dev vs. isabelle-release should have happened for RC2, but without AFP moving as well, it would merely cause even more confusion. So what is the current plan AFP? We have again a situation of "several weeks delay for no particular reasons", do we?
I’ve been busy elsewhere as well, but we can do the AFP fork soon. Let me announce it for Mon, we’ll see if that sparks the usual last minute panic requests.
Great.
So I can announce RC3 with the repository fork for Mon 01-Dec-2025 or Tue
02-Dec-2025 at 11:00 RBT (Royal Bavarian Time). I will tell later which day it
will be.
The fork will happen at the same time. Anything still happening on
isabelle-dev until the fork is for Isabelle2025-1 release: It should be
finalization / polishing of already present things, no new "features", no "bug
fixes" for old problems from past releases.
Makarius
Email Gateway (Nov 28 2025 at 16:54):From: Makarius <makarius@sketis.net>
On 27/11/2025 22:48, Gerwin Klein wrote:
On 27 Nov 2025, at 22:20, Makarius <makarius@sketis.net> wrote:
My original plan was to publish the next release candidate yesterday, but I was too busy elsewhere and a few notable points are still open. It will happen within a few days.
We are already > 3 weeks into the official release process, and the isabelle-dev repository is still blocked. I usually try to keep that state of uncertainty at approx. 2 weeks (which is already quite a lot). Sometimes people get uneasy to push changes that are for the next release onto it.
There's no reason why there should be urgency to add new features for after the current release into the repo right now. It’s easy in distributed version control to wait with such merges. It’s good that we have the fork process, but that should be a safety feature, not an excuse for chaos.
Gerwin, we do have a big chaos already: more and more post-release changes on
isabelle-dev are coming in. (These are things that are not strictly necessary
to turn RC2 into a proper stable release eventually.)
From long years of experience as release manager, that is caused by having >
2 weeks of "uncertainty" on the status of isabelle-dev: Is it before or after
the release? How does it relate to afp-devel? Shall I push now or much later?
We cannot change that situation for now, but I am hoping for next time, which
means that the Isabelle release schedule is properly aligned with AFP
beforehand --- it will save a lot of time for both of us.
Right now, I will merely apply the specification of the "before-vs-after
release point" semantically to current isabelle-dev vs. isabelle-release, with
the side-condition that the persistent history is not messed up unnecessarily.
Thus the feature additions by Tobias shortly after RC2 are included by
accident, because they are already on isabelle-release: 58fc6856e31a
concerning HOL-Library.While, 65734c8badd5 concerning newly introduced
HOL-Library.Time_Functions. Obscure corners of HOL-Library are not main HOL,
after all.
Other changes and feature additions by Martin and Jasmin on main HOL
(concerning cvc5 and metis) are not included: 764bc386d7dc etc. and a12a78878d4a.
The fork-point for the release shall be:
changeset: 83654:52cd371a36dd
user: wenzelm
date: Wed Nov 26 20:00:47 2025 +0100
files: Admin/Mercurial/mercurial-6.1.4-hgweb.patch
description:
adhoc patch for hgweb.wsgi: provide "hg clone" via HTTP without suffering from
Denial-of-Service attacks on website content (e.g. by Non-Intelligent Agents);
I will write a formal posting later today, to explain the status of the
different repositories, as usual. In particular, changes for the release need
to be sent to me via email, and not pushed onto isabelle-dev at the same time.
We are already late in the release process, and the year is approaching its
end. I hope to be able to publish the final and ultimate release until
17-Dec-2025, still within the plan that was published some months ago:
https://sketis.net/2025/plan-for-isabelle2025-1-december-2025
Here is also a notable quotation from that post:
"""
Important: Contributors need to have things ready for RC1 or RC2. There need
to be several weeks left to consolidate everything, before the release becomes
final and unchangable (until the subsequent release).
"""
Makarius
Email Gateway (Nov 28 2025 at 17:35):From: Tobias Nipkow <nipkow@in.tum.de>
On 28/11/2025 17:53, Makarius wrote:
Thus the feature additions by Tobias shortly after RC2 are included by accident,
because they are already on isabelle-release: 58fc6856e31a concerning HOL-
Library.While, 65734c8badd5 concerning newly introduced HOL-
Library.Time_Functions. Obscure corners of HOL-Library are not main HOL, after all.
It is called HOL-Library.While_Combinator and is one of the widely used theories
in HOL-Library. Less judgemental and more factual is shorter and better.
Tobias
Email Gateway (Nov 28 2025 at 18:53):From: Makarius <makarius@sketis.net>
On 28/11/2025 18:35, Tobias Nipkow wrote:
On 28/11/2025 17:53, Makarius wrote:
Thus the feature additions by Tobias shortly after RC2 are included by
accident, because they are already on isabelle-release: 58fc6856e31a
concerning HOL- Library.While, 65734c8badd5 concerning newly introduced HOL-
Library.Time_Functions. Obscure corners of HOL-Library are not main HOL,
after all.It is called HOL-Library.While_Combinator and is one of the widely used
theories in HOL-Library. Less judgemental and more factual is shorter and better.
"Widely used" would actually have been a point for excluding it from the
release. But things are as they are now.
Makarius
Email Gateway (Nov 30 2025 at 22:09):From: Makarius <makarius@sketis.net>
On 28/11/2025 13:08, Makarius wrote:
So I can announce RC3 with the repository fork for Mon 01-Dec-2025 or Tue 02-
Dec-2025 at 11:00 RBT (Royal Bavarian Time). I will tell later which day it
will be.
We are already past the repository fork. I will build Isabelle2025-1-RC3 from
https://isabelle.sketis.net/repos/isabelle-release (for "hg clone" or "hg
pull) on Mon 01-Dec-2025 RBT (Royal Bavarian Time).
Makarius
Last updated: Dec 10 2025 at 12:50 UTC