[isabelle-dev] Extracting dependencies from theory headers

[Gerwin Klein]

On 31/12/2010, at 12: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.

Sounds entirely reasonable to me.


> 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.

Is anyone in particular working on that? 

Cheers,
Gerwin