[isabelle-dev] AFP build times out in file/theory presentation

[Gerwin Klein]

> On 16 Nov 2021, at 22:24, Makarius <makarius at sketis.net> wrote:
> 
> On 16/11/2021 09:16, Gerwin Klein wrote:
>> You were too fast :-), afp-devel is is for isabelle-devel, it shouldn't have isabelle-release changes in it.
> 
> We have had this time of uncertainty of the pair isabelle-dev vs. afp-devel
> after the fork of isabelle-dev to isabelle-release routinely in the past few
> years.
> 
> From the Isabelle side, the "window of uncertainty" is only 30min .. 2h. For
> AFP we often had many days, sometimes 1-2 weeks (IIRC).
> 
> So can this be organized in a better way?
> E.g. have the "call to finalize AFP" earlier in the process and maybe have a
> separate "afp-release" fork for it.

You're right that the uncertainty period is not really ideal. It relies on there not being any major content changes in isabelle-release. Often that works fine, but occasionally content drift does happen as it did this cycle.

What I've usually done in the past (and now) when content drift occurs, is what you suggest, i.e. an afp-release fork, which here is directly getting the name afp-2021-1. It can get that name, because the model for the AFP is that the release remains a separate fork, so what now operates as the pre-release fork will become the official release fork when everything is done.

We could remove the uncertainty period by always doing that and coordinating on the fork time. I'd be happy to try that out for the next release. 


>> After the fork we should temporarily revert that commit for Complex_Bounded_Operators in afp-devel (but keep it on afp-2021-1) until the release has happened.
> Note that I will occasionally merge isabelle-release back to isabelle-dev
> before final lift-off. It will happen within 2-3 days, for example.

That is nice, and makes the situation with afp-devel a bit easier to manage (the smaller the merge in the end, the less work there is at the actual release point).

Cheers,
Gerwin