search

leanprover-community / lean4-mode

Emacs major mode for Lean 4
https://leanprover.github.io/
Apache License 2.0
55 stars 27 forks source link

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

Open Yuhta opened 6 months ago

Yuhta commented 6 months ago

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 commented 6 months ago

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