> On 1 Jun 2020, at 05:52, Makarius <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
