[isabelle-dev] HOL-ex

Fri Jun 5 03:51:34 CEST 2020

> 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