Lean.Nat

Stream: lean4

[Damiano Testa]

I was a little surprised by the following:

import Lean.Expr

-- you can also open `Nat` here or repeat a namespace for more ambiguities
open Lean Int

/-- error: ambiguous namespace 'Nat', possible interpretations: '[Nat, Int.Nat, Lean.Nat]' -/
#guard_msgs in
open Nat hiding add_comm

/-- error: unknown identifier 'Lean.Nat' -/
#guard_msgs in
#check Lean.Nat

[Edward van de Meent]

it seems this doesn't reproduce as-is on live? i forgot how #guard_msgs works

[Aaron Liu]

import Lean.Expr

-- you can also open `Nat` here or repeat a namespace for more ambiguities
open Lean Int

/-- error: ambiguous namespace 'Nat', possible interpretations: '[Nat, Int.Nat, Lean.Nat]' -/
#guard_msgs in
open Nat hiding add_comm

/-- error: unknown identifier 'Lean.Nat' -/
#guard_msgs in
#check Lean.Nat

#check Lean.Nat.mkInstAdd
#check Lean.Nat.mkInstDiv
#check Lean.Nat.mkInstHAdd
#check Lean.Nat.mkInstHDiv
#check Lean.Nat.mkInstHMod
#check Lean.Nat.mkInstHMul
#check Lean.Nat.mkInstHPow
#check Lean.Nat.mkInstHSub
#check Lean.Nat.mkInstLE
#check Lean.Nat.mkInstLT
#check Lean.Nat.mkInstMod
#check Lean.Nat.mkInstMul
#check Lean.Nat.mkInstNatPow
#check Lean.Nat.mkInstPow
#check Lean.Nat.mkInstSub
#check Lean.Nat.mkType

[Aaron Liu]

There are lots of Lean.Nat.* stuff, even though Lean.Nat doesn't exist.

[Damiano Testa]

Edward van de Meent said:

it seems this doesn't reproduce as-is on live?

It does reproduce for me both locally and on the server.

[Edward van de Meent]

right, i had a big brainfart

[Damiano Testa]

Indeed, the Lean.Nat stuff is defined in the "minimised" import above. I still am a little surprised that there is some ambiguity.

[Edward van de Meent]

it's funny if this is how we get unambiguous opens

[Damiano Testa]

If you open Nat, you also get a Nat.Nat ambiguity.

[Edward van de Meent]

how do you mean?

[Damiano Testa]

import Lean.Expr

-- you can also open `Nat` here or repeat a namespace for more ambiguities
open Lean Nat

/-- error: ambiguous namespace 'Nat', possible interpretations: '[Nat, Nat.Nat, Lean.Nat]' -/
#guard_msgs in
open Nat hiding add_comm

[Edward van de Meent]

ah right

[Aaron Liu]

This is docs#Nat.Nat.zero_eq_one_mod_iff, probably a mistake?

[Damiano Testa]

Oh, it looks like core does not have a duplicatedNamespace linter!

[Aaron Liu]

Int.Nat.* seems to just be docs#Int.Nat.cast_ofNat_Int, also a mistake?

[Damiano Testa]

These are some more repeated namespaces:

import Mathlib

open Lean

/--
info: 9 repeated namespaces in 48 declarations:

* 'Array' is repeated in the declaration
[Array.Array.data]

* 'Backtrack' is repeated in the 3 declarations
[Meta.Tactic.Backtrack.Backtrack.tryAllM,
 Meta.Tactic.Backtrack.Backtrack.tryAllM.match_1,
 Meta.Tactic.Backtrack.Backtrack.tryAllM.match_2]

* 'Element' is repeated in the 4 declarations
[Xml.Element.Element, Xml.Element.Element.inj, Xml.Element.Element.injEq, Xml.Element.Element.sizeOf_spec]

* 'Loop' is repeated in the 12 declarations
[Std.Internal.UV.Loop.Loop.Options,
 Std.Internal.UV.Loop.Loop.Options.accumulateIdleTime,
 Std.Internal.UV.Loop.Loop.Options.blockSigProfSignal,
 Std.Internal.UV.Loop.Loop.Options.casesOn,
 Std.Internal.UV.Loop.Loop.Options.mk,
 Std.Internal.UV.Loop.Loop.Options.mk.inj,
 Std.Internal.UV.Loop.Loop.Options.mk.injEq,
 Std.Internal.UV.Loop.Loop.Options.mk.sizeOf_spec,
 Std.Internal.UV.Loop.Loop.Options.noConfusion,
 Std.Internal.UV.Loop.Loop.Options.noConfusionType,
 Std.Internal.UV.Loop.Loop.Options.rec,
 Std.Internal.UV.Loop.Loop.Options.recOn]

* 'Nat' is repeated in the declaration
[Nat.Nat.zero_eq_one_mod_iff]

* 'Parser' is repeated in the 12 declarations
[Parser.Parser,
 Parser.Parser.casesOn,
 Parser.Parser.fn,
 Parser.Parser.info,
 Parser.Parser.mk,
 Parser.Parser.mk.inj,
 Parser.Parser.mk.injEq,
 Parser.Parser.mk.sizeOf_spec,
 Parser.Parser.noConfusion,
 Parser.Parser.noConfusionType,
 Parser.Parser.rec,
 Parser.Parser.recOn]

* 'TZif' is repeated in the 12 declarations
[Std.Time.TimeZone.TZif.TZif,
 Std.Time.TimeZone.TZif.TZif.casesOn,
 Std.Time.TimeZone.TZif.TZif.mk,
 Std.Time.TimeZone.TZif.TZif.mk.inj,
 Std.Time.TimeZone.TZif.TZif.mk.injEq,
 Std.Time.TimeZone.TZif.TZif.mk.sizeOf_spec,
 Std.Time.TimeZone.TZif.TZif.noConfusion,
 Std.Time.TimeZone.TZif.TZif.noConfusionType,
 Std.Time.TimeZone.TZif.TZif.rec,
 Std.Time.TimeZone.TZif.TZif.recOn,
 Std.Time.TimeZone.TZif.TZif.v1,
 Std.Time.TimeZone.TZif.TZif.v2]

* 'Tactic' is repeated in the declaration
[Elab.Tactic.Tactic]

* 'toACExpr' is repeated in the 2 declarations [Meta.AC.toACExpr.toACExpr, Meta.AC.toACExpr.toACExpr.match_1]
---
warning: unused variable `declsSorted`
note: this linter can be disabled with `set_option linter.unusedVariables false`
-/
#guard_msgs in
run_cmd
  let mut repHash : Std.HashMap Name Name := ∅
  for (c, _) in (← getEnv).constants do
    if ! c.isInternal then
      let parts := c.components.zip (c.components.drop 1)
      if let some rep := parts.find? fun (a, b) => a == b then
        repHash := repHash.insert c rep.1
  let gped := repHash.keysArray.groupByKey (repHash[·]!)
  let gpdedSorted := gped.toArray.qsort (·.1.toString < ·.1.toString)
  let mut msg := []
  for (rep, decls) in gpdedSorted do
    let declsSorted := decls.qsort (·.toString < ·.toString)
    let declsSorted : Array MessageData := decls.qsort (·.toString < ·.toString) |>.map (.ofConstName)
    let declStr := if decls.size == 1 then "declaration" else s!"{decls.size} declarations"
    msg := msg ++ [m!"* '{rep}' is repeated in the {declStr}\n{.ofArray declsSorted}"]
  logInfo <| .joinSep (s!"{gped.size} repeated namespaces in {repHash.size} declarations:" :: msg) "\n\n"

[Damiano Testa]

Aaron Liu said:

This is docs#Nat.Nat.zero_eq_one_mod_iff, probably a mistake?

Should docs#Nat.Nat.zero_eq_one_mod_iff be renamed to Nat.zero_eq_one_mod_iff?

[Damiano Testa]

I also wonder whether Array.Array.data which is deprecated, should actually be deprecating Array.data.
EDIT: maybe not, since there is also a deprecated Array.data.

[Kim Morrison]

The issues reported here have finally been fixed in lean#7448. Apologies for the delay!