Thanks Makarius, I believe that addresses my use-case.
Another question: If the user asks Isabelle to process theory A, and theory A has statement
imports "dir1/B" and theory B has statement imports "dir2/C" then will Isabelle look for theory C in dir1 or dir1/dir2 ?In other words, does master_dir change to the enclosing directory of the theory being imported?
Thanks, -john On Dec 30, 2010, at 5:17 AM, Makarius wrote:
On Wed, 22 Dec 2010, Gerwin Klein wrote:I would think that only one search path is necessary, but I don't understand what is meant by master_dir, I missed that part of the discussion.This thread is getting almost as entangled as the history of the sources for this long standing issue.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.In Isabelle/00b2b6716ed8 the legacy status of the load path feature is made explicit. I have also cleared out the Isabelle distribution already. AFP/00b2b6716ed8 still has approximately 200 files that are located via the "secondary search path", as can be seen by grepping for that text the log files.Makarius
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
