Types not fitting into echo area

Stream: Emacs

[Dominic Steinitz]

I think I have lean working in emacs. One thing I have a problem with is that if I hover over an identifier then there is no pop up showing the type like there is in VS but there is something in the echo area. But sadly the echo area is not big enough to contain the type. I have tried various incantations to expand the echo area but to no avail.

Is this a known problem? And is there a known solution?

[Mauricio Collares]

I think everything printed in the echo area (minibuffer) ends up in the *Messages* buffer

[Mauricio Collares]

But maybe you'll get a more VS Code-like experience if you add (use-package lsp-ui) to your config file (but I don't use this package so I'm not sure)

[Dominic Steinitz]

That's what I though (the echo area ending up in the *Messages* buffer) but that is not happening so either my installation is somehow borked or maybe it is up to the package to decide which output goes where.

[Dominic Steinitz]

But I do see this when I open a .lean file

LSP :: Unable to autoconfigure company-mode. [2 times]
LSP :: Connected to [lean4-lsp:1398 /Users/dom/Dropbox/Tidy/DifferentialGeometry/TestLean].

[Yury G. Kudryashov]

What are the lean and lsp-related lines in your config file?

[Dominic Steinitz]

I am not sure what you mean by config file - .emacs?

(use-package lean4-mode
  :straight (lean4-mode
         :type git
         :host github
         :repo "leanprover/lean4-mode"
         :files ("*.el" "data"))
  ;; to defer loading the package until required
  :commands (lean4-mode))

(require 'lean4-mode)

[Richard Copley]

You could try the command eldoc-doc-buffer show the Eldoc documentation buffer. It might also be necessary to customize the variable eldoc-echo-area-prefer-doc-buffer to the value t ("Prefer ElDoc's documentation buffer").

[Dominic Steinitz]

Thanks for this but the eldoc-doc-buffer just shows the single line I see in the echo area i.e. not the full type. I am about to ask what my .emacs file should be given all the work that has been going on so no need to reply. And thanks once again.

[Mahdi Khaleghi]

add LSP UI Mode to your installation:

;; Install lsp-ui
  (use-package lsp-ui
    :commands lsp-ui-mode
    :hook (lsp-mode . lsp-ui-mode)
    :config
    (setq lsp-ui-sideline-show-hover t
          lsp-ui-doc-enable t))

  (use-package lean4-mode
    :straight (lean4-mode :type git :host github
                          :repo "leanprover-community/lean4-mode"
                          :commit "8404acf3d8facf3351d78ac18e9414d27872105c" ;if your lsp buffer is empty, they fixed it in this commit.
                          :files ("*.el" "data"))
    :hook ((lean4-mode . lsp)
           (lean4-mode . lsp-ui-mode)) ; Add lsp-ui-mode if you want UI enhancements

please delete your lean4-mode folder from your straight directory before changing it.