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.
Alex _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
