panic when adding declaration existing in private scope

Stream: lean4

[Floris van Doorn]

addDecl panics when I add a declaration whose name is already used in private scope. I expect this is undesired behavior.

Related question: how can I check whether I can safely add a declaration with name foo to the environment? Environment.contains foo doesn't help here.

module
import Lean

open Lean Environment

def foo := 1

-- in live.lean-lang
/--
info: PANIC at _private.Lean.Environment.0.Lean.AsyncConsts.add Lean.Environment:478:4: duplicate normalized declaration name foo vs. _private.«external:file:///MathlibDemo/MathlibDemo.lean».0.foo
backtrace:
---
info: PANIC at _private.Lean.Environment.0.Lean.AsyncConsts.add Lean.Environment:478:4: duplicate normalized declaration name foo vs. _private.«external:file:///MathlibDemo/MathlibDemo.lean».0.foo
backtrace:
-/
#guard_msgs in
run_meta do
  addDecl <| .thmDecl { name := `foo, levelParams := [], type := mkConst `True, value := mkConst `trivial }

/-- info: false -/
#guard_msgs in
run_meta do
  logInfo m!"{(← getEnv).contains `foo}"

(cc @Sebastian Ullrich)

[Sebastian Ullrich]

Floris van Doorn said:

I expect this is undesired behavior.

No, as without metaprogramming there is and has (always?) been the same restriction.

Floris van Doorn said:

how can I check whether I can safely add a declaration with name foo to the environment?

I think we have various elaborators that try contains with and without mkPrivateName. You may need to wrap this test in withoutExporting to make sure you have access to the private scope if you're not already in it.

[Floris van Doorn]

Ok, so metaprograms that call addDecl have to make sure to check whether the name exists themselves, before trying to run addDecl. That's good to know.