8000 fix: deprecation span should only cover the ident by digama0 · Pull Request #2459 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

fix: deprecation span should only cover the ident #2459

New issue 8000

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

digama0
Copy link
Collaborator
@digama0 digama0 commented Aug 25, 2023

Previously, if foo is deprecated then the entire simp [foo] cal 8000 l would be highlighted. This causes issues for a linter I am writing which requires that the warning just cover the identifier, as well as just being generally confusing for the user if there are many identifiers in the simp call.

simp is not the only affected tactic, many functions call resolveId? without setting the ref first. An alternative solution would be to have Linter.checkDeprecated take a syntax directly instead of using the ref, but there are also some other errors that identifier resolution can throw which are subject to the same issue.

@Kha
Copy link
Member
Kha commented Aug 25, 2023

LGTM but could you add a brief comment as to what the new test is testing?

@tydeu tydeu added the awaiting-author Waiting for PR author to address issues label Aug 25, 2023
@Kha Kha self-assigned this Sep 6, 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 review from leodemoura and Kha as code owners November 20, 2023 08:15
@github-actions github-actions bot added the stale label Dec 21, 2023
@github-actions github-actions bot removed the stale label Feb 10, 2024
@Kha Kha removed their assignment Feb 13, 2024
@github-actions github-actions bot added the stale label May 5, 2024
@github-actions github-actions bot removed the stale label May 30, 2024
@github-actions github-actions bot added stale and removed stale labels Jun 29, 2024
@github-actions github-actions bot added the stale label Aug 20, 2024
@github-actions github-actions bot removed the stale label Sep 6, 2024
@github-actions github-actions bot added the stale label Dec 23, 2024
@github-actions github-actions bot removed the stale label Jun 7, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author Waiting for PR author to address issues
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants
3070
0