Nael — An Emacs major mode for Lean

To install Nael the easy way, first set up Melpa as package-archive, then type M-x package-install RET nael RET. For more detailed instructions, consult the Installation chapter below.

Language Server Protocol (LSP):

• C-c C-e (eglot) starts Eglot, the LSP client.
• C-h . (eldoc-doc-buffer) displays the ElDoc documentation buffer showing tactic state and expected goal at point.
• C-c C-l (lsp) starts lsp-mode, an alternative LSP client. The key is only bound if nael-lsp is (auto)loaded.

Abbreviations:

• C-c C-a (abbrev-mode) enables abbreviations.
• C-c C-k (nael-abbrev-help) echoes abbreviations that expand to the character at point, or, if active, to the selected region.
• C-x ' (expand-abbrev) expands the abbreviation before point without any inserting any character. (Usually, you'd insert a space or newline to expand.)

Build:

• C-c C-c (project-compile) prompts for a command to build the current project. It will suggest lake build because Nael configures the compile-command variable.

Navigation:

• M-a (forward-sentence) go to beginning of current sentence/block, or to previous one.
• M-e (backward-sentence) go to end of current sentence/block, or to next one.
• M-g i (imenu) jumps to an interactively chosen definition in current buffer.

Comments:

• M-; (comment-dwim) toggles the active region as comment or, if no region is active, creates a comment at end of line.
• M-q (prog-fill-reindent-defun) fills the string- or comment-paragraph at point, or reindents the point-surrounding code.

To view the complete list of Nael's user option variables from within Emacs, customize the group nael (and its child-groups) with M-x customize-group RET nael RET. This chapter highlights and elaborates on some of them.

As an exception, Emacs customization groups cannot include keymaps. You can bind custom keys in nael-mode-map like this:

(keymap-set nael-mode-map "C-c ." #'highlight-symbol-at-point)

To automatically enable features (e.g. abbreviations, Eglot or lsp-mode) when Nael is started, customize nael-mode-hook as follows:

(add-hook 'nael-mode-hook #'abbrev-mode)
(add-hook 'nael-mode-hook #'eglot-ensure)

Nael's Abbrev tables use the :regexp property which is incompatible with Company's company-abbrev and Cape's cape-abbrev. Instead, Nael supports completion-at-point natively via nael-abbrev-capf. This CAPF is buffer-locally added to completion-at-point-functions whenever Abbrev mode is enabled inside Nael. To ditch this feature, set the nael-abbrev-capf variable to nil.

Nael's LSP-based features (via Eglot or lsp-mode), require Lean version 4 to be installed.

(require 'package)
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)

;; git clone https://codeberg.org/mekeor/nael.git ~/path/to/nael
(add-to-list 'load-path "~/path/to/nael/nael")
;; (add-to-list 'load-path "~/path/to/nael/nael-lsp")
;; Option 1, eager loading:
(require 'nael)
;; (require 'nael-lsp)
;; Option 2, lazy loading:
;; cd ~/path/to/nael && ./build.el autoloads
;; (require 'nael-autoloads)
;; (require 'nael-lsp-autoloads)
;; Optionally, make readme available as info manual:
(require 'info)
(info-initialize)
(add-to-list 'Info-directory-list "~/path/to/nael/nael")

(require 'package-vc)
(setopt package-vc-selected-packages
 '((nael
 :doc "nael/README.org"
 :lisp-dir "nael"
 :url "https://codeberg.org/mekeor/nael.git")
 ;; (nael-lsp
 ;; :lisp-dir "nael-lsp"
 ;; :url "https://codeberg.org/mekeor/nael.git")
 ))
(package-initialize)
;; Option 1, lazy loading:
(require 'nael-autoloads)
;; (require 'nael-lsp-autoloads)
;; Option 2, eager loading:
;; (require 'nael)
;; (require 'nael-lsp)

(use-package nael
 :vc ( :doc "nael/README.org"
 :lisp-dir "nael"
 :url "https://codeberg.org/mekeor/nael.git"))
;; (use-package nael-lsp
;; :after nael
;; :vc ( :lisp-dir "nael-lsp"
;; :url "https://codeberg.org/mekeor/nael.git"))

Nael is effectively licensed under GNU GPL version 3 only. More precisely, it is licensed under Apache-2.0 and sublicensed under GPL-3.0.

Nael is maintained by Mekeor Melire (mekeor@posteo.de) on Codeberg.