[isabelle-dev] Extracting dependencies from theory headers

[John Matthews]

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

-------------- 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/c8a12fd9/attachment.bin>