Calling lean4-toggle-info causing lsp--send-request-async: The connected server(s) does not support method $/lean/plainGoal.

[Yuhta]

Lean (version 4.4.0, commit ca7d6dadb9e1, Release)
lean4-mode commit: d1c9364
GNU Emacs 28.1 (build 1, x86_64-pc-linux-gnu, GTK+ Version 3.24.20, cairo version 1.16.0) of 2022-05-31

Debugger entered--Lisp error: (error "The connected server(s) does not support method $/...")
  signal(error ("The connected server(s) does not support method $/..."))
  error("The connected server(s) does not support method %s..." "$/lean/plainGoal")
  lsp--send-request-async((:jsonrpc "2.0" :method "$/lean/plainGoal" :params (:textDocument (:uri "file:///home/yuhta/tmp/test.lean") :position (:line 0 :character 9))) (closure (lean4-info-mode-abbrev-table t) (input0) (let* ((_ input0) (goals (if (ht\? _) (progn (gethash "goals" _))))) (setq lean4-goals goals) (lean4-info-buffer-redisplay-debounced))) tick ignore nil nil :plain-goal)
  lsp-request-async("$/lean/plainGoal" (:textDocument (:uri "file:///home/yuhta/tmp/test.lean") :position (:line 0 :character 9)) (closure (lean4-info-mode-abbrev-table t) (input0) (let* ((_ input0) (goals (if (ht\? _) (progn (gethash "goals" _))))) (setq lean4-goals goals) (lean4-info-buffer-redisplay-debounced))) :error-handler ignore :mode tick :cancel-token :plain-goal)
  (progn (lsp-request-async "$/lean/plainGoal" (lsp--text-document-position-params) #'(lambda (input0) (let* ((_ input0) (goals (if ... ...))) (setq lean4-goals goals) (lean4-info-buffer-redisplay-debounced))) :error-handler #'ignore :mode 'tick :cancel-token :plain-goal) (lsp-request-async "$/lean/plainTermGoal" (lsp--text-document-position-params) #'(lambda (input0) (let* ((_ input0) (goal (if ... ...))) (setq lean4-term-goal goal) (lean4-info-buffer-redisplay-debounced))) :error-handler #'ignore :mode 'tick :cancel-token :plain-term-goal))
  (if (lean4-info-buffer-active lean4-info-buffer-name) (progn (lsp-request-async "$/lean/plainGoal" (lsp--text-document-position-params) #'(lambda (input0) (let* ((_ input0) (goals ...)) (setq lean4-goals goals) (lean4-info-buffer-redisplay-debounced))) :error-handler #'ignore :mode 'tick :cancel-token :plain-goal) (lsp-request-async "$/lean/plainTermGoal" (lsp--text-document-position-params) #'(lambda (input0) (let* ((_ input0) (goal ...)) (setq lean4-term-goal goal) (lean4-info-buffer-redisplay-debounced))) :error-handler #'ignore :mode 'tick :cancel-token :plain-term-goal)))
  lean4-info-buffer-refresh()
  lean4-toggle-info()
  funcall-interactively(lean4-toggle-info)
  call-interactively(lean4-toggle-info nil nil)
  command-execute(lean4-toggle-info)

[Yuhta]

Does it work only inside a project directory? I was trying to run it on a single file. It works inside project.

[quinn-dougherty]

Same.

Debugger entered--Lisp error: (error "The connected server(s) does not support method $/...")
  error("The connected server(s) does not support method %s..." "$/lean/plainGoal")
  lsp--send-request-async((:jsonrpc "2.0" :method "$/lean/plainGoal" :params (:textDocument (:uri "file:///home/qd/Projects/casper/mtl-actus/src/Actu...") :position (:line 72 :character 33))) #<subr F616e6f6e796d6f75732d6c616d626461_anonymous_lambda_72> tick ignore nil nil :plain-goal)
  lsp-request-async("$/lean/plainGoal" (:textDocument (:uri "file:///home/qd/Projects/casper/mtl-actus/src/Actu...") :position (:line 72 :character 33)) #<subr F616e6f6e796d6f75732d6c616d626461_anonymous_lambda_72> :error-handler ignore :mode tick :cancel-token :plain-goal)
  lean4-info-buffer-refresh()
  lean4-toggle-info()
  funcall-interactively(lean4-toggle-info)
  command-execute(lean4-toggle-info)

Emacs: 29.4
lean4-mode: da7b63d

[mekeor]

Can anyone provide a minimal reproducing example?

[AtticusKuhn]

I also encountered this same error.
Here's what I did:

1. Ran lake new lean_test math
2. Opened the file Basic.lean in Emacs
3. Tried the command lean4-toggle-info
4. Got this error.

Here is the error I got

Debugger entered--Lisp error: (error "The connected server(s) does not support method $/...")
  error("The connected server(s) does not support method %s..." "$/lean/plainGoal")
  lsp--send-request-async((:jsonrpc "2.0" :method "$/lean/plainGoal" :params (:textDocument (:uri "file:///home/atticusk/coding/lean_test/LeanTest/Ba...") :position (:line 0 :character 0))) #<subr F616e6f6e796d6f75732d6c616d626461_anonymous_lambda_72> tick ignore nil nil :plain-goal)
  lsp-request-async("$/lean/plainGoal" (:textDocument (:uri "file:///home/atticusk/coding/lean_test/LeanTest/Ba...") :position (:line 0 :character 0)) #<subr F616e6f6e796d6f75732d6c616d626461_anonymous_lambda_72> :error-handler ignore :mode tick :cancel-token :plain-goal)
  lean4-info-buffer-refresh()
  lean4-toggle-info()
  funcall-interactively(lean4-toggle-info)
  command-execute(lean4-toggle-info)

Can anyone provide a minimal reproducing example?

For me, the minimal reproducing example is just a basic project which you get from lake new $project_name math

Emacs version: GNU Emacs 29.4 (build 1, x86_64-pc-linux-gnu, X toolkit, cairo version 1.18.0, Xaw3d scroll bars)
Elan version: elan 3.1.1

By the way, if it helps, here is the *lsp-log*

Command "/etc/profiles/per-user/atticusk/bin/lake serve" is present on the path.
Command "/etc/profiles/per-user/atticusk/bin/lake serve" is present on the path.
Found the following clients for /home/atticusk/coding/lean_test/LeanTest/Basic.lean: (server-id lean4-lsp, priority 0)
The following clients were selected based on priority: (server-id lean4-lsp, priority 0)

[AtticusKuhn]

relevant: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20The.20connected.20server.28s.29.20does.20not.20support.20method.20.24.2Flean.2F.2E.2E.2E

Maybe this issue is related to Doom Emacs?