[isabelle-dev] Consolidation of manual naming
makarius at sketis.net
Wed Apr 9 13:17:40 CEST 2014
On Mon, 7 Apr 2014, Florian Haftmann wrote:
>>> Nevertheless I still think its a good idea to spend half an hour to
>>> establish a more strict name correspondance while keeping the
>>> (lowercase) document names stable, e.g.
>>> foo-bar <-:-> Foo_Bar
>> I now see b266e7a86485 with foo-bar <-:-> Foo-Bar.
>> It is still unclear to me what the actual confusion was, and what is the
>> improvement. A "-" within a session name is obsolete for a long time --
>> it is in conflict with session-qualified theory names and plain long_id
>> token syntax. (That is not very relevant for Doc sessions, though.)
> When inspecting the ROOT file I saw the session name for »ZF-Logics« and
> gave that some authority.
> Maybe it is best if I will move on »ZF_Logics« etc. in yet another
> iteration to get rid of these historic names. At least that made the
> confusion apparent.
I still don't understand what the confusion actually is. These things are
really old, especially the "logics" manuals, which used to be just one
latex document a long time ago. It is not always possible to have
immediately obvious canonical names for everything -- there are often
conflicting side-conditions etc.
We do have a tradition to get things right eventually, but for that there
needs to be a clear direction, and some level of significance for a change
to be considered: it needs 2-3 good reasons, not just half a reason.
More information about the isabelle-dev