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

PANIC at Lean.Lsp.CompletionItem.getFileSource! Lean.Server.CompletionItemData:34:22: no data param on completion item #5807

Open
nomeata opened this issue Oct 22, 2024 · 1 comment · May be fixed by #5835
Open

PANIC at Lean.Lsp.CompletionItem.getFileSource! Lean.Server.CompletionItemData:34:22: no data param on completion item #5807

nomeata opened this issue Oct 22, 2024 · 1 comment · May be fixed by #5835
Labels
bug Something isn't working P-medium We may work on this issue if we find the time

Comments

@nomeata
Copy link
Contributor

nomeata commented Oct 22, 2024 •
edited
Loading

On master I sometimes get

Lean server printed an error: PANIC at Lean.Lsp.CompletionItem.getFileSource! Lean.Server.CompletionItemData:34:22: no data param on completion item - backtrace:

I can reproduce it with a file like this:

import Doesnotexist

/-!
Press Ctrl-Space here:
-/

Backtrace:

/home/jojo/build/lean/lean4/src> lean --version
Lean (version 4.12.0, x86_64-unknown-linux-gnu, Release)
PANIC at Lean.Lsp.CompletionItem.getFileSource! Lean.Server.CompletionItemData:34:22: no data param on completion item -
backtrace:
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x6d) [0x7f6e156f6efd]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_12731____spec__7___lambda__1+0x2f) [0x7f6e1433139f]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(lean_apply_1+0x115) [0x7f6e15700f75]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(l_Lean_Server_routeLspRequest+0xd0) [0x7f6e1435e9d0]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(l_Lean_Server_Watchdog_forwardRequestToWorker+0x187) [0x7f6e11fb70d7]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(l_Lean_Server_Watchdog_mainLoop+0xd7e) [0x7f6e11fc120e]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(l_Lean_Server_Watchdog_initAndRunWatchdogAux+0x230) [0x7f6e11fc5c50]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(lean_server_watchdog_main+0x138) [0x7f6e11fd0048]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(+0x831b32) [0x7f6e11631b32]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(lean_main+0x29e5) [0x7f6e11634795]
/nix/store/ksk3rnb0ljx8gngzk19jlmbjyvac4hw6-glibc-2.38-44/lib/libc.so.6(+0x280ce) [0x7f6e10b5d0ce]
/nix/store/ksk3rnb0ljx8gngzk19jlmbjyvac4hw6-glibc-2.38-44/lib/libc.so.6(__libc_start_main+0x89) [0x7f6e10b5d189]
/home/jojo/.elan/toolchains/lean4-stage0/bin/lean(_start+0x25) [0x5569f7533075]
PANIC at Lean.Lsp.CompletionItem.getFileSource! Lean.Server.CompletionItemData:34:22: no data param on completion item -
backtrace:
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x6d) [0x7f6e156f6efd]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(l_Lean_Server_registerLspRequestHandler___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_12731____spec__7___lambda__1+0x2f) [0x7f6e1433139f]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(lean_apply_1+0x115) [0x7f6e15700f75]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(l_Lean_Server_routeLspRequest+0xd0) [0x7f6e1435e9d0]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(l_Lean_Server_Watchdog_forwardRequestToWorker+0x187) [0x7f6e11fb70d7]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(l_Lean_Server_Watchdog_mainLoop+0xd7e) [0x7f6e11fc120e]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(l_Lean_Server_Watchdog_initAndRunWatchdogAux+0x230) [0x7f6e11fc5c50]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(lean_server_watchdog_main+0x138) [0x7f6e11fd0048]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(+0x831b32) [0x7f6e11631b32]
/home/jojo/build/lean/lean4/build/release/stage0/bin/../lib/lean/libleanshared.so(lean_main+0x29e5) [0x7f6e11634795]
/nix/store/ksk3rnb0ljx8gngzk19jlmbjyvac4hw6-glibc-2.38-44/lib/libc.so.6(+0x280ce) [0x7f6e10b5d0ce]
/nix/store/ksk3rnb0ljx8gngzk19jlmbjyvac4hw6-glibc-2.38-44/lib/libc.so.6(__libc_start_main+0x89) [0x7f6e10b5d189]
/home/jojo/.elan/toolchains/lean4-stage0/bin/lean(_start+0x25) [0x5569f7533075]
Setup information

Operating system: Linux (release: 6.9.7)
CPU architecture: x64
CPU model: 8 x 11th Gen Intel(R) Core(TM) i7-1185G7 @ 3.00GHz
Available RAM: 16.46 GB

VS Code version: Reasonably up-to-date (version: 1.93.0)
Lean 4 extension version: 0.0.183
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.12.0)
Project: Valid Lean project (path: /home/jojo/build/lean/lean4/src)

Elan toolchains:

installed toolchains
--------------------

nightly
lean4
lean4-stage0
leanprover/lean4-pr-releases:pr-release-3160
leanprover/lean4-pr-releases:pr-release-3714.tmp
leanprover/lean4-pr-releases:pr-release-3718
leanprover/lean4-pr-releases:pr-release-3772
leanprover/lean4-pr-releases:pr-release-4149
leanprover/lean4-pr-releases:pr-release-4154
leanprover/lean4-pr-releases:pr-release-5182
leanprover/lean4-pr-releases:pr-release-5479
leanprover/lean4-pr-releases:pr-release-5563
leanprover/lean4-pr-releases:pr-release-5686
leanprover/lean4:4.6.0
leanprover/lean4:4.7.0
leanprover/lean4:4.8.0
leanprover/lean4:nightly-2024-01-13
leanprover/lean4:nightly-2024-02-13
leanprover/lean4:nightly-2024-08-20
leanprover/lean4:nightly-2024-08-21
leanprover/lean4:nightly-2024-08-25
leanprover/lean4:nightly-2024-08-26
leanprover/lean4:nightly-2024-09-02
leanprover/lean4:nightly-2024-09-09
leanprover/lean4:nightly-2024-09-16
leanprover/lean4:nightly-2024-09-17
leanprover/lean4:nightly-2024-09-19
leanprover/lean4:nightly-2024-10-07
leanprover/lean4:stable
leanprover/lean4:v4.10.0-rc1
leanprover/lean4:v4.10.0-rc2
leanprover/lean4:v4.11.0
leanprover/lean4:v4.11.0-rc1
leanprover/lean4:v4.11.0-rc2
leanprover/lean4:v4.12.0
leanprover/lean4:v4.12.0-rc1
leanprover/lean4:v4.13.0-rc3

leanprover/lean4:v4.5.0
leanprover/lean4:v4.6.0-rc1
leanprover/lean4:v4.7.0
leanprover/lean4:v4.7.0-rc1
leanprover/lean4:v4.7.0-rc2
leanprover/lean4:v4.8.0
leanprover/lean4:v4.8.0-rc1
leanprover/lean4:v4.9.0-rc1
leanprover/lean4:v4.9.0-rc2
leanprover/lean4:v4.9.0-rc3

active toolchain
----------------

lean4-stage0 (overridden by '/home/jojo/build/lean/lean4/src/lean-toolchain')

Lean (version 4.12.0, x86_64-unknown-linux-gnu, Release)

Doesn't seem to be happening on live.lean-lang.org though.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
@nomeata nomeata added the bug Something isn't working label Oct 22, 2024
@mhuisi
Copy link
Contributor

mhuisi commented Oct 23, 2024

(I've noticed this as well and it's already fixed on a local branch with other completion work, to be merged next release cycle)

@mhuisi mhuisi linked a pull request Oct 25, 2024 that will close this issue
Open
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Oct 25, 2024
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 P-medium We may work on this issue if we find the time
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

feat: structure auto-completion & partial InfoTrees mhuisi/lean4
3 participants
@nomeata @mhuisi @leanprover-bot