Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems using the same theory name in differe...

Email Gateway (Aug 23 2022 at 08:33):

From: Makarius <makarius@sketis.net>
On 02/03/2020 16:43, Wolfgang Jeltsch wrote:

I want to have certain theories in different sessions to have the same
name, but currently I cannot make this work.

As an example, consider two sessions A and B, each of them
containing a theory named Core. If I have theory B.Core import
theory A.Core, Isabelle/jEdit gives me the following error message at
the beginning of B.Core:

exception THEORY raised (line 233 of "context.ML"):
• Duplicate theory name
• {..., HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main,
A.Core, B.Core}
• {..., HOL.Filter, HOL.Conditionally_Complete_Lattices,
HOL.Binomial, Main, A.Core}

Until a few years ago, bad things would happen without any error. It is
already some progress that it fails properly.

So far, I considered sessions to introduce their own name spaces, so
that A.Core and B.Core refer to different theories. Was this
assumption wrong, or am I just missing something that is necessary to
make such theory naming work?

There is a name space for theory names (session name "." theory name), and an
internal name space prefix for each theory: the latter is the theory base name.

This is done for two reasons:

(1) Extra qualification would make internal full names rather long. (One day
we will just do it, like we did for the theory prefix 20 years ago.)

(2) Many tools from the past 10 years expect the first name component of
internal type/const/thm names to be the theory. (I failed to convince tool
authors not to impose such assumptions on their implementations, so I will
have to come up with some smart trick eventually.)

For now the above is known and intended behaviour of the system.

Isabelle2020 will be again more efficient in handling session-qualified theory
names, but there is no change of the internal name space policy.

Makarius

Email Gateway (Aug 23 2022 at 08:37):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!

Thanks for the clarification.

Given that theory names appear to be global, what is the recommended way
for avoiding theory name clashes? The only really safe way I can imagine
would be something like including the session name in the theory name,
which would lead to names like Session.Session-Theory. However, this
seems odd to me.

What do other people do about this? In particular, how do other people
name theories that collect certain foundational or utility bits of a
session? I wanted to name those something like Foundations, but
apparently this is not a good idea.

All the best,
Wolfgang

Email Gateway (Aug 23 2022 at 08:38):

From: Manuel Eberl <eberlm@in.tum.de>
In my experience, this is really only an issue for those "lemma bucket"
theories that contain material that is not particularly interesting
and/or should probably be in the distribution.

I usually call those something like "<name of AFP entry>_Library", or,
if I have enough material to split it into several theories, "<name of
AFP entry>_Polynomial_Library" and "<name of AFP
entry>_Integration_Library" etc.

I don't think I've ever run into duplicate theory names. If this does
happen, I guess the only way around it is to rename one of the theories
in the AFP.

This is of course not ideal and if I recall correctly, properly
session-qualified theory names are something on Makarius's long-term to
do list.

There is another problem that is even more of a headache because there
is no workaround for it at all and no solution in sight, namely
conflicting type class instantiations. There the only solution is simply
to avoid type class instantiations whenever there is more than one
"sensible" instance.

Manuel

Email Gateway (Aug 23 2022 at 08:38):

From: Manuel Eberl <eberlm@in.tum.de>
Addendum: I guess this is simply because Isabelle was created over 30
years ago and back then nobody thought it would still be around 30 years
later and be used for developments as big as what we have today, so a
fancy module system wasn't really on the agenda.

(That is just my conjecture. I was not around back then – Isabelle is
quite a bit older than I am.)

Manuel

Email Gateway (Aug 23 2022 at 08:38):

From: Lawrence Paulson <lp15@cam.ac.uk>
Indeed. It’s inspiring to see old developments that took years of work and were huge at the time running in around 30s on modern machines. It’s awesome to see new developments built upon great hierarchies of other developments.

In the beginning, even constant names had global scope.

Larry

Email Gateway (Aug 23 2022 at 08:38):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!

I want to have certain theories in different sessions to have the same
name, but currently I cannot make this work.

As an example, consider two sessions A and B, each of them
containing a theory named Core. If I have theory B.Core import
theory A.Core, Isabelle/jEdit gives me the following error message at
the beginning of B.Core:

exception THEORY raised (line 233 of "context.ML"):
• Duplicate theory name
• {..., HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main,
A.Core, B.Core}
• {..., HOL.Filter, HOL.Conditionally_Complete_Lattices,
HOL.Binomial, Main, A.Core}

So far, I considered sessions to introduce their own name spaces, so
that A.Core and B.Core refer to different theories. Was this
assumption wrong, or am I just missing something that is necessary to
make such theory naming work?

All the best,
Wolfgang

Email Gateway (Aug 23 2022 at 08:41):

From: Makarius <makarius@sketis.net>
Technically, all names of the primitive logic are global. Over time we have
built a lot of extra-logical infrastructure to provide the appearance of
structured names and name space policies.

The idea to use even more qualification for long names is rather obvious, but
it will break many relatively recent tools that impose their own assumptions
about the structure of full names.

I do have some ideas to accommodate such tools eventually, but many other
things have higher priority.

Makarius

Email Gateway (Aug 23 2022 at 08:44):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Hi Wolfgang,

at least the namespace is not completely different.

E.g., if you define in A.Core a constant “foo", then the
internal name is “Core.foo” (no “A” attached).
Similarly, a “foo” within B.Core is also named “Core.foo” (no “B” attached).

So, it will be problematic to load both A.Core and B.Core.

e.g., in the concrete example below you will see that there will be no
occurrence of the session name HOL-Library in the name of the constant.

theory Scratch
imports
Main
"HOL-Library.Code_Target_Int"
begin

ML ‹
val x = @{term "Code_Target_Int.positive"}
|> Term.dest_Const
›

Best,
René
signature.asc

Last updated: Apr 25 2024 at 01:08 UTC