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) > <[email protected]> wrote: > > > >> 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
