robkorn/spacemacs-lean-layer

Spacemacs layer for the Lean Theorem Prover.

This is a Spacemacs layer for the Lean theorem prover which uses Lean Mode with updated keybindings.

Lean: https://github.com/leanprover/lean Lean Mode: https://github.com/leanprover/lean-mode

Key Bindings and Commands

Key	Function
g d	jump to definition in source file (lean-find-definition)
Spc m f	jump to definition in source file (lean-find-definition)
Spc m ,	jump back to position before M-. (xref-pop-marker-stack)
Spc m k	shows the keystroke needed to input the symbol under the cursor
Spc m xx	execute lean in stand-alone mode (lean-std-exe)
Spc m h	run a command on the hole at point (lean-hole)
Spc m d	show a searchable list of definitions (helm-lean-definitions)
Spc m g	toggle showing current tactic proof goal (lean-toggle-show-goal)
Spc m n	toggle showing next error in dedicated buffer (lean-toggle-next-error)
Spc m b	toggle showing output in inline boxes (lean-message-boxes-toggle)
Spc m r	restart the lean server (lean-server-restart)
Spc m s	switch to a different Lean version via elan (lean-server-switch-version)
Spc m a	toggle company auto-complete menu
Spc e n	flycheck: go to next error
Spc e p	flycheck: go to previous error
Spc e l	flycheck: show list of errors

Installation

    $ git clone https://github.com/robkorn/spacemacs-lean-layer
    $ cd spacemacs-lean-layer 
    $ mv lean ~/.emacs.d/private/local

Then simply add 'lean' as one of your configuration layers in your spacemacs config.

Possible Issues

1. 'Spc m' isn't available for lean.

After a couple hours of hunting around for why this issue exists it seems it is in relation to the lean-mode package itself. Even using lean-server-restart doesn't seem to initalize it properly. However to fix this simply toggle company auto-complete and for whatever reason Spacemacs remembers you are indeed in Vim mode and should have access to the Vim Leader Key for this major mode. This issue exists whether or not company-lean is installed.

spacemacs-lean-layer's Issues

Update to Lean 4

I was wondering whether you plan to update your layer to lean 4?

lean4-mode is still not on elpa but can be loaded via recipe

Currently, there is a messy transition situation that makes lean almost completely inaccessible in Emacs for the average user. Making your layer usable both with Lean 3 and Lean 4 would help at least the Spacemacs users a lot.

There are also some suggestions for evil keybindings for lean4-mode. These would make sense in the layer config (but probably not in lean4-mode itself as suggested by the cited issue).