[isabelle-dev] HOL-ex

[Klein, Gerwin (Data61, Kensington NSW)]

ps: the very next point in the paper (long theory names) would be very useful to us!

Cheers,
Gerwin

> On 1 Jun 2020, at 08:54, Klein, Gerwin (Data61, Kensington NSW) <Gerwin.Klein at data61.csiro.au> wrote:
> 
> 
> 
>> 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
>