[isabelle-dev] Extracting dependencies from theory headers

[John Matthews]

> then will Isabelle look for theory C in dir1 or dir1/dir2 ?

Oops, that should be "dir2 or dir1/dir2".

-john

On Dec 30, 2010, at 7:55 AM, John Matthews wrote:

> Thanks Makarius, I believe that addresses my use-case.
>
> Another question: If the user asks Isabelle to process theory A, and  
> theory A has statement
>
>  imports "dir1/B"
>
> and theory B has statement
>
>  imports "dir2/C"
>
> then will Isabelle look for theory C in dir1 or dir1/dir2 ?
>
> In other words, does master_dir change to the enclosing directory of  
> the theory being imported?
>
> Thanks,
> -john
>
> On Dec 30, 2010, at 5:17 AM, Makarius wrote:
>
>> On Wed, 22 Dec 2010, Gerwin Klein wrote:
>>
>>> 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.
>>
>> This thread is getting almost as entangled as the history of the  
>> sources for this long standing issue.
>>
>> Last summer I've made another round in clearing out the confusion,  
>> working towards a stateless model based solely on the master  
>> directory, which is the location of the enclosing theory file when  
>> traversing the import graph.  Thus the implicit use of current  
>> directory or load path can be discontinued eventually, but user  
>> theories have to be adapted a bit.
>>
>> In Isabelle/00b2b6716ed8 the legacy status of the load path feature  
>> is made explicit.  I have also cleared out the Isabelle  
>> distribution already. AFP/00b2b6716ed8 still has approximately 200  
>> files that are located via the "secondary search path", as can be  
>> seen by grepping for that text the log files.
>>
>>
>> 	Makarius
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- 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/20101230/8a601a83/attachment.bin>