[isabelle-dev] HOL-ex

[Klein, Gerwin (Data61, Kensington NSW)]

> On 1 Jun 2020, at 05:52, Makarius <makarius at sketis.net> wrote:
> 
> On 31/05/2020 21:19, Lawrence Paulson wrote:
> 
>> 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
> decades.
> 
> See also my NEWS reading on the Isabelle 2020 Workshop:
> 
> https://files.sketis.net/Isabelle_Workshop_2020/Isabelle_2020_paper_7.pdf
> 
> """
> As a future clarification of the session structure, session sub-directories
> could be
> 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
> Prover
> IDE would present tags via a suitable GUI presentation, e.g. a “tag cloud” instead
> of an old-fashioned directory tree.
> “"


Can you say a bit more about how this would look like? It seems to me that tags don’t conflict with a session using multiple directories (sub or otherwise). 

Maybe I don’t really understand what you mean by duplicates. Doesn’t the current (Isabelle2020) session structure already prevent duplicates? 

I find a session A with multiple directories fairly natural for larger applications. In l4v for instance we have a session ASpec that has subdirectories ARM, X64, RISC-V and so on, which contains theories that are included in ASpec theories via "$L4V_ARCH/Some_Theory”, where L4V_ARCH will be one of those subdirectories. Neither ASpec on its own nor the subdirectory ARM on its own form a useful session — in fact, the pattern is that almost every theory in ASpec has a corresponding theory in "$L4V_ARCH/" that contains the platform-dependent part of the formalisation which is included in the generic part. I’m not quite sure how we would replicate that kind of structure in a tag-based system. We could possibly put everything into the same directory and use file name variations, but that sounds like a complete mess to me.

Cheers,
Gerwin