[isabelle-dev] erroneous "Legacy feature" warnings about secondary search path
makarius at sketis.net
Fri Jan 14 16:53:12 CET 2011
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"
> theory B
> imports A
> 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.
More information about the isabelle-dev