[isabelle-dev] Extracting dependencies from theory headers

Alexander Krauss 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 mailing list