Towards Isabelle2025-1-RC3 and AFP release

[Makarius]

On 27/11/2025 22:48, Gerwin Klein wrote:
> 
>> On 27 Nov 2025, at 22:20, Makarius <makarius at 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