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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
