<div dir="auto"><div><br><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Sep 29, 2021, 12:09 Martin Desharnais <<a href="mailto:martin.desharnais@posteo.de">martin.desharnais@posteo.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi all,<br>
<br>
> In my view the current schema has the following weaknesses:<br>
> * No separator between »Isabelle« and year (an imitation of CaMlCaSe).<br>
> * Two numeric identifiers side by side.<br>
> <br>
> None of these is pressing enough to change the current schema, but if we<br>
> change the schema, they should be addressed.<br>
> <br>
> Personally I'd go with sth. like<br>
> <br>
>       Isabelle-2021-Dec<br>
<br>
Note that this suggestion, while very readable, cannot be correctly <br>
sorted by the lexicographical order used by many tools (e.g. ls, sort).<br>
<br>
I am not certain what the perceived problem with two numeric identifiers <br>
is. Something like Isabelle-2021-02 and Isabelle-2021-12 looks readable <br>
to me. This is well known from the Ubuntu naming scheme (e.g. Ubuntu <br>
21.04, Ubuntu 21.10).<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">Apropos Ubuntu naming scheme: Most version numbers I am aware of use dots as separator. Moreover, there is a difference between the version number and the name of the thing. How about</div><div dir="auto"><br></div><div dir="auto">  Isabelle 2021</div><div dir="auto">  Isabelle 2021.01</div><div dir="auto">  Isabelle 2021.02</div><div dir="auto">  ...</div><div dir="auto"><br></div><div dir="auto">(where the version is only the part after the space and maybe the first one should be "Isabelle 2021.00")?</div><div dir="auto"><br></div><div dir="auto">Just my 2 cents.</div><div dir="auto"><br></div><div dir="auto">cheers</div><div dir="auto"><br></div><div dir="auto">Chris</div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Regards,<br>
Martin<br>
_______________________________________________<br>
isabelle-dev mailing list<br>
<a href="mailto:isabelle-dev@in.tum.de" target="_blank" rel="noreferrer">isabelle-dev@in.tum.de</a><br>
<a href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev" rel="noreferrer noreferrer" target="_blank">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a><br>
</blockquote></div></div></div>