On 27/09/2021 18:54, Martin Desharnais wrote: > > Three > emperors in a year are certainly to be avoided at all cost, but it cannot be > excluded entirely. The naming scheme should have a solution in such situation. > What would happen if a critical bug was discovered in Isabelle2021-Dec?
This is always a very unusual situation, one of big crisis of the state. There would be at least two possibilities to address it: * Use the older tag scheme to make an amendment, e.g. Isabelle2021-Dec is superseded by Isabelle2021-Dec-1. * Delay the amendment long enough to allocate new month name, e.g. Isabelle2021-Dec is superseded by Isabelle2022-Jan. > An> lengthy solution would be to use ISO 8601 dates (e.g. Isabelle2021-12-01) but > is aesthetically disputable. We already have that for non-releases, using a different date standard, e.g. see current Isabelle_27-Sep-2021 from https://isabelle.sketis.net/devel/release_snapshot Playing with the endless possibilities of date formats, one could also imagine Isabelle_Dec-2021 (and thus Isabelle_Dec-2021-1 for an amendment that is never meant to happen under normal circumstances). Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
