Zulip Chat Archive

Stream: lean4

Topic: lean4-mode: "Error processing message: wrong type argument"


Jannis Limperg (Jun 18 2021 at 12:14):

I've recently been getting a lot of these error messages whenever I'm using lean4-mode with Spacemacs:

Error processing message (wrong-type-argument listp #s(hash-table size 65 test equal rehash-size 1.5 rehash-threshold 0.8125 data ("textDocument" #s(hash-table size 65 test equal rehash-size 1.5 rehash-threshold 0.8125 data ("version" 0 "uri" "file:///home/jannis/uni/lean4/aesop/src/Lean/Environment.lean")) "processing" []))).

They don't seem to break anything, but they sure are annoying. My lean4-mode is the most recent one from the lean4 repo (b3535e4e3e97fb6a38a9942e1b56000f8e9c1e3d). lsp-version reports lsp-mode 20210613.1645, Emacs 27.2, gnu/linux. Any advice?

Sebastian Ullrich (Jun 18 2021 at 12:26):

Could you give me a stacktrace?

Jannis Limperg (Jun 18 2021 at 12:45):

Like this? Sorry, my elisp-fu is nonexistent.

Debugger entered--Lisp error: (wrong-type-argument listp #<hash-table equal 2/65 0x156c8bd3fed9>)
  lean4-fringe-update(#s(lsp--workspace :ewoc nil :server-capabilities #<hash-table equal 9/65 0x156c89209651> :registered-server-capabilities nil :root "/home/jannis/uni/aesop" :client #s(lsp--client :language-id nil :add-on? nil :new-connection (:connect #f(compiled-function (filter sentinel name environment-fn) #<bytecode 0x156c880d8e8d>) :test\? #f(compiled-function () #<bytecode 0x156c880d8ea5>)) :ignore-regexps nil :ignore-messages nil :notification-handlers #<hash-table equal 1/65 0x156c880d8eb1> :request-handlers #<hash-table equal 0/65 0x156c8816ff3d> :response-handlers #<hash-table eql 4/65 0x156c880d8ed1> :prefix-function nil :uri-handlers #<hash-table equal 0/65 0x156c880d8ef1> :action-handlers #<hash-table equal 0/65 0x156c880d8f11> :major-modes (lean4-mode) :activation-fn nil :priority 0 :server-id lean4-lsp :multi-root nil :initialization-options nil :semantic-tokens-faces-overrides nil :custom-capabilities nil :library-folders-fn nil :before-file-open-fn nil :initialized-fn nil :remote? nil :completion-in-comments? nil :path->uri-fn nil :uri->path-fn nil :environment-fn nil :after-open-fn nil :async-request-handlers #<hash-table equal 0/65 0x156c88468d99> :download-server-fn nil :download-in-progress? nil :buffers nil) :host-root nil :proc #<process lean4-lsp> :cmd-proc #<process lean4-lsp> :buffers (#<buffer MutAltTree.lean> #<buffer Percent.lean>) :semantic-tokens-faces [lsp-face-semhl-keyword lsp-face-semhl-variable lsp-face-semhl-property] :semantic-tokens-modifier-faces [] :extra-client-capabilities nil :status initialized :metadata #<hash-table equal 0/65 0x156c88bbd60d> :watches #<hash-table equal 0/65 0x156c88bbd62d> :workspace-folders nil :last-id 0 :status-string nil :shutdown-action nil :diagnostics #<hash-table equal 0/65 0x156c88bbe7a9> :work-done-tokens #<hash-table equal 0/65 0x156c88bbeba9>) #<hash-table equal 2/65 0x156c8bd3fed9>)
  lsp--on-notification(#s(lsp--workspace :ewoc nil :server-capabilities #<hash-table equal 9/65 0x156c89209651> :registered-server-capabilities nil :root "/home/jannis/uni/aesop" :client #s(lsp--client :language-id nil :add-on? nil :new-connection (:connect #f(compiled-function (filter sentinel name environment-fn) #<bytecode 0x156c880d8e8d>) :test\? #f(compiled-function () #<bytecode 0x156c880d8ea5>)) :ignore-regexps nil :ignore-messages nil :notification-handlers #<hash-table equal 1/65 0x156c880d8eb1> :request-handlers #<hash-table equal 0/65 0x156c8816ff3d> :response-handlers #<hash-table eql 4/65 0x156c880d8ed1> :prefix-function nil :uri-handlers #<hash-table equal 0/65 0x156c880d8ef1> :action-handlers #<hash-table equal 0/65 0x156c880d8f11> :major-modes (lean4-mode) :activation-fn nil :priority 0 :server-id lean4-lsp :multi-root nil :initialization-options nil :semantic-tokens-faces-overrides nil :custom-capabilities nil :library-folders-fn nil :before-file-open-fn nil :initialized-fn nil :remote? nil :completion-in-comments? nil :path->uri-fn nil :uri->path-fn nil :environment-fn nil :after-open-fn nil :async-request-handlers #<hash-table equal 0/65 0x156c88468d99> :download-server-fn nil :download-in-progress? nil :buffers nil) :host-root nil :proc #<process lean4-lsp> :cmd-proc #<process lean4-lsp> :buffers (#<buffer MutAltTree.lean> #<buffer Percent.lean>) :semantic-tokens-faces [lsp-face-semhl-keyword lsp-face-semhl-variable lsp-face-semhl-property] :semantic-tokens-modifier-faces [] :extra-client-capabilities nil :status initialized :metadata #<hash-table equal 0/65 0x156c88bbd60d> :watches #<hash-table equal 0/65 0x156c88bbd62d> :workspace-folders nil :last-id 0 :status-string nil :shutdown-action nil :diagnostics #<hash-table equal 0/65 0x156c88bbe7a9> :work-done-tokens #<hash-table equal 0/65 0x156c88bbeba9>) #<hash-table equal 3/65 0x156c8bd3fca9>)
  lsp--parser-on-message(#<hash-table equal 3/65 0x156c8bd3fca9> #s(lsp--workspace :ewoc nil :server-capabilities #<hash-table equal 9/65 0x156c89209651> :registered-server-capabilities nil :root "/home/jannis/uni/aesop" :client #s(lsp--client :language-id nil :add-on? nil :new-connection (:connect #f(compiled-function (filter sentinel name environment-fn) #<bytecode 0x156c880d8e8d>) :test\? #f(compiled-function () #<bytecode 0x156c880d8ea5>)) :ignore-regexps nil :ignore-messages nil :notification-handlers #<hash-table equal 1/65 0x156c880d8eb1> :request-handlers #<hash-table equal 0/65 0x156c8816ff3d> :response-handlers #<hash-table eql 4/65 0x156c880d8ed1> :prefix-function nil :uri-handlers #<hash-table equal 0/65 0x156c880d8ef1> :action-handlers #<hash-table equal 0/65 0x156c880d8f11> :major-modes (lean4-mode) :activation-fn nil :priority 0 :server-id lean4-lsp :multi-root nil :initialization-options nil :semantic-tokens-faces-overrides nil :custom-capabilities nil :library-folders-fn nil :before-file-open-fn nil :initialized-fn nil :remote? nil :completion-in-comments? nil :path->uri-fn nil :uri->path-fn nil :environment-fn nil :after-open-fn nil :async-request-handlers #<hash-table equal 0/65 0x156c88468d99> :download-server-fn nil :download-in-progress? nil :buffers nil) :host-root nil :proc #<process lean4-lsp> :cmd-proc #<process lean4-lsp> :buffers (#<buffer MutAltTree.lean> #<buffer Percent.lean>) :semantic-tokens-faces [lsp-face-semhl-keyword lsp-face-semhl-variable lsp-face-semhl-property] :semantic-tokens-modifier-faces [] :extra-client-capabilities nil :status initialized :metadata #<hash-table equal 0/65 0x156c88bbd60d> :watches #<hash-table equal 0/65 0x156c88bbd62d> :workspace-folders nil :last-id 0 :status-string nil :shutdown-action nil :diagnostics #<hash-table equal 0/65 0x156c88bbe7a9> :work-done-tokens #<hash-table equal 0/65 0x156c88bbeba9>))
  #f(compiled-function (proc input) #<bytecode 0x156c88bbebd9>)(#<process lean4-lsp> "Content-Length: 241\15\n\15\n{\"params\":{\"textDocument\":{...")

Sebastian Ullrich (Jun 18 2021 at 12:50):

Yes, like that. Now I'm puzzled though, it seems to forward a request to the wrong handler

Sebastian Ullrich (Jun 18 2021 at 13:02):

Ah no, I misinterpreted it. Could be because of a very old dash version...? https://github.com/emacs-lsp/lsp-mode/issues/1229

Jannis Limperg (Jun 18 2021 at 14:23):

I just nuked and recompiled all my packages, but to no avail. list-packages says my dash is 20210609.1330, so that's probably not it.

Sebastian Ullrich (Jun 18 2021 at 14:31):

Hmmm. Unfortunately this is happening inside the lsp-mode macro for pattern matching on LSP messages, so I'm not exactly sure how to debug that either.

Sebastian Ullrich (Jun 18 2021 at 14:33):

It doesn't help that the hashtable object is a bit inscrutable

Jannis Limperg (Jun 18 2021 at 14:36):

All right, maybe it is time for me to learn elisp after all (or ignore this issue until it goes away). Thanks for the help!

Lucas Viana (Jun 19 2021 at 21:37):

I was having a similar issue, but I don't know if it is related:

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/goal.20view/near/237369198

Jannis Limperg (Jun 21 2021 at 12:50):

I tried commenting out all (two) references to lean4-info-buffer-refresh. That didn't seem to do anything, but then I nuked and reinstalled lean4-mode and the error disappeared. :shrug: Works for me!

Jannis Limperg (Jun 21 2021 at 13:26):

(deleted)


Last updated: Dec 20 2023 at 11:08 UTC