Constant is in `e.constants` but is not accessible by name

Stream: lean4

[Eric Wieser]

This seems to be a behavior change in 4.19.0:

import Lean.Elab.Command

def foo : Nat := .zero

run_cmd do
  let e ← Lean.getEnv
  for (n, c) in e.constants.map₂ do
    Lean.logInfo m!"{n} : {c.type}"

#print foo._cstage2

Previously in v4.18.0, the #print would succeed, but in the latest rc it fails

[Eric Wieser]

Relatedly, the logInfo above results in an _obj in the infoview which produces Error: Rpc error: InternalError: unknown constant '_obj' when hovered over.

[Aaron Liu]

You can even redeclare it

import Lean.Elab.Command

def foo : Nat := .zero

run_cmd do
  let e ← Lean.getEnv
  for (n, c) in e.constants.map₂ do
    Lean.logInfo n
    Lean.logInfo m!"{n} : {c.type}"

def foo._cstage2 : Nat := .succ .zero

#print foo._cstage2

[Aaron Liu]

You get a kernel error but the #print succeeds with the new definition

[Aaron Liu]

This is in contrast to what happens if you try to redeclare a regular definition, in that case the #print will print the original definition, but here it prints the new one.

[Sebastian Ullrich]

Yes, this is a temporary regression until the old code generator is removed. If any metaprograms are broken by this, I would suggest ignoring constants from map_2 that are not in Environment.find?

[Eric Wieser]

Is the nonexistent _obj also going away?

[Sebastian Ullrich]

I don't know but that has always been the case when pretty-printing IR