[isabelle-dev] Extracting dependencies from theory headers
noschinl at in.tum.de
Tue Dec 21 16:47:23 CET 2010
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
(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
More information about the isabelle-dev