Re: [isabelle] Theory name conflict



Le lundi 17 janvier 2011 21:00:48, Makarius a écrit :
> On Mon, 17 Jan 2011, Mathieu Giorgino wrote:
> > 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.
> 
> Yes, that's a "normal" feature of paths in theory imports.
> 
> > 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 is strange.  Can you try this all-inclusive version?
> 
>    http://www4.in.tum.de/~wenzelm/test/Isabelle_14-Jan-2011/download.html

It's still the same. Reading this:

  theory Scratch
    imports
    "~~/src/HOL/Imperative_HOL/Array"
    "/home/giorgino/repos/afp/thys/Collections/common/Array"
  begin

or this:

  theory Scratch
    imports
    "~~/src/HOL/Imperative_HOL/Array"
    "/non/existing/path/Array"
    "a/relative/non/existing/path/Array"
    "/home/giorgino/repos/afp/thys/Collections/common/Array"
  begin

  term Array

works like a charm. I think that if any non-existing path ending with the name 
of an imported theory is ignored, it should be the same for existing ones, 
else this "normal" feature could have been avoided (unless there is a reason 
for this one ?).

> What is your OS, Proof General and Emacs version anyway?

I work on an Archlinux x86-64
with isabelle2009-2 or isabelle-dev
and ProofGeneral-4.1pre110112
and GNU Emacs 23.2.1

Mathieu





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