[isabelle-dev] Extracting dependencies from theory headers

[Lars Noschinski]

On 19.11.2010 11:49, Makarius wrote:
> On Fri, 19 Nov 2010, Alexander Krauss wrote:
>
>> - Relative paths are not resolved by the current simple parser. I
>> remember that there used to be some oddities in PG related to relative
>> paths. I am not sure what the situation is now. What is the meaning of
>> a relative path in an "imports" or "uses" declaration?
[...]
> In principle the relatively recent "master path" concept should solve
> all that, but its needs to be done right once and for all in the Scala
> layer. The add_path stuff should disappear at some point, with the usual
> delay in deleting old features.

I did some tests to see how this master path concept works (by loading 
theories with convoluted imports in isabelle tty). My current 
understanding is as follows:

For a path P, let name(P) be the last component of the past and base(P) 
the remaining components.

  - For each theory file, its "master directory" is the directory, the
    theory file is located in.

  - When theory A imports theory B, then Isabelle searches

      (1) master_dir(A)/B
      (2) current_dir/name(B)
      (3) $LOAD_PATH/name(B)
          (for some load paths, includes e.g. Library for HOL)

(If I read the code correctly, (2) belongs to (3), as current_dir is 
part of the load path).

Is this understanding correct?

While I agree with (1), I'm a bit sceptical about (2) and (3). For one, 
it seems strange to drop base(B) in this cases -- is this intentional?
One should either use B here (or perhaps drop (2) and (3) completely, if 
B is not just a theory name).

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

Greetings, Lars