[isabelle-dev] Extracting dependencies from theory headers

[John Matthews]

That all makes sense, thanks.

-john

On Dec 21, 2010, at 4:42 PM, Gerwin Klein wrote:

> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2205 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101221/ce718780/attachment.bin>