[isabelle-dev] HOL-ex

[Tobias Nipkow]

I am afraid I do not understand the problem with subdirectories and the need to 
have "tags", "tag clouds" and "topics". Why is "A_B.thy" better than "A/B.thy"? 
What are the ill-defined situations? Are there other systems (not necessarily 
theorem provers) out there that jettison subdirectories because of the confusion 
they cause?

Tobias

On 03/06/2020 21:44, Makarius wrote:
> On 01/06/2020 02:54, Klein, Gerwin (Data61, Kensington NSW) wrote:
>>
>> 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?
> 
> Tags would be a slight extension of what is already there as "command
> markers", probably for the 'theory' command with special treatment in certain
> situations.
> 
> It would be merely an extra hint to group theories within sessions, without
> any structural impact nor naming of theories.
> 
> 
> In contrast, session-subdirectories introduce slightly ill-defined situations
> about files vs. actual theories. E.g. the accidental presence or absence of a
> file in one of multiple directories can change the session content in subtle ways.
> 
> We have started with a very badly defined situation many years ago, and now
> have a chance to make a last step to have it all clear: 1-1 theory vs. file
> relation without any special tricks.
> 
> 
>> I find a session A with multiple directories fairly natural for larger applications.
> 
> IIRC, you were the first one to introduce that in MicroJava. Ever since, a lot
> of extra complexity and unclarity has come from it.
> 
> (Not directly related: I have started to make my own jokes about the
> subdirectories of Isabelle/Pure, saying that the multiple directories obscure
> the structure of a logically flat arrangement. Quite often I get lost myself,
> and other people have hardly any chance to locate a named ML module on the spot.)
> 
> 
>> 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 don't quite understand this. Can you point to the actual source?
> 
> Does it mean you dynamically change the session content via the L4V_ARCH
> environment variable?
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200604/f3a9ff26/attachment.bin>