Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Theory name conflict

view this post on Zulip Email Gateway (Aug 18 2022 at 16:48):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Mathieu,

unfortunately, not.

@Peter: maybe we should consider renaming one of these, e.g.
~~/src/HOL/Imperative_HOL/Array.thy to Arr.thy. But I do not see a
natural choice here, maybe you do.

Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 16:49):

From: Alexander Krauss <krauss@in.tum.de>

Is there an easy "user side" way to get rid of it without renaming one of
them?

unfortunately, not.

Yes... it's a known (and very annoying when you hit it) limitation of
the current flat theory namespace.

@Peter: maybe we should consider renaming one of these, e.g.
~~/src/HOL/Imperative_HOL/Array.thy to Arr.thy. But I do not see a
natural choice here, maybe you do.

Making the name shorter will inevitably provoke new conflicts. If you
change it, make it longer, e.g. Heap_Array. Users usually don't import
this theory individually, only the via Imperative_HOL entry point.

But I now see that the theory name is intended as a qualifier for
constants... Could one achieve this behavior using other means, e.g., a
vacuous locale or something?

Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 16:50):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
In principle, yes. But it is a complication and cluttering, no
simplification.

Let us again revisit the actual situation:

"~~/src/HOL/Imperative_HOL/Array"
"afp/thys/Collections/common/Array"

If I understand correctly, the problem is that fact names (also constant
names?) in Collections shadow some in Imperative_HOL. My intention is
to refrain from any modification of the existing theories if there is
»natural« way to do so.

So maybe a user-space workaround is an intermediate theory

theory Heap_Array
imports "~~/src/HOL/Imperative_HOL/Array"
begin

lemmas xyz = Array.xyz

...

end

and then in the main theory the imports

"~~/src/HOL/Imperative_HOL/Heap_Array"
"afp/thys/Collections/common/Array"

which would allow to access the facts mirrored in Heap_Array by
Heap_Array.xyz.

Would this solve your issue?

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 16:51):

From: Alexander Krauss <krauss@in.tum.de>
No. The problem is that you simply cannot load two theories of the same
name.

Try the following:

theory Scratch
imports "~~/src/HOL/Imperative_HOL/Array"
"$PATH_TO_AFP/Collections/common/Array"
begin

term array_of_list

Interestingly, you don't even get an error, but the second theory is
silently ignored but not loaded.

Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 16:53):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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.

Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 16:53):

From: Alexander Krauss <krauss@in.tum.de>
When I try it, it loads Imperative_HOL, but nothing from Collections.

Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 16:53):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
I've been too long to answer but it could anyway explain a little more the
problem.

Let us again revisit the actual situation:

"~~/src/HOL/Imperative_HOL/Array"
"afp/thys/Collections/common/Array"

If I understand correctly, the problem is that fact names (also constant
names?) in Collections shadow some in Imperative_HOL. My intention is
to refrain from any modification of the existing theories if there is
»natural« way to do so.

In fact, all objects defined or imported by the last in the import list (the
last read theory ?) are hidden.

For example, in the reverse situation:

"afp/thys/Collections/common/Array"
"~~/src/HOL/Imperative_HOL/Array"

where "Imperative_HOL/Array" imports "Heap_Monad" which imports "Heap",

term Array.get
thm Array.noteq_sym

term Heap_Monad.Heap
typ "'a Heap_Monad.Heap"

thm Heap.addr_of_array_inj
typ Heap.heap
term Heap.empty

are all hidden, and so trying to import this:

"afp/thys/Collections/common/Array"
"~~/src/HOL/Imperative_HOL/Ref" (* where Ref imports Array*)

or this:

"~~/src/HOL/Imperative_HOL/Array"
"afp/thys/Collections/common/ArrayHashMap_Impl"

results in errors, as "Ref" uses the type "Heap.heap" and ArrayHashMap_Impl
uses constant "Array.array_get".

Then, it is impossible to import "Collections" (importing "ArrayHashMap_Impl")
and "Imperative_HOL" (importing "Ref") at the same time.

So maybe a user-space workaround is an intermediate theory
...
Would this solve your issue?

It would not solve the issue as the intermediate theory would have to be
inserted in "Collections" or "Imperative_HOL" and it would then be easier to
change one theory name.

I will try to import selectively theories "Ref" and "Mrec" of "Imperative_HOL"
as I don't use "Imperative_HOL" arrays anyway... but I could have...

I hope to see soon localization of theories...

Thank you both,

Mathieu

view this post on Zulip Email Gateway (Aug 18 2022 at 16:55):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Hello all,

I'm having a conflict on theory names from HOL and afp, one theory hiding
definitions of the other one (according to the order of imports).

"~~/src/HOL/Imperative_HOL/Array"
"afp/thys/Collections/common/Array"

I got this while updating my theories using both Imperative_HOL and
Collections.

Is there an easy "user side" way to get rid of it without renaming one of
them?

Thanks,

Mathieu Giorgino

view this post on Zulip Email Gateway (Aug 18 2022 at 16:57):

From: Makarius <makarius@sketis.net>
On Wed, 5 Jan 2011, Florian Haftmann wrote:

No. The problem is that you simply cannot load two theories of the same
name.

Try the following:

theory Scratch
imports "~~/src/HOL/Imperative_HOL/Array"
"$PATH_TO_AFP/Collections/common/Array"
begin

term array_of_list

Interestingly, you don't even get an error, but the second theory is
silently ignored but not loaded.

This is a known feature of theory import paths, which have been added as
an afterthought some years ago, and never really worked. Stay tuned until
we get proper sessions with theory name spaces.

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?

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 16:57):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I am not able to reproduce this behaviour. Maybe it was just an
accidental situation while interactively changing the imports over and over.

Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 16:57):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
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...

view this post on Zulip Email Gateway (Aug 18 2022 at 16:58):

From: Makarius <makarius@sketis.net>
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

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

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 16:59):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 16:59):

From: Alexander Krauss <krauss@in.tum.de>
Mathieu Giorgino wrote:
What do you mean with "works like a charm". What is the behaviour you
see? I would expect that the declaration is accepted but the second
theory is not loaded. Is that correct? If yes, "works like a charm" is a
bit of a euphemism. If no, what happens exactly?

Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 16:59):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Yes, sorry... I mean that the declaration is accepted but the second theory is
not loaded.

Mathieu

Last updated: Apr 23 2024 at 12:29 UTC