Zulip Chat Archive
Stream: lean4
Topic: emacs lean4-mode
Alexandre Rademaker (Nov 26 2021 at 21:57):
I am getting command-execute: Wrong type argument: commandp, lean4-message-boxes-toggle error following the installation instructions from https://github.com/leanprover/lean4/tree/master/lean4-mode. Lean itself I installed with elan... the Nix setup is quite complicated ..
Tomas Skrivan (Nov 27 2021 at 08:23):
Is your lean4-mode and lean version matching? Did you install stable or nightly version of lean? Stable is really out of date and nightly should be used.
Alexandre Rademaker (Nov 27 2021 at 13:24):
I am using the lean4-mode version from the lean4 repo I cloned yesterday. The lean -v from the terminal is given me Lean (version 4.0.0-nightly-2021-11-26, commit 3ccd44fafae1, Release). Still, I am getting the error:
Sebastian Ullrich (Nov 27 2021 at 13:30):
Without pressing C-c C-b?
Alexandre Rademaker (Nov 27 2021 at 13:49):
Sorry ? What you mean ? Interaction with Lean seems to work, lean4 is quite different form lean3, relearning here. Are you saying that C-c C-b is already known to be broken?
Sebastian Ullrich (Nov 27 2021 at 13:53):
The function behind it doesn't exist anymore, yes
Alexandre Rademaker (Nov 27 2021 at 13:58):
Oh, I see. So C-c TAB and C-c ! l are the only alternatives for inspecting outputs.
Sebastian Ullrich (Nov 27 2021 at 14:04):
The message box functionality can also be replaced with https://github.com/emacs-lsp/lsp-ui#lsp-ui-sideline
Last updated: Dec 20 2023 at 11:08 UTC