Skip to content

fix: resolve _root_ in macro, syntax, elab#2239

Open
digama0 wants to merge 2 commits intoleanprover:masterfrom
digama0:macro_root
Open

fix: resolve _root_ in macro, syntax, elab#2239
digama0 wants to merge 2 commits intoleanprover:masterfrom
digama0:macro_root

Conversation

@digama0
Copy link
Copy Markdown
Collaborator

@digama0 digama0 commented May 28, 2023

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.

@digama0 digama0 added the needs-update-stage0 stage 0 should be updated after merging this PR label May 28, 2023
@Kha
Copy link
Copy Markdown
Member

Kha commented Jun 5, 2023

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
Copy link
Copy Markdown
Collaborator Author

digama0 commented Jun 5, 2023 •
edited
Loading

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
Copy link
Copy Markdown
Collaborator Author

digama0 commented Jun 8, 2023

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

@digama0 digama0 mentioned this pull request Jul 21, 2023
Closed
@leodemoura leodemoura requested a review from Kha August 9, 2023 16:21
@leodemoura leodemoura added the awaiting-review Waiting for someone to review the PR label Aug 9, 2023
@Kha
Copy link
Copy Markdown
Member

Kha commented Sep 13, 2023

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?

@Kha Kha added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Sep 13, 2023
@Kha Kha self-assigned this Sep 13, 2023
@digama0
Copy link
Copy Markdown
Collaborator Author

digama0 commented Sep 13, 2023

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

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 14, 2023
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Sep 14, 2023
Update lean-toolchain for testing leanprover/lean4#2239
89d44a3
@ghost
Copy link
Copy Markdown

ghost commented Sep 14, 2023

@digama0
Copy link
Copy Markdown
Collaborator Author

digama0 commented Sep 14, 2023

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

@digama0 digama0 added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Sep 14, 2023
@Kha
Copy link
Copy Markdown
Member

Kha commented Sep 18, 2023

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
Copy link
Copy Markdown
Member

Kha commented Sep 18, 2023

@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

@Kha Kha added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Sep 19, 2023
@github-actions github-actions bot added the stale label Oct 20, 2023
@github-actions github-actions bot removed the stale label Nov 2, 2023
@Kha Kha requested a review from leodemoura as a code owner November 20, 2023 08:15
@github-actions github-actions bot added the stale label Dec 22, 2023
@github-actions github-actions bot removed the stale label Feb 11, 2024
@Kha Kha removed their assignment Feb 13, 2024
@github-actions github-actions bot added the stale label May 7, 2024
@github-actions github-actions bot removed the stale label May 31, 2024
@github-actions github-actions bot added stale and removed stale labels Jul 2, 2024
@github-actions github-actions bot added the stale label Nov 4, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Kha Kha Awaiting requested review from Kha

@leodemoura leodemoura Awaiting requested review from leodemoura

Assignees

No one assigned

Labels

awaiting-author Waiting for PR author to address issues needs-update-stage0 stage 0 should be updated after merging this PR stale toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@digama0 @Kha @leodemoura