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

Stream: lean4

[Jannis Limperg]

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]

Could you give me a stacktrace?

[Jannis Limperg]

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]

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

[Sebastian Ullrich]

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]

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]

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]

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

[Jannis Limperg]

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]

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]

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]

(deleted)