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