makarius at sketis.net
Sun May 31 23:52:29 CEST 2020
On 31/05/2020 21:19, Lawrence Paulson wrote:
> Tobias has pointed out that directory ex is easily overlooked these days and perhaps we should rename it, e.g. to Examples. Any comments?
That directory is a rather ancient Isabelle tradition, but already 10-15 years
ago, it has declined in relevance: most examples are rather odd experiments,
so "ex" could just as well mean that.
We could think of genuine examples in a new HOL-Examples session, without 90%
of the odd stuff. But this would also mean to reform sessions like
HOL-Isar_Examples in a similar manner.
In the past 10 years, I have de-facto used the "Examples" slot of the
Isabelle/jEdit Documentation panel to refer to other sessions with examples.
> Conceivably it could be subdivided, as it seems to have 94 entries.
Now might be actually a good time to disallow sub-directories of a session
directory. They have accumulated a lot of confusion and problems in the past
See also my NEWS reading on the Isabelle 2020 Workshop:
As a future clarification of the session structure, session sub-directories
superseded by “tags” to group theories via “topics”. Thus the space of session-
qualified theories would directly correspond to the file-system arrangement, with-
out the potential confusion via duplicates in different sub-directories. The
IDE would present tags via a suitable GUI presentation, e.g. a “tag cloud” instead
of an old-fashioned directory tree.
More information about the isabelle-dev