Email Gateway (Jul 25 2023 at 13:12): Email Gateway (Jul 25 2023 at 13:12):From: Makarius <makarius@sketis.net>
Isabelle2023-RC2 is planned for Wednesday 26-Jul-2023. This is the last chance
to sort out minor things for it, especially NEWS and CONTRIBUTORS.
On Friday 28-Jul-2023, I will travel to Warsaw and attend ITP 2023 in
Bialystok next week.
After the conference, Isabelle2023-RC3 will emerge rather quickly: we need to
make serious moves towards a final version. RC3 will be also the fork of
isabelle-dev vs. isabelle-release repositories --- in the past we have usually
had it at RC2 or RC3.
What is the schedule for the corresponding AFP release?
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jul 26 2023 at 13:52):From: Makarius <makarius@sketis.net>
On 25/07/2023 15:11, Makarius wrote:
Isabelle2023-RC2 is planned for Wednesday 26-Jul-2023. This is the last chance
to sort out minor things for it, especially NEWS and CONTRIBUTORS.
It will take a few hours than anticipated: I am still waiting for some AFP
test that became necessary after revisiting a change that is a non-regression
wrt. Isabelle2022 (and thus strictly speaking not relevant for Isabelle2023),
but it has caused some confusion wrt. Isabelle2021-1:
changeset: 75840:f8c412a45af8
user: wenzelm
date: Sat Aug 13 14:29:59 2022 +0200
summary: more accurate treatment of option "editor_output_state", e.g.
when changed via Isabelle/jEdit Plugin Options panel;
There might be something still coming about this today: I've spend 1-2 days
sorting things out.
In the meantime I had to eliminate erratic noise on the isabelle-dev repository:
changeset: 78468:33bc244eafdb
tag: tip
user: wenzelm
date: Wed Jul 26 15:42:13 2023 +0200
files: src/Tools/jEdit/src/output_dockable.scala
description:
revert adhoc change ab9cc7cda0ec: lacks reasoning (and discussion);
changeset: 78467:ab9cc7cda0ec
user: kleing
date: Wed Jul 26 15:06:06 2023 +0200
files: src/Tools/jEdit/src/output_dockable.scala
description:
output panel: don't discard already filtered messages
I have no time to give a lecture on how Isabelle development has worked the
past decade(s).
When making a change, one always needs to provide proper reasoning (usually
based on the recorded history). And maybe also start a discussion with the
one(s) who is reposible for that part of the system.
ab9cc7cda0ec has no proof. Sorry.
What is the schedule for the corresponding AFP release?
This question is still open.
We already have a tradition of delaying the Isabelle/AFP release 2-3 weeks
without any particular reasons.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jul 26 2023 at 14:24):From: Makarius <makarius@sketis.net>
There was some minimal reasoning here:
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2023-05/msg00045.html
Note that silence about proposals for changes does not mean acceptance. (I
did not answer at that point, due to lack of historical context and since it
was formally no regression from Isabelle2022 to Isabelle2023; thus it could
wait another release cycle).
The Sydney group is a major user of Isabelle and thus has its own vital
interests that quality standards don't degrade!
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 06 2023 at 20:01):From: Makarius <makarius@sketis.net>
On 25/07/2023 15:11, Makarius wrote:
Isabelle2023-RC2 is planned for Wednesday 26-Jul-2023. This is the last chance
to sort out minor things for it, especially NEWS and CONTRIBUTORS.On Friday 28-Jul-2023, I will travel to Warsaw and attend ITP 2023 in
Bialystok next week.
I am now back from Warsaw and Białystok, where I have learned the proper
Polish spelling of the name (and the pronunciation). I have also learned about
local dishes in the Babka restaurant at the city center (Polish, Russian,
Belarussian, Ukrainian, Lithunian), and the very interesting beverage of
Kvass, e.g. in this Lithunian variety (thick and sweet):
https://esklep.spolembialystok.pl/strona-glowna/165785-naturalny-litewski-kwas-backoriu-05-l-uab-lompart-4779020201075.html
Back in wet and cold Bavaria, it is now time to pick up all open threads, and
target at Isabelle2023-RC3 on 09..10-Aug-2023. That will also be the fork
point of the isabelle-dev vs. isabelle-release repository.
Afterwards, isabelle-dev will in principle be ready for anything intended for
the next release after Isabelle2023, but bigger changes need to wait for the
corresponding AFP release and fork-point.
What is the schedule for the corresponding AFP release?
My guess: we will see another 3-5 weeks delay for no particular reason.
Such things could be done concurrently, e.g. with Isabelle RC1 or RC2.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 08 2023 at 10:02):From: Gerwin Klein <kleing@unsw.edu.au>
The main precondition for the AFP fork is that the tests are stable, including the slow ones. If we have a full passing run with Isabelle2023-RC3, a week or two after RC3 would be a good point for the AFP to fork as well, which should put the AFP release very shortly after the Isabelle release.
I’ll announce the fork point on isabelle-users when RC3 is out.
We will also attempt to empty the queue of submissions, but that can be relatively independent of the fork point for afp-devel.
I’m still travelling, so things might be a bit slower than usual, but I will be travelling for the entire release period, so there is no point in waiting for anything.
Cheers,
Gerwin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 08 2023 at 10:46):From: Makarius <makarius@sketis.net>
I always do a full AFP test before publishing an Isabelle release candidate.
Now even for ARM64, thanks to recent efforts by David Matthews (see
Isabelle/5683e49f7884). This became possible due to the availability of proper
test hardware at TUM.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 08 2023 at 11:31):From: Gerwin Klein <kleing@unsw.edu.au>
Perfect, then we don’t need to wait for the slow test to kick in.
With that I’d say we should do the AFP fork one week after the Isabelle fork to give some time for the last flurry of activity that tends to happen when deadlines approach.
Cheers,
Gerwin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 08 2023 at 13:10):From: Makarius <makarius@sketis.net>
OK, lets do that.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 27 2024 at 20:14 UTC