[isabelle-dev] Extracting dependencies from theory headers

[Gerwin Klein]

Hi John,

On 22/12/2010, at 10:24 AM, John Matthews wrote:
>> On 22/12/2010, at 2:52 AM, Lars Noschinski wrote:
>>> Furthermore, I would argue that current_dir should not be part of the load_path while recursively loading dependencies. The only time current_dir should be considered is when loading a theory file "from the toplevel
>> 
>> Seconded. This causes quite a bit of confusion every time new users come in.
> 
> I'm not quite sure what "recursive dependencies" means here. However I think it's important to support the use-case where a new-ish user decides to split their single theory into two or more separate theories in the same directory and have one theory import the others. Would this still be supported?

I would hope so. I would think that only one search path is necessary, but I don't understand what is meant by master_dir, I missed that part of the discussion. 

Maybe I should expand on what really causes the confusion in my experience: a difference between interactive work and batch session, maybe because you have started your interactive session somewhere random which breaks reliance on the current directory. Another source of confusion in theory loading is that you can leave out the path when the theory you are referring to is already processed (either manually or of it is in the base image), but you need something the theory loader finds correctly when it is processed as a dependency. 

In the absence of a name space for theory names, it is important to be able to use relative paths in imports. 

Where that relative path is based in doesn't matter so much if the base location can be controlled (either by search path or other means) and if doesn't change for strange reasons.

Cheers,
Gerwin