[isabelle-dev] Unification of doc sessions vs. doc names
makarius at sketis.net
Mon Oct 1 16:48:46 CEST 2012
On Sat, 22 Sep 2012, Florian Haftmann wrote:
> Currently, we have still the ancient walking-by of doc sessions (e.g.
> IsarImplementation – note the CaMeL case) and corresponding document
> names (e.g. implementation). Is there anything speaking against
> unifying these now?
When I turned doc-src into more regular src/Doc some weeks ago, I
remembered that you have pointed out this question before, but I did not
see yet a direction where to move.
If you take the session IsarRef and its resulting document isar-ref, it is
both fairly non-standard. A proper session name would be Isar_Ref.
Or one could de-unifiy things with the other sessions and call it isar_ref
in conformance with its isar_ref.pdf. This would simplify the situation
in "isabelle build_doc", but deviate from normal session naming and
existing public names like http://isabelle.in.tum.de/doc/isar-ref.pdf
To add more to the confusion, there are also some regular sessions that
produce some manual:
* HOL-SPARK-Manual with regular document.pdf
* Collections (AFP) with document.pdf and userguide.pdf
All these variants have good reasons to exisit. Where is the general
direction to move? I don't see it yet.
More information about the isabelle-dev