[isabelle-dev] erroneous "Legacy feature" warnings about secondary search path

[Makarius]

On Thu, 13 Jan 2011, Brian Huffman wrote:

> I recently discovered that warnings about the secondard search path are 
> generated more often than they ought to be. I am using repository 
> version 1fa4725c4656.
>
> Create two files A.thy and B.thy with the following contents:
>
> theory A
> imports "~~/src/HOL/Library/Cardinality"
> begin
> end
>
> theory B
> imports A
> begin
> end
>
> Theory A loads an arbitrary file from HOL/Library, which is included
> in the legacy default search path, although the full path is given
> here to avoid the "Legacy feature" warning.
>
> If I load theory A by itself in ProofGeneral, it imports
> Cardinality.thy without warning. Similarly, if I load theory B by
> itself in ProofGeneral, there is no warning. But if I have both A.thy
> and B.thy open in ProofGeneral, step through A.thy first, and *then*
> start stepping through B.thy, I get the following warning when I
> import A from B:
>
> ### Legacy feature! File "Cardinality.thy" located via secondary
> search path: "$ISABELLE_HOME/src/HOL/Library

Thanks for isolating this problem.  This is due to an omission in 
ProofGeneral.inform_file_processed/Thy_Info.register_thy that is now 
addressed in bd0bebf93fa6.  If it had not been 
$ISABELLE_HOME/src/HOL/Library above, which happens to be still in the 
load path, Proof General would have failed to find that file.

It seems that theory import paths have always had this problem.  This 
might also explain why some AFP sessions provide seemingly redundant load 
paths, probably to ensure that one of the many ways of finding files 
happens to work.  Removing more an more such features, the situation 
should become more clear-cut, until we arrive at proper theory name spaces 
with well-defined rules for locating corresponding sources.


 	Makarius