[isabelle-dev] Extracting dependencies from theory headers
matthews at galois.com
Thu Dec 30 16:55:28 CET 2010
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
and theory B has statement
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?
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
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 2205 bytes
Desc: not available
More information about the isabelle-dev