[isabelle-dev] HOL-ex

[Makarius]

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