Confusing delaboration in doc-gen

Stream: lean4

[Henrik Böving]

Hi, as you might have noticed doc-gen has been misprinting a few type names recently, for example docs#Lean.Name is mysteriously printed as Lake.Name. I injected some tracing code into doc-gen that checks whether it is currently documenting the Lean.Name declaration and if it prints will print the delaborated expressions (coming from this function https://github.com/leanprover/doc-gen4/blob/dc9549e2e6bd553cfbb55a10de38be24753ac3c8/DocGen4/Process/Base.lean#L179) to check whether I am messing up myself or just getting weird info. Printing the CodeWithInfos from the type of the anonymous constructor already gives me:

Lean.Widget.TaggedText.tag ... (Lean.Widget.TaggedText.text "Lake.Name")

so it appears it is already Lean who is giving me a wrong namespace here??? Does anyone have a clue how this could happen? The part of doc-gen that sets up the Environment which gets analyzed here is: https://github.com/leanprover/doc-gen4/blob/dc9549e2e6bd553cfbb55a10de38be24753ac3c8/DocGen4/Load.lean#L40-L59

CC: @Mac Malone

[Mario Carneiro]

what environment is this? Can you replicate in lean normally?

[Mario Carneiro]

can you make a doc-gen free MWE?

[Henrik Böving]

I'll try but that will probably take a bit, was just hoping someone here might have an idea instantly.

[Mario Carneiro]

import Lean
import Lake

#eval show Lean.MetaM _ from do
  let ⟨fmt, _⟩ ← Lean.PrettyPrinter.ppExprWithInfos (Lean.mkConst ``Lean.Name)
  println! fmt

[Henrik Böving]

Oh, didn't expect it to be that easy :D

[Henrik Böving]

off topic: is println! new?

[Mario Carneiro]

nope

[Mario Carneiro]

import Lean
import Lake

open Lean
#eval show MetaM _ from do
  unresolveNameGlobal ``Name

[Mario Carneiro]

(By the way, the reason Lake.Name is even showing up is most likely because Lake re-exports Name)

[Mario Carneiro]

It seems the issue is that re-exports are preferred over the original name in unresolveNameGlobal, even if you are not in the scope of the re-export

[Henrik Böving]

@Mario Carneiro are you planning on tackling this or should I open an issue about it and investigate myself?

[Mario Carneiro]

@Henrik Böving Have at it. I'm not sure yet what the desired algorithm is

[Henrik Böving]

https://github.com/leanprover/lean4/issues/2524

[Mac Malone]

@Henrik Böving Note that if you pass fullNames := true you get the right answer:

#eval show MetaM _ from do -- # `Lean.Name
  unresolveNameGlobal ``Name true

[Mac Malone]

I think the problem may be that the non-fullNames algorithm of unresolveGlobalName tries candidates in reverse?