[isabelle-dev] Extracting dependencies from theory headers
noschinl at in.tum.de
Tue Jan 4 08:19:35 CET 2011
On 30.12.2010 14:17, Makarius wrote:
> 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.
What do you intend as the replacement of the load path? For things like
HOL/Library or the AFP, named roots (i.e. paths like
"AFP:Abstract-Rewriting/Abstract_Rewriting") could do the trick, but I
don't see what is wrong about a properly implemented load path (i.e.
paths not stored in images; without the relative path naming anomalies I
outlined above; maybe distinguishing between references relative to the
master_dir or to the load path, like '#include "..."' and '#include
<...>' in C).
Absolute paths like you introduced in 64cd30d6b0b8 only work for core
Isabelle, not for the AFP.
More information about the isabelle-dev