[isabelle-dev] Extracting dependencies from theory headers
krauss at in.tum.de
Tue Jan 4 09:31:03 CET 2011
>> Last summer I've made another round in clearing out the confusion,
>> working towards a stateless model based solely on the master directory,
> 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
The main point now is to remove old features rather than add new ones.
> Absolute paths like you introduced in 64cd30d6b0b8 only work for core
> Isabelle, not for the AFP.
Note that paths may contain environment variables from the settings. So
for now we could use the convention that $AFP is the thys directory of
the afp. This pretty much does what you propose. The IsaFoR project uses
this approach already.
More information about the isabelle-dev