Skip to content
New issue

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

Sign up for GitHub

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

Jump to bottom

Unknown constant 'Lean.Elab.Term.elabNumLit' on Go to Definition #3789

Closed
mhuisi opened this issue Mar 27, 2024 · 2 comments · Fixed by #4780
Closed

Unknown constant 'Lean.Elab.Term.elabNumLit' on Go to Definition #3789

mhuisi opened this issue Mar 27, 2024 · 2 comments · Fixed by #4780
Labels
bug Something isn't working

Comments

@mhuisi
Copy link
Contributor

mhuisi commented Mar 27, 2024

Description

Use the following MWE and trigger Go to Definition at <cursor>:

#eval <cursor>1

This yields an error:

[Error - 11:37:43 AM] Request textDocument/definition failed.
  Message: unknown constant 'Lean.Elab.Term.elabNumLit'
  Code: -32603

I would not expect an error here.

Versions

Current nightly.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
@mhuisi mhuisi added the bug Something isn't working label Mar 27, 2024
@kim-em
Copy link
Collaborator

kim-em commented Apr 22, 2024

On leanprover/lean4:nightly-2024-04-21, I'm just getting a pop-up "No definition found for '1'". Can anyone else reproduce?

@mhuisi
Copy link
Contributor Author

mhuisi commented Apr 22, 2024

On leanprover/lean4:nightly-2024-04-21, I'm just getting a pop-up "No definition found for '1'". Can anyone else reproduce?

You get the popup, but you also get a server error under Output > Lean: Editor.

kmill added a commit to kmill/lean4 that referenced this issue Jul 18, 2024
@kmill
fix: handle unimported builtin names for location links
62e795c 
The function `locationLinksFromDecl` could throw an error if the name it is provided doesn't exist in the environment, which is possible if for example an elaborator is a builtin.

Closes leanprover#3789
@kmill kmill mentioned this issue Jul 18, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Jul 27, 2024
@kmill
fix: handle unimported builtin names for location links (#4780)
30c78a4 
The function `locationLinksFromDecl` could throw an error if the name it
is provided doesn't exist in the environment, which is possible if for
example an elaborator is a builtin.

Closes #3789
github-merge-queue bot pushed a commit that referenced this issue Jul 27, 2024
@kmill
fix: handle unimported builtin names for location links (#4780)
906bc58 
The function `locationLinksFromDecl` could throw an error if the name it
is provided doesn't exist in the environment, which is possible if for
example an elaborator is a builtin.

Closes #3789
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: handle unimported builtin names for location links kmill/lean4
2 participants
@kim-em @mhuisi