fix: resolve _root_ in macro, syntax, elab

[digama0]

This is not just a convenience feature: Because _root_ is resolved in def, if we do not also resolve it in macro there will be a mismatch between the syntax kind used for the definition and the one used for the parenthesizer / formatter. This comes up in practice for register_simp_attr, which is defined like:

namespace Lean.Meta
...

macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc:(docComment)?
  "register_simp_attr" id:ident : command => ...

leading to a parser that puts the syntax kind Lean.Meta._root_.Lean.Parser.Command.registerSimpAttr on generated nodes, and a parenthesizer that is expecting to find syntax kind Lean.Parser.Command.registerSimpAttr.

[Kha]

An alternative solution would be to change Name.append to discard the first parameter if the second one is absolute (just like FilePath.join). I don't know if we want to make Name itself that "intelligent", but we already do almost the same thing in there for macro scopes after all!

[digama0]

Not so sure about using Name.append, but there should definitely be a name function to do this rather than reinventing it all over the place.

[digama0]

Ping on this one, it is the cause of a bug in mathport. How should I address the issue about name joining?

[Kha]

there should definitely be a name function to do this rather than reinventing it all over the place.

Do you want to add such a function (possibly #2341)? Then I think this is good to go. Actually, why do we need the stage 0 update?

[digama0]

@Kha Should this PR wait on #2341? I'm fine with landing that and updating this to use it.

[leanprover-community-mathlib4-bot]

• 🟡 Mathlib branch lean-pr-testing-2239 build this PR didn't complete normally. (2023-09-14 04:30:25) View Log

[digama0]

@Kha perhaps the difference between the two CI runs answers your question about why the update-stage0 is needed.

[Kha]

I see, it's a stage 2 failure. That makes sense in this case as we build it under prefer_native=true in contrast to stage 1.

[Kha]

@Kha Should this PR wait on #2341? I'm fine with landing that and updating this to use it.

Could you cherry-pick it into this PR (and adjust if desired)? I would prefer it to be part of a PR with clear impact