Go to definition for `namespace` and `open` commands jumps to either nowhere or to the command definition

Prerequisites

• Check that your issue is not already filed:
• Reduce the issue to a minimal, self-contained, reproducible test case.
• Test your test case against the latest nightly release, for example on

Description

The LSP "go to definition" does not properly go to definition for the namespace or open commands, and instead either will go nowhere or will jump to the definition of the namespace command itself.

(Whether this is a bug or an enhancement seems slightly subjective, so certainly no issue if it's classified as the latter)

Context

Mentioned here with minimal additional context.

Steps to Reproduce

Given a file containing:

-- import Lean
namespace Nat
end Nat

trying to jump to definition on Nat will either:

• go nowhere if the import line is left commented out
• jump to Lean/Elab/BuiltinCommand.lean if you uncomment the import (n.b. Mathlib has this import in its prelude, so essentially all Mathlib users see this half of the behavior more or less always)

The same behavior happens for open Nat.

Expected behavior: It would seem to me more expected that this should instaed be jumping to the definition of Nat (or whatever declaration is resolved by the namespace, if any) with or without the import.

Versions

[Output of #eval Lean.versionString]: "4.12.0, commit "
[OS version, if not using live.lean-lang.org.]: macOS 14.6.1

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the namespace and open examples in the issue, with and without the commented import, and inspect the go-to-definition behavior that currently reaches Lean/Elab/BuiltinCommand.lean. Done means both commands resolve the referenced namespace or declaration, including the no-import case described in the report.