czm-lean4.el: Some embellishments for lean4-mode

Overview

This package collects features that I’m using in conjunction with (my fork of bustercopley’s fork of) lean4-mode. (The new feature of my fork is to provide hover docs for the info view.)

1. Reasonable values for beginning-of-defun-function and end-of-defun-function, so that beginning-of-defun (C-M-a), end-of-defun (C-M-e) and narrow-to-defun (C-x n d) work.
2. Reasonable values for outline-regexp and outline-level, so that Outline mode works.
3. A command for displaying the active namespace/section/variable declarations.
4. (Taken from leanprover-community/lean4-mode#22) A command for temporarily pausing the info display.
5. Commands for searching the appropriate Mathlib folder (via consult-ripgrep), either for all text or just theorem-like headings.
6. A command for inserting sections/namespaces, or wrapping a region with those, and similarly for comment blocks.
7. A command for displaying the info buffer below the current window (rather than the default behavior, to the side - I often prefer one over the other).
8. Line wrapping for the goal window, with visual indicators where it wraps.
9. Commands for cycling delimiters, ( -> { -> [ -> ( -> … and in reverse.
10. Commands that help format code according to the Mathlib conventions.
11. Toggleable and live in-buffer proof state overlays, for when you want to see the goal but don’t feel like having the info window open. Use M-x czm-lean4-toggle-goal-overlay and M-x czm-lean4-live-goal-mode.

Configuration

This package requires lean4-mode, so install that first.

Download this repository, install using M-x package-install-file (or package-vc-install, straight, elpaca, …), and add something like the following to your init file:

(use-package czm-lean4
  :after lean4-mode
  :hook (lean4-mode . czm-lean4-mode-hook)
  :hook (magit-section-mode . czm-lean4-magit-section-mode-hook)
  :bind (:map lean4-mode-map
              ("C-c v" . czm-lean4-show-variables)
              ("C-c C-p C-p" . czm-lean4-toggle-info-pause)
              ("C-c m m" . czm-lean4-search-mathlib)
              ("C-c m h" . czm-lean4-search-mathlib-headings)
              ("C-c C-o" . czm-lean4-toggle-info-split-below))
  :config
  (advice-add 'lean4-info-buffer-redisplay :around #'czm-lean4-info-buffer-redisplay))

Customize the binds as you like, and use the built-in documentation (C-h f czm-lean4-whatever) to see exactly what the commands do.

More configuration

My current complete lean4-related configuration can be found in the lean section of my init file. It uses elpaca and makes use of other packages, including eldoc-icebox, preview-auto and preview-tailor. Here’s a lightly edited snapshot, perhaps better suited for inspiration rather than direct use:

(defun czm-set-lean4-local-variables ()
  (setq preview-tailor-local-multiplier 0.7)
  (setq TeX-master my-preview-master))

(use-package lean4-mode
  :ensure (:host github :repo "ultronozm/lean4-mode" :files ("*.el" "data"))
  :diminish
  :hook
  (lean4-mode . czm-set-lean4-local-variables)
  :custom
  (lean4-idle-delay 0.02)
  (lean4-info-plain nil)
  (lean4-info-refresh-even-if-invisible t)
  :bind (:map lean4-mode-map
              ("RET" . newline)
              ("C-j" . newline-and-indent)
              ("C-M-i" . completion-at-point)
              ("C-c C-k" . quail-show-key))
  :config
  (add-to-list 'lean4-workspace-roots "~/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/src/lean/")
  :defer t)

(use-package czm-lean4
  :ensure (:host github :repo "ultronozm/czm-lean4.el" :depth nil)
  :after lean4-mode
  :hook
  (lean4-mode . czm-lean4-mode-hook)
  :hook (magit-section-mode . czm-lean4-magit-section-mode-hook)
  :bind (:map lean4-mode-map
              ("C-c v" . czm-lean4-show-variables)
              ;; ("C-c C-p C-p" . czm-lean4-toggle-info-pause)
              ("C-c C-m C-m" . czm-lean4-search-mathlib)
              ("C-c C-m C-h" . czm-lean4-search-mathlib-headings)
              ("C-c C-m C-g" . czm-lean4-toggle-goal-overlay)
              ("C-c C-m C-l" . czm-lean4-live-goal-mode)
              ("C-c C-," . czm-lean4-insert-section-or-namespace)
              ("C-c C-." . czm-lean4-insert-comment-block)
              ("C-c C-i" . czm-lean4-toggle-info-split-below)
              ("C-c C-y" . czm-lean4-toggle-info-split-right)
              ("M-]" . czm-lean4-cycle-delimiter-forward)
              ("M-[" . czm-lean4-cycle-delimiter-backward))
  :custom
  (czm-lean4-info-window-height-fraction 0.4)
  (czm-lean4-info-window-width-fraction 0.47)
  :config
  (advice-add 'lean4-info-buffer-redisplay :around #'czm-lean4-info-buffer-redisplay)
  (map-keymap
   (lambda (key cmd)
     (define-key lean4-mode-map (vector key) cmd))
   copilot-completion-map))

(defun czm-add-lean4-eldoc ()
  (when (with-current-buffer eldoc-icebox-parent-buffer
          (or (eq major-mode 'lean4-mode)
              (equal (buffer-name)
                     "*Lean Goal*")))
    (add-hook 'eldoc-documentation-functions #'lean4-info-eldoc-function
              nil t)
    (eldoc-mode)))

(use-package eldoc-icebox
  :ensure (:host github :repo "ultronozm/eldoc-icebox.el" :depth nil)
  :bind (("C-c C-h" . eldoc-icebox-store)
         ("C-c C-n" . eldoc-icebox-toggle-display))
  :hook
  (eldoc-icebox-post-display . shrink-window-if-larger-than-buffer)
  (eldoc-icebox-post-display . czm-lean4-fontify-buffer)
  (eldoc-icebox-post-display . czm-add-lean4-eldoc))