Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Duplicate theory name Discrete


view this post on Zulip Email Gateway (Nov 12 2024 at 20:25):

From: Paolo Crisafulli <paolo.crisafulli@irt-systemx.fr>
Hi all,

I have the following error message in a thy file which uses both
sessions Ordinary_Differential_Equations and HOL-CSPM:

exception THEORY raised (line 378 of "context.ML"):
  Duplicate theory name
  {..., Main, HOLCF.Porder, HOLCF.Pcpo, HOLCF.Cont, Discrete}
  {..., HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main,
Discrete}

A simple setup to reproduce the error is with the following theory:

theory MyTheory
  imports
    "HOLCF.Discrete"
    "HOL-Library.Library"
begin
end

and a ROOTS file such as:

/path/to/Isabelle2024/src/HOL

Any idea on how to fix this?

Thank you very much in advance.

Paolo

view this post on Zulip Email Gateway (Nov 13 2024 at 08:46):

From: Fabian Huch <huch@in.tum.de>
You cannot have two theories with the same base name in an import path
unfortunately (a limitation coming from a time when theories were
considered globally unique entities).

Currently, the only option (that I am aware of) is is to rename one of
the theories.

Fabian

On 11/12/24 21:25, Paolo Crisafulli wrote:

Hi all,

I have the following error message in a thy file which uses both
sessions Ordinary_Differential_Equations and HOL-CSPM:

exception THEORY raised (line 378 of "context.ML"):
  Duplicate theory name
  {..., Main, HOLCF.Porder, HOLCF.Pcpo, HOLCF.Cont, Discrete}
  {..., HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main,
Discrete}

A simple setup to reproduce the error is with the following theory:

theory MyTheory
  imports
    "HOLCF.Discrete"
    "HOL-Library.Library"
begin
end

and a ROOTS file such as:

/path/to/Isabelle2024/src/HOL

Any idea on how to fix this?

Thank you very much in advance.

Paolo

view this post on Zulip Email Gateway (Nov 13 2024 at 09:58):

From: bpuyobro <cl-isabelle-users@lists.cam.ac.uk>
Le 2024-11-13 09:46, Fabian Huch a écrit :

You cannot have two theories with the same base name in an import path
unfortunately (a limitation coming from a time when theories were
considered globally unique entities).

Currently, the only option (that I am aware of) is is to rename one of
the theories.

Fabian

On 11/12/24 21:25, Paolo Crisafulli wrote:

Hi all,

I have the following error message in a thy file which uses both
sessions Ordinary_Differential_Equations and HOL-CSPM:

exception THEORY raised (line 378 of "context.ML"):
  Duplicate theory name
  {..., Main, HOLCF.Porder, HOLCF.Pcpo, HOLCF.Cont, Discrete}
  {..., HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main,
Discrete}

A simple setup to reproduce the error is with the following theory:

theory MyTheory
  imports
    "HOLCF.Discrete"
    "HOL-Library.Library"
begin
end

and a ROOTS file such as:

/path/to/Isabelle2024/src/HOL

Any idea on how to fix this?

Thank you very much in advance.

Paolo

Hi, I'm currently working with Paolo and we share the issue.

Is there a way of renaming a theory during the import of said theory
(using long names maybe?) so that the solution of the issue is carried
in the theory file or should we just bruteforce it by renaming said
theory "by hand" in the HOL/Library folder (we would like to avoid this)
?

Regards,
Benjamin

view this post on Zulip Email Gateway (Nov 13 2024 at 11:58):

From: Makarius <makarius@sketis.net>
On 13/11/2024 09:46, Fabian Huch wrote:

You cannot have two theories with the same base name in an import path
unfortunately (a limitation coming from a time when theories were considered
globally unique entities).

Note that theory names are still globally unique, although the name is usually
qualified by the session name, so clashes don't occur in the session context.

There is an additional restriction for theories that are formally merged: base
names need to be unique, because thy are used for the standard name space
policy. One happy day, when the name space policies are changed --- after a
lot of hard work --- this restriction will disappear.

Currently, the only option (that I am aware of) is is to rename one of the
theories.

Yes, indeed.

Dirty tricks should be avoided. The planet needs to be kept clean and alive.

Although HOL-Library.Discrete could just as well be called something else,
e.g. HOL-Librrary.Discrete_Funs, it is probably easier to clean-up HOLCF a
little bit.

Here is historic evidence for the introduction of this theory in 1997:
https://isabelle-dev.sketis.net/rISABELLEc2508f4ab739

That is interesting on its own account: it shows how theory construction had
to alternate between .thy files (for specifications) and .ML files (for
proofs) a few decades ago.

Today there is very little motivation of have these few specifications and
proofs in the separate theory HOLCF.Discrete. The material could be moved to
the start of its descendent HOLCF.Lift (and maybe separated by 'section'
headings).

Makarius

view this post on Zulip Email Gateway (Nov 13 2024 at 12:51):

From: Manuel Eberl <manuel@pruvisto.org>
Hello,

it is somewhat rare to include all of HOL-Library in a theory. Usually
you only import the bits of it that you actually need.

If your work does not depend on HOL-Library.Discrete then I would
recommend to simply import the bits of HOL-Library that you explicitly need.

Of course we should try to make sure that at least within the HOL part
of the Isabelle distribution, no duplicate theory names occur. And in
the future, in the AFP as well.

Manuel

On 13/11/2024 10:48, bpuyobro (via cl-isabelle-users Mailing List) wrote:

Le 2024-11-13 09:46, Fabian Huch a écrit :

You cannot have two theories with the same base name in an import
path unfortunately (a limitation coming from a time when theories
were considered globally unique entities).

Currently, the only option (that I am aware of) is is to rename one
of the theories.

Fabian

On 11/12/24 21:25, Paolo Crisafulli wrote:

Hi all,

I have the following error message in a thy file which uses both
sessions Ordinary_Differential_Equations and HOL-CSPM:

exception THEORY raised (line 378 of "context.ML"):
  Duplicate theory name
  {..., Main, HOLCF.Porder, HOLCF.Pcpo, HOLCF.Cont, Discrete}
  {..., HOL.Transcendental, HOL.Complex, HOL.MacLaurin,
Complex_Main, Discrete}

A simple setup to reproduce the error is with the following theory:

theory MyTheory
  imports
    "HOLCF.Discrete"
    "HOL-Library.Library"
begin
end

and a ROOTS file such as:

/path/to/Isabelle2024/src/HOL

Any idea on how to fix this?

Thank you very much in advance.

Paolo

Hi, I'm currently working with Paolo and we share the issue.

Is there a way of renaming a theory during the import of said theory
(using long names maybe?) so that the solution of the issue is carried
in the theory file or should we just bruteforce it by renaming said
theory "by hand" in the HOL/Library folder (we would like to avoid
this) ?

Regards,
Benjamin

view this post on Zulip Email Gateway (Nov 13 2024 at 12:54):

From: Fabian Huch <huch@in.tum.de>

On 11/13/24 11:03, Manuel Eberl wrote:

Of course we should try to make sure that at least within the HOL part
of the Isabelle distribution, no duplicate theory names occur. And in
the future, in the AFP as well.

Note that the AFP submission checker explicitly warns of possible clashes.

Fabian

view this post on Zulip Email Gateway (Nov 13 2024 at 14:46):

From: Paolo Crisafulli <paolo.crisafulli@irt-systemx.fr>
Thank you for your responses, but does this mean that we should wait for
the next Isabelle release, as both HOL-Library and HOLCSP are part of it?

Is there a practical solution to allow us to submit our theories to AFP
before that?

(For the record, we can't apply this advice:

If your work does not depend on HOL-Library.Discrete then I would
recommend to simply import the bits of HOL-Library that you explicitly need.

We don't import anything directly from both HOL-Library or HOLCF, these
are transitive dependencies of HOL-CSPM and
Ordinary_Differential_Equations.)

Thank you all in advance for your help.

Best,

Paolo

On 13/11/2024 12:57, Makarius wrote:

On 13/11/2024 09:46, Fabian Huch wrote:

You cannot have two theories with the same base name in an import path
unfortunately (a limitation coming from a time when theories were considered
globally unique entities).
Note that theory names are still globally unique, although the name is usually
qualified by the session name, so clashes don't occur in the session context.

There is an additional restriction for theories that are formally merged: base
names need to be unique, because thy are used for the standard name space
policy. One happy day, when the name space policies are changed --- after a
lot of hard work --- this restriction will disappear.

Currently, the only option (that I am aware of) is is to rename one of the
theories.
Yes, indeed.

Dirty tricks should be avoided. The planet needs to be kept clean and alive.

Although HOL-Library.Discrete could just as well be called something else,
e.g. HOL-Librrary.Discrete_Funs, it is probably easier to clean-up HOLCF a
little bit.

Here is historic evidence for the introduction of this theory in 1997:
https://cas5-0-urlprotect.trendmicro.com:443/wis/clicktime/v1/query?url=https%3a%2f%2fisabelle%2ddev.sketis.net%2frISABELLEc2508f4ab739&umid=070888fe-b1e4-40d4-8c4b-fc350f75d77e&auth=b6005005a7b50bc3a68b2003f1e38d069f93f262-8a9ce3d82ace24c3827208341f125e1ee2693d94

That is interesting on its own account: it shows how theory construction had
to alternate between .thy files (for specifications) and .ML files (for
proofs) a few decades ago.

Today there is very little motivation of have these few specifications and
proofs in the separate theory HOLCF.Discrete. The material could be moved to
the start of its descendent HOLCF.Lift (and maybe separated by 'section'
headings).

Makarius

view this post on Zulip Email Gateway (Nov 13 2024 at 15:00):

From: Manuel Eberl <manuel@pruvisto.org>

We don't import anything directly from both HOL-Library or HOLCF,
these are transitive dependencies of HOL-CSPM and
Ordinary_Differential_Equations.)
If none of them actually need HOL-Library.Discrete one could change
those entries to simply not import it.

Other than that, the best option would probably to rename
HOL-Library.Discrete. In the long run, that is the only sensible option
anyway.

Is there a practical solution to allow us to submit our theories to
AFP before that?
Once the issue has been taken care of in afp-devel you can submit your
entry to afp-devel (https://devel.isa-afp.org/submission/). It will
however only appear in the official release version of the AFP after the
next Isabelle release (some time in Q1 of 2025, if I recall correctly).

I don't think there is a sensible way to submit your entry to the
"regular" AFP before then.

Cheers,

Manuel

On 13/11/2024 15:45, Paolo Crisafulli wrote:

Thank you for your responses, but does this mean that we should wait
for the next Isabelle release, as both HOL-Library and HOLCSP are part
of it?

Is there a practical solution to allow us to submit our theories to
AFP before that?

(For the record, we can't apply this advice:

If your work does not depend on HOL-Library.Discrete then I would
recommend to simply import the bits of HOL-Library that you explicitly
need.

We don't import anything directly from both HOL-Library or HOLCF,
these are transitive dependencies of HOL-CSPM and
Ordinary_Differential_Equations.)

Thank you all in advance for your help.

Best,

Paolo

On 13/11/2024 12:57, Makarius wrote:

On 13/11/2024 09:46, Fabian Huch wrote:

You cannot have two theories with the same base name in an import path
unfortunately (a limitation coming from a time when theories were
considered
globally unique entities).
Note that theory names are still globally unique, although the name
is usually
qualified by the session name, so clashes don't occur in the session
context.

There is an additional restriction for theories that are formally
merged: base
names need to be unique, because thy are used for the standard name
space
policy. One happy day, when the name space policies are changed ---
after a
lot of hard work --- this restriction will disappear.

Currently, the only option (that I am aware of) is is to rename one
of the
theories.
Yes, indeed.

Dirty tricks should be avoided. The planet needs to be kept clean and
alive.

Although HOL-Library.Discrete could just as well be called something
else,
e.g. HOL-Librrary.Discrete_Funs, it is probably easier to clean-up
HOLCF a
little bit.

Here is historic evidence for the introduction of this theory in 1997:
https://cas5-0-urlprotect.trendmicro.com:443/wis/clicktime/v1/query?url=https%3a%2f%2fisabelle%2ddev.sketis.net%2frISABELLEc2508f4ab739&umid=070888fe-b1e4-40d4-8c4b-fc350f75d77e&auth=b6005005a7b50bc3a68b2003f1e38d069f93f262-8a9ce3d82ace24c3827208341f125e1ee2693d94

That is interesting on its own account: it shows how theory
construction had
to alternate between .thy files (for specifications) and .ML files (for
proofs) a few decades ago.

Today there is very little motivation of have these few
specifications and
proofs in the separate theory HOLCF.Discrete. The material could be
moved to
the start of its descendent HOLCF.Lift (and maybe separated by 'section'
headings).

Makarius

view this post on Zulip Email Gateway (Nov 13 2024 at 17:45):

From: Paolo Crisafulli <paolo.crisafulli@irt-systemx.fr>
Thank you for you answer.

HOL-Library.Discrete is used by HOL-Analysis (in Summation_Tests), fully
imported by Ordinary_Differential_Equations.Linear_ODE, through
Bounded_Linear_Operator.

On the other hand, I have renamed HOL-Library.Discrete to LDiscrete (not
a great name, just testing), and it only requires a reasonable effort to
propagate the change:

./HOL/ex/Function_Growth.thy:19
./HOL/Library/Library.thy:1
./HOL/Library/LDiscrete.thy:24
./HOL/Analysis/Summation_Tests.thy:14

Didn't actually do it for the whole AFP, but it looks reasonable too:

$ grep -r -l "HOL-Library.Discrete" . | xargs grep -c Discrete
./thys/Bertrands_Postulate/Bertrand.thy:26
./thys/Universal_Turing_Machine/Recs_alt_Def.thy:1
./thys/Universal_Turing_Machine/Recs.thy:1
./thys/Vickrey_Clarke_Groves/MiscTools.thy:3
./thys/Pell/Efficient_Discrete_Sqrt.thy:23
./thys/Pell/Pell_Algorithm.thy:6
./thys/Hoare_Time/Nielson_Sqrt.thy:11
./thys/Hoare_Time/QuantK_Sqrt.thy:11
./thys/LLL_Basis_Reduction/LLL_Complexity.thy:1
./thys/Continued_Fractions/Quadratic_Irrationals.thy:8
./thys/Number_Theoretic_Transform/Butterfly.thy:4
./thys/DPRM_Theorem/Diophantine/Exponentiation.thy:1
./thys/Karatsuba_Sqrt/Karatsuba_Sqrt_Library.thy:8
./thys/Karatsuba_Sqrt/Karatsuba_Sqrt.thy:40

I am willing to do the job if necessary.

Any thoughts anyone?

Thank you,

Paolo

On 13/11/2024 15:59, Manuel Eberl wrote:

We don't import anything directly from both HOL-Library or HOLCF,
these are transitive dependencies of HOL-CSPM and
Ordinary_Differential_Equations.)
If none of them actually need HOL-Library.Discrete one could change
those entries to simply not import it.

Other than that, the best option would probably to rename
HOL-Library.Discrete. In the long run, that is the only sensible option
anyway.

Is there a practical solution to allow us to submit our theories to
AFP before that?
Once the issue has been taken care of in afp-devel you can submit your
entry to afp-devel (https://cas5-0-urlprotect.trendmicro.com:443/wis/clicktime/v1/query?url=https%3a%2f%2fdevel.isa%2dafp.org%2fsubmission%2f&umid=a4a9516f-bf37-440e-8da9-834154c471fb&auth=b6005005a7b50bc3a68b2003f1e38d069f93f262-e828e06bbdc7fff258c13967647d8aeeb6b4a4b2). It will
however only appear in the official release version of the AFP after the
next Isabelle release (some time in Q1 of 2025, if I recall correctly).

I don't think there is a sensible way to submit your entry to the
"regular" AFP before then.

Cheers,

Manuel

On 13/11/2024 15:45, Paolo Crisafulli wrote:

Thank you for your responses, but does this mean that we should wait
for the next Isabelle release, as both HOL-Library and HOLCSP are part
of it?

Is there a practical solution to allow us to submit our theories to
AFP before that?

(For the record, we can't apply this advice:

If your work does not depend on HOL-Library.Discrete then I would
recommend to simply import the bits of HOL-Library that you explicitly
need.

We don't import anything directly from both HOL-Library or HOLCF,
these are transitive dependencies of HOL-CSPM and
Ordinary_Differential_Equations.)

Thank you all in advance for your help.

Best,

Paolo

On 13/11/2024 12:57, Makarius wrote:

On 13/11/2024 09:46, Fabian Huch wrote:

You cannot have two theories with the same base name in an import path
unfortunately (a limitation coming from a time when theories were
considered
globally unique entities).
Note that theory names are still globally unique, although the name
is usually
qualified by the session name, so clashes don't occur in the session
context.

There is an additional restriction for theories that are formally
merged: base
names need to be unique, because thy are used for the standard name
space
policy. One happy day, when the name space policies are changed ---
after a
lot of hard work --- this restriction will disappear.

Currently, the only option (that I am aware of) is is to rename one
of the
theories.
Yes, indeed.

Dirty tricks should be avoided. The planet needs to be kept clean and
alive.

Although HOL-Library.Discrete could just as well be called something
else,
e.g. HOL-Librrary.Discrete_Funs, it is probably easier to clean-up
HOLCF a
little bit.

Here is historic evidence for the introduction of this theory in 1997:
https://cas5-0-urlprotect.trendmicro.com:443/wis/clicktime/v1/query?url=https%3a%2f%2fisabelle%2ddev.sketis.net%2frISABELLEc2508f4ab739&umid=070888fe-b1e4-40d4-8c4b-fc350f75d77e&auth=b6005005a7b50bc3a68b2003f1e38d069f93f262-8a9ce3d82ace24c3827208341f125e1ee2693d94

That is interesting on its own account: it shows how theory
construction had
to alternate between .thy files (for specifications) and .ML files (for
proofs) a few decades ago.

Today there is very little motivation of have these few
specifications and
proofs in the separate theory HOLCF.Discrete. The material could be
moved to
the start of its descendent HOLCF.Lift (and maybe separated by 'section'
headings).

Makarius

view this post on Zulip Email Gateway (Nov 13 2024 at 19:39):

From: Makarius <makarius@sketis.net>
On 13/11/2024 15:59, Manuel Eberl wrote:

Other than that, the best option would probably to rename HOL-
Library.Discrete. In the long run, that is the only sensible option anyway.

Looking again more closely, I now understand the rather generic name of theory
HOL-Library.Discrete: it defines qualified functions like Discrete.log.

In contrast, HOLCF.Discrete is merely "internal" to HOLCF and not used
directly elsewhere. So we could easily change that for Isabelle2025 (March
2025), using the included changeset.

Makarius

ch

view this post on Zulip Email Gateway (Nov 15 2024 at 12:33):

From: Lawrence Paulson <lp15@cam.ac.uk>
Theory Library/Discrete is headed "Common discrete functions”. I would suggest renaming it to Discrete_Functions in time for the next release. Quite apart from the propensity for name clashes, the current name is ambiguous.

Turning to HOLCF, many of the theories have short names that made perfect sense in 1997, but no longer. Some of them have the suffix _cpo, but unfortunately Discrete currently does not.

Larry

On 13 Nov 2024, at 10:03, Manuel Eberl <manuel@pruvisto.org> wrote:

Of course we should try to make sure that at least within the HOL part of the Isabelle distribution, no duplicate theory names occur. And in the future, in the AFP as well.

view this post on Zulip Email Gateway (Nov 15 2024 at 13:07):

From: Tobias Nipkow <nipkow@in.tum.de>
Good suggestions. Happy to take care of it later today.

Tobias

On 15/11/2024 13:32, Lawrence Paulson wrote:

Theory Library/Discrete is headed "Common discrete functions”. I would suggest renaming it to Discrete_Functions in time for the next release. Quite apart from the propensity for name clashes, the current name is ambiguous.

Turning to HOLCF, many of the theories have short names that made perfect sense in 1997, but no longer. Some of them have the suffix _cpo, but unfortunately Discrete currently does not.

Larry

On 13 Nov 2024, at 10:03, Manuel Eberl <manuel@pruvisto.org> wrote:

Of course we should try to make sure that at least within the HOL part of the Isabelle distribution, no duplicate theory names occur. And in the future, in the AFP as well.

smime.p7s

view this post on Zulip Email Gateway (Nov 15 2024 at 13:26):

From: Manuel Eberl <manuel@pruvisto.org>
As Makarius noted, the problem is that the functions defined in
"HOL-Library.Discrete" can (by design) only be used with their
fully-qualified names "Discrete.sqrt" and "Discrete.log".

I don't think we want "Discrete_Functions.log" since that's quite a
mouthful.

Personally I'm not a huge fan of "Discrete.log" and "Discrete.sqrt"
either. Perhaps something like "floorlog2" and "floorsqrt"? (cf. my
"ceillog2" that Larry recently moved into the distribution).
Alternatively "log2_nat" and "sqrt_nat" would also work, but then the
question arises what one should call the corresponding versions that
round up instead of down.

Manuel

On 15/11/2024 14:06, Tobias Nipkow wrote:

Good suggestions. Happy to take care of it later today.

Tobias

On 15/11/2024 13:32, Lawrence Paulson wrote:

Theory Library/Discrete is headed "Common discrete functions”. I
would suggest renaming it to Discrete_Functions in time for the next
release. Quite apart from the propensity for name clashes, the
current name is ambiguous.

Turning to HOLCF, many of the theories have short names that made
perfect sense in 1997, but no longer. Some of them have the suffix
_cpo, but unfortunately Discrete currently does not.

Larry

On 13 Nov 2024, at 10:03, Manuel Eberl <manuel@pruvisto.org> wrote:

Of course we should try to make sure that at least within the HOL
part of the Isabelle distribution, no duplicate theory names occur.
And in the future, in the AFP as well.

view this post on Zulip Email Gateway (Nov 15 2024 at 13:33):

From: Tobias Nipkow <nipkow@in.tum.de>

On 15/11/2024 14:25, Manuel Eberl wrote:

As Makarius noted, the problem is that the functions defined in "HOL-
Library.Discrete" can (by design) only be used with their fully-qualified names
"Discrete.sqrt" and "Discrete.log".

Sorry, yes, I'll leave Library.Discrete alone.

I don't think we want "Discrete_Functions.log" since that's quite a mouthful.

Personally I'm not a huge fan of "Discrete.log" and "Discrete.sqrt" either.
Perhaps something like "floorlog2" and "floorsqrt"? (cf. my "ceillog2" that
Larry recently moved into the distribution).

floor_log2? (Personally, I belive in having the important name components first
but can see that floor_log2 is more natural).

Tobias

Alternatively "log2_nat" and
"sqrt_nat" would also work, but then the question arises what one should call
the corresponding versions that round up instead of down.

Manuel

On 15/11/2024 14:06, Tobias Nipkow wrote:

Good suggestions. Happy to take care of it later today.

Tobias

On 15/11/2024 13:32, Lawrence Paulson wrote:

Theory Library/Discrete is headed "Common discrete functions”. I would
suggest renaming it to Discrete_Functions in time for the next release. Quite
apart from the propensity for name clashes, the current name is ambiguous.

Turning to HOLCF, many of the theories have short names that made perfect
sense in 1997, but no longer. Some of them have the suffix _cpo, but
unfortunately Discrete currently does not.

Larry

On 13 Nov 2024, at 10:03, Manuel Eberl <manuel@pruvisto.org> wrote:

Of course we should try to make sure that at least within the HOL part of
the Isabelle distribution, no duplicate theory names occur. And in the
future, in the AFP as well.

smime.p7s

view this post on Zulip Email Gateway (Nov 15 2024 at 13:49):

From: Manuel Eberl <manuel@pruvisto.org>
I'd be fine with "floor_log2" as well, but then you should adjust
"ceillog2" as well.

I think I picked "ceillog2" because there is something similar (but more
general) called "floorlog" elsewhere in the library.

On 15/11/2024 14:32, Tobias Nipkow wrote:

On 15/11/2024 14:25, Manuel Eberl wrote:

As Makarius noted, the problem is that the functions defined in "HOL-
Library.Discrete" can (by design) only be used with their
fully-qualified names "Discrete.sqrt" and "Discrete.log".

Sorry, yes, I'll leave Library.Discrete alone.

I don't think we want "Discrete_Functions.log" since that's quite a
mouthful.

Personally I'm not a huge fan of "Discrete.log" and "Discrete.sqrt"
either. Perhaps something like "floorlog2" and "floorsqrt"? (cf. my
"ceillog2" that Larry recently moved into the distribution).

floor_log2? (Personally, I belive in having the important name
components first but can see that floor_log2 is more natural).

Tobias

Alternatively "log2_nat" and "sqrt_nat" would also work, but then the
question arises what one should call the corresponding versions that
round up instead of down.

Manuel

On 15/11/2024 14:06, Tobias Nipkow wrote:

Good suggestions. Happy to take care of it later today.

Tobias

On 15/11/2024 13:32, Lawrence Paulson wrote:

Theory Library/Discrete is headed "Common discrete functions”. I
would suggest renaming it to Discrete_Functions in time for the
next release. Quite apart from the propensity for name clashes, the
current name is ambiguous.

Turning to HOLCF, many of the theories have short names that made
perfect sense in 1997, but no longer. Some of them have the suffix
_cpo, but unfortunately Discrete currently does not.

Larry

On 13 Nov 2024, at 10:03, Manuel Eberl <manuel@pruvisto.org> wrote:

Of course we should try to make sure that at least within the HOL
part of the Isabelle distribution, no duplicate theory names
occur. And in the future, in the AFP as well.

view this post on Zulip Email Gateway (Nov 15 2024 at 21:40):

From: Tobias Nipkow <nipkow@in.tum.de>
HOLCF.Discrete has been renamed to HOLCF.Discrete_Cpo.

Tobias

On 15/11/2024 14:06, Tobias Nipkow wrote:

Good suggestions. Happy to take care of it later today.

Tobias

On 15/11/2024 13:32, Lawrence Paulson wrote:

Theory Library/Discrete is headed "Common discrete functions”. I would suggest
renaming it to Discrete_Functions in time for the next release. Quite apart
from the propensity for name clashes, the current name is ambiguous.

Turning to HOLCF, many of the theories have short names that made perfect
sense in 1997, but no longer. Some of them have the suffix _cpo, but
unfortunately Discrete currently does not.

Larry

On 13 Nov 2024, at 10:03, Manuel Eberl <manuel@pruvisto.org> wrote:

Of course we should try to make sure that at least within the HOL part of the
Isabelle distribution, no duplicate theory names occur. And in the future, in
the AFP as well.

smime.p7s

view this post on Zulip Email Gateway (Nov 17 2024 at 13:51):

From: Tobias Nipkow <nipkow@in.tum.de>
Presumably this means Discrete.sqrt -> floor_sqrt as well?

Tobias

On 15/11/2024 14:48, Manuel Eberl wrote:

I'd be fine with "floor_log2" as well, but then you should adjust "ceillog2" as
well.

I think I picked "ceillog2" because there is something similar (but more
general) called "floorlog" elsewhere in the library.

On 15/11/2024 14:32, Tobias Nipkow wrote:

On 15/11/2024 14:25, Manuel Eberl wrote:

As Makarius noted, the problem is that the functions defined in "HOL-
Library.Discrete" can (by design) only be used with their fully-qualified
names "Discrete.sqrt" and "Discrete.log".

Sorry, yes, I'll leave Library.Discrete alone.

I don't think we want "Discrete_Functions.log" since that's quite a mouthful.

Personally I'm not a huge fan of "Discrete.log" and "Discrete.sqrt" either.
Perhaps something like "floorlog2" and "floorsqrt"? (cf. my "ceillog2" that
Larry recently moved into the distribution).

floor_log2? (Personally, I belive in having the important name components
first but can see that floor_log2 is more natural).

Tobias

Alternatively "log2_nat" and "sqrt_nat" would also work, but then the
question arises what one should call the corresponding versions that round up
instead of down.

Manuel

On 15/11/2024 14:06, Tobias Nipkow wrote:

Good suggestions. Happy to take care of it later today.

Tobias

On 15/11/2024 13:32, Lawrence Paulson wrote:

Theory Library/Discrete is headed "Common discrete functions”. I would
suggest renaming it to Discrete_Functions in time for the next release.
Quite apart from the propensity for name clashes, the current name is
ambiguous.

Turning to HOLCF, many of the theories have short names that made perfect
sense in 1997, but no longer. Some of them have the suffix _cpo, but
unfortunately Discrete currently does not.

Larry

On 13 Nov 2024, at 10:03, Manuel Eberl <manuel@pruvisto.org> wrote:

Of course we should try to make sure that at least within the HOL part of
the Isabelle distribution, no duplicate theory names occur. And in the
future, in the AFP as well.

smime.p7s

view this post on Zulip Email Gateway (Nov 17 2024 at 13:51):

From: Manuel Eberl <manuel@pruvisto.org>
That seems reasonable to me.

On 17/11/2024 14:50, Tobias Nipkow wrote:

Presumably this means Discrete.sqrt -> floor_sqrt as well?

Tobias

On 15/11/2024 14:48, Manuel Eberl wrote:

I'd be fine with "floor_log2" as well, but then you should adjust
"ceillog2" as well.

I think I picked "ceillog2" because there is something similar (but
more general) called "floorlog" elsewhere in the library.

On 15/11/2024 14:32, Tobias Nipkow wrote:

On 15/11/2024 14:25, Manuel Eberl wrote:

As Makarius noted, the problem is that the functions defined in
"HOL- Library.Discrete" can (by design) only be used with their
fully-qualified names "Discrete.sqrt" and "Discrete.log".

Sorry, yes, I'll leave Library.Discrete alone.

I don't think we want "Discrete_Functions.log" since that's quite a
mouthful.

Personally I'm not a huge fan of "Discrete.log" and "Discrete.sqrt"
either. Perhaps something like "floorlog2" and "floorsqrt"? (cf. my
"ceillog2" that Larry recently moved into the distribution).

floor_log2? (Personally, I belive in having the important name
components first but can see that floor_log2 is more natural).

Tobias

Alternatively "log2_nat" and "sqrt_nat" would also work, but then
the question arises what one should call the corresponding versions
that round up instead of down.

Manuel

On 15/11/2024 14:06, Tobias Nipkow wrote:

Good suggestions. Happy to take care of it later today.

Tobias

On 15/11/2024 13:32, Lawrence Paulson wrote:

Theory Library/Discrete is headed "Common discrete functions”. I
would suggest renaming it to Discrete_Functions in time for the
next release. Quite apart from the propensity for name clashes,
the current name is ambiguous.

Turning to HOLCF, many of the theories have short names that made
perfect sense in 1997, but no longer. Some of them have the
suffix _cpo, but unfortunately Discrete currently does not.

Larry

On 13 Nov 2024, at 10:03, Manuel Eberl <manuel@pruvisto.org> wrote:

Of course we should try to make sure that at least within the
HOL part of the Isabelle distribution, no duplicate theory names
occur. And in the future, in the AFP as well.

view this post on Zulip Email Gateway (Nov 17 2024 at 20:52):

From: Tobias Nipkow <nipkow@in.tum.de>

Thus both Discrete theories have been renamed now.

Tobias

PS There was no log2. I did not touch other variants elsewhere, like ceillog2.

On 15/11/2024 14:48, Manuel Eberl wrote:

I'd be fine with "floor_log2" as well, but then you should adjust "ceillog2" as
well.

I think I picked "ceillog2" because there is something similar (but more
general) called "floorlog" elsewhere in the library.

On 15/11/2024 14:32, Tobias Nipkow wrote:

On 15/11/2024 14:25, Manuel Eberl wrote:

As Makarius noted, the problem is that the functions defined in "HOL-
Library.Discrete" can (by design) only be used with their fully-qualified
names "Discrete.sqrt" and "Discrete.log".

Sorry, yes, I'll leave Library.Discrete alone.

I don't think we want "Discrete_Functions.log" since that's quite a mouthful.

Personally I'm not a huge fan of "Discrete.log" and "Discrete.sqrt" either.
Perhaps something like "floorlog2" and "floorsqrt"? (cf. my "ceillog2" that
Larry recently moved into the distribution).

floor_log2? (Personally, I belive in having the important name components
first but can see that floor_log2 is more natural).

Tobias

Alternatively "log2_nat" and "sqrt_nat" would also work, but then the
question arises what one should call the corresponding versions that round up
instead of down.

Manuel

On 15/11/2024 14:06, Tobias Nipkow wrote:

Good suggestions. Happy to take care of it later today.

Tobias

On 15/11/2024 13:32, Lawrence Paulson wrote:

Theory Library/Discrete is headed "Common discrete functions”. I would
suggest renaming it to Discrete_Functions in time for the next release.
Quite apart from the propensity for name clashes, the current name is
ambiguous.

Turning to HOLCF, many of the theories have short names that made perfect
sense in 1997, but no longer. Some of them have the suffix _cpo, but
unfortunately Discrete currently does not.

Larry

On 13 Nov 2024, at 10:03, Manuel Eberl <manuel@pruvisto.org> wrote:

Of course we should try to make sure that at least within the HOL part of
the Isabelle distribution, no duplicate theory names occur. And in the
future, in the AFP as well.

smime.p7s

view this post on Zulip Email Gateway (Nov 18 2024 at 14:34):

From: Paolo Crisafulli <paolo.crisafulli@irt-systemx.fr>
Thank you very much.

(For the record, Makarius' patch is enough to fix the issue locally, for
any user wanting to quickly import both HOLCF and HOL-Library.Discrete).

Paolo

On 15/11/2024 22:40, Tobias Nipkow wrote:

HOLCF.Discrete has been renamed to HOLCF.Discrete_Cpo.

Tobias

On 15/11/2024 14:06, Tobias Nipkow wrote:

Good suggestions. Happy to take care of it later today.

Tobias

On 15/11/2024 13:32, Lawrence Paulson wrote:

Theory Library/Discrete is headed "Common discrete functions”. I
would suggest renaming it to Discrete_Functions in time for the next
release. Quite apart from the propensity for name clashes, the
current name is ambiguous.

Turning to HOLCF, many of the theories have short names that made
perfect sense in 1997, but no longer. Some of them have the suffix
_cpo, but unfortunately Discrete currently does not.

Larry

On 13 Nov 2024, at 10:03, Manuel Eberl <manuel@pruvisto.org> wrote:

Of course we should try to make sure that at least within the HOL
part of the Isabelle distribution, no duplicate theory names occur.
And in the future, in the AFP as well.

view this post on Zulip Email Gateway (Nov 19 2024 at 13:17):

From: Paolo Crisafulli <paolo.crisafulli@irt-systemx.fr>
Thank you Manuel.

To sum up:

Is that correct?

Best,

Paolo

On 13/11/2024 15:59, Manuel Eberl wrote:

We don't import anything directly from both HOL-Library or HOLCF,
these are transitive dependencies of HOL-CSPM and
Ordinary_Differential_Equations.)
If none of them actually need HOL-Library.Discrete one could change
those entries to simply not import it.

Other than that, the best option would probably to rename
HOL-Library.Discrete. In the long run, that is the only sensible option
anyway.

Is there a practical solution to allow us to submit our theories to
AFP before that?
Once the issue has been taken care of in afp-devel you can submit your
entry to afp-devel (https://cas5-0-urlprotect.trendmicro.com:443/wis/clicktime/v1/query?url=https%3a%2f%2fdevel.isa%2dafp.org%2fsubmission%2f&umid=a4a9516f-bf37-440e-8da9-834154c471fb&auth=b6005005a7b50bc3a68b2003f1e38d069f93f262-e828e06bbdc7fff258c13967647d8aeeb6b4a4b2). It will
however only appear in the official release version of the AFP after the
next Isabelle release (some time in Q1 of 2025, if I recall correctly).

I don't think there is a sensible way to submit your entry to the
"regular" AFP before then.

Cheers,

Manuel

On 13/11/2024 15:45, Paolo Crisafulli wrote:

Thank you for your responses, but does this mean that we should wait
for the next Isabelle release, as both HOL-Library and HOLCSP are part
of it?

Is there a practical solution to allow us to submit our theories to
AFP before that?

(For the record, we can't apply this advice:

If your work does not depend on HOL-Library.Discrete then I would
recommend to simply import the bits of HOL-Library that you explicitly
need.

We don't import anything directly from both HOL-Library or HOLCF,
these are transitive dependencies of HOL-CSPM and
Ordinary_Differential_Equations.)

Thank you all in advance for your help.

Best,

Paolo

On 13/11/2024 12:57, Makarius wrote:

On 13/11/2024 09:46, Fabian Huch wrote:

You cannot have two theories with the same base name in an import path
unfortunately (a limitation coming from a time when theories were
considered
globally unique entities).
Note that theory names are still globally unique, although the name
is usually
qualified by the session name, so clashes don't occur in the session
context.

There is an additional restriction for theories that are formally
merged: base
names need to be unique, because thy are used for the standard name
space
policy. One happy day, when the name space policies are changed ---
after a
lot of hard work --- this restriction will disappear.

Currently, the only option (that I am aware of) is is to rename one
of the
theories.
Yes, indeed.

Dirty tricks should be avoided. The planet needs to be kept clean and
alive.

Although HOL-Library.Discrete could just as well be called something
else,
e.g. HOL-Librrary.Discrete_Funs, it is probably easier to clean-up
HOLCF a
little bit.

Here is historic evidence for the introduction of this theory in 1997:
https://cas5-0-urlprotect.trendmicro.com:443/wis/clicktime/v1/query?url=https%3a%2f%2fisabelle%2ddev.sketis.net%2frISABELLEc2508f4ab739&umid=070888fe-b1e4-40d4-8c4b-fc350f75d77e&auth=b6005005a7b50bc3a68b2003f1e38d069f93f262-8a9ce3d82ace24c3827208341f125e1ee2693d94

That is interesting on its own account: it shows how theory
construction had
to alternate between .thy files (for specifications) and .ML files (for
proofs) a few decades ago.

Today there is very little motivation of have these few
specifications and
proofs in the separate theory HOLCF.Discrete. The material could be
moved to
the start of its descendent HOLCF.Lift (and maybe separated by 'section'
headings).

Makarius


Last updated: Jan 04 2025 at 20:18 UTC