Re: [isabelle] Theory name conflict



Le lundi 17 janvier 2011 07:54:19, Florian Haftmann a écrit :
> >> But
> >> 
> >>   theory Scratch
> >>   imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"
> >>   
> >>     "$PATH_TO_AFP/Collections/common/Array"
> >>   
> >>   begin
> >> 
> >> on its own works – not that I would call that a well-defined behaviour.
> > 
> > This looks strange, and should not import two different "Array"
> > theories. Which Isabelle version is this actually?
> 
> I am not able to reproduce this behaviour.  Maybe it was just an
> accidental situation while interactively changing the imports over and
> over.
> 
> 	Florian

I have tried this again and it worked... even when I discovered an error in my 
path to the afp... which is silently ignored by Isabelle. In fact, putting any 
path finishing with a theory name already existing in other imports,  is 
completely ignored.

For example:

  theory Scratch
    imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"
    "/non/existing/path/Array"
  begin

and

  theory Scratch
    imports "/non/existing/path/Nat"
  begin

are prefectly fine even after a new pull (41597:ced4f78bb728), update, HOL 
make.



Furthermore, I am still able to import two theories with the same name (after 
a check of the paths, and a "fresh" isabelle emacs)... and I can't see/imagine 
the difference with your configurations...





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.