[isabelle-dev] HOL-ex

[Makarius]

That old thread about sessions with multiple source directories is still
pending. Conceptually it causes a lot of extra worries and complexity, but I
don't see a proper way to eliminate it in the foreseeable future.

So this "feature" will stay and we will have to "patch" various "bugs" coming
from it eventually.


	Makarius

On 05/06/2020 03:51, Klein, Gerwin (Data61, Kensington NSW) wrote:
> 
> 
>> On 4 Jun 2020, at 03:44, Makarius <makarius at sketis.net> 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.
> 
> Can you give an example of how it would look like?
> 
> 
>> 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 agree that the session content should be fully statically declared (not dependent on
> pure file presence), but I thought we have already achieved that now, so I’m probably
> still missing something. Are you worried about a situation where referring to theory
> “A” in a structure like this:
> 
> ./A.thy
> ./dir/A.thy
> 
> is not uniquely defined? My understanding is that “A" currently (in Isabelle2020) 
> can only refer to "./A.thy” from files in “.", never to “./dir/A.thy”, and that paths in
> import statements are relative to the location of the file, which uniquely pins down
> what they refer to. 
> 
> There is potential for confusion when e.g. "./dir/B.thy” imports “A”, which refers to
> "./dir/A.thy" and then B is moved a directory higher, but when we move theories
> around we’d expect to have to adjust paths.
> 
> 
>>> 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.
> 
> That was David before me :-), I just kept using what was there.
> 
> 
>> (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.)
> 
> It is true that it is sometimes hard to figure out where to find things, but would a flat file
> system structure really help that? It might make it even worse.
> 
> This is actually a fairly deep discussion in the sense that the opinion of the human/computer
> interface field has gone back and forth a few times. Things started out flat, then file systems
> got directories/tree structure. Similar on desktops, first flat, then very soon folders to group icons.
> Same on phones, initially flat structure on e.g. the iPhone UI, fairly soon with folders.
> Then some of these went back to flat structures, seeing the file system more as a database,
> tags instead of structure on web pages such as blogs as well as in gmail. Most programming
> languages take the deep directory structure approach coupled with their module system,
> because it does mesh nicely with principles of abstraction, but the people packaging a large
> number of modules/libraries also tend to provide search functions to help navigate that structure. 
> 
> In the AFP we have a flat top-level structure for entires, with freedom internal to the entries,
> and a hierarchical structure of the topic index, but the ability of entries to be a member of
> multiple topics, which makes those topics tags. 
> 
> I can’t really say if one is better than the other, humans are overwhelmed quickly by either
> of them when there is too much content. But I do think that at least tags and directories are
> orthogonal. There is no reason one would contradict the other.
> 
> 
>>> 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?
> 
> Yes, what the session ASpec is depends on the value of that variable. In that sense there 
> are multiple ASpec sessions, and in fact multiple instances of the entire session structure
> (and completely different proofs).
> 
> These instances don’t interoperate with each other, i.e. it does not make sense to have
> an ARM session interact with an X64 session, and if you’d try to build one on the other,
> the proof just fails.
> 
> This is the ASpec session in the ROOT file:
> https://github.com/seL4/l4v/blob/isabelle-2020/spec/ROOT#L30-L58
> 
> This is an example of a generic session importing an architecture-dependent session:
> https://github.com/seL4/l4v/blob/isabelle-2020/spec/abstract/Structures_A.thy#L14-L17
> 
> For L4V_ARCH=ARM, this will import this theory, which itself imports generic theories:
> https://github.com/seL4/l4v/blob/isabelle-2020/spec/abstract/ARM/Arch_Structs_A.thy#L13-L18
> 
> For L4V_ARCH=X64, it is this theory instead:
> https://github.com/seL4/l4v/blob/isabelle-2020/spec/abstract/X64/Arch_Structs_A.thy
> 
> What is important, is that generic theories can refer to architecture-dependent names
> generically when these (by convention) offer the same name.
> 
> For instance, the type `arch_cap` is defined in both Arch_Structs_A theories, and is
> used in the generic Structures_A.
> 
> Cheers,
> Gerwin
>