lean4-mode.texi

\input texinfo    @c -*- texinfo -*-
@c %**start of header
@setfilename lean4-mode.info
@settitle Lean4-Mode - Emacs major mode for Lean language
@documentencoding UTF-8
@documentlanguage en
@c %**end of header

@dircategory Emacs misc features
@direntry
* Lean4-Mode: (lean4-mode). Emacs major mode for Lean language.
@end direntry

@finalout
@titlepage
@title Lean4-Mode - Emacs major mode for Lean language
@end titlepage

@contents

@ifnottex
@node Top
@top Lean4-Mode - Emacs major mode for Lean language

This package extends @uref{https://www.gnu.org/software/emacs/, GNU Emacs} by providing a major mode for editing
code written in version 4 of the programming language and theorem
prover @uref{https://lean-lang.org, Lean}.

The Lean4-Mode source code is developed at @uref{https://github.com/leanprover-community/lean4-mode, Github} and its issues
tracked there too.  Further discussions and question-answering takes
place in the @uref{https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs, #Emacs channel} of Lean's Zulip chat.

For legacy version 3 of Lean, use the archived @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode} (also known
as @emph{Lean-Mode}).

@end ifnottex

@menu
* Installation::
* Usage::
* Configuration::
* Common Pitfalls::

@detailmenu
--- The Detailed Node Listing ---

Installation

* Brief and Generic Instructions::
* Detailed and Concrete Instructions::
* Instructions for Source-Based Use-Package::

Instructions for Source-Based Use-Package

* Native @samp{vc} (Emacs 30 or later)::
* Doom-Emacs::
* Straight::

Usage

* lsp-mode::
* Flycheck::

Configuration

* lsp-mode: lsp-mode (1). 
* Flycheck: Flycheck (1). 

@end detailmenu
@end menu

@node Installation
@chapter Installation

@menu
* Brief and Generic Instructions::
* Detailed and Concrete Instructions::
* Instructions for Source-Based Use-Package::
@end menu

@node Brief and Generic Instructions
@section Brief and Generic Instructions

First, install the dependencies of Lean4-Mode:
@itemize
@item
@uref{https://lean-lang.org/lean4/doc/setup.html, Lean} (version 4)
@item
Emacs (version 27 or later)
@item
Emacs packages @uref{https://github.com/magnars/dash.el, Dash} (available on GNU-Elpa), @uref{https://emacs-lsp.github.io/lsp-mode, lsp-mode}, and
@uref{https://github.com/magit/magit/blob/main/lisp/magit-section.el, Magit-Section} (available on Melpa)
@end itemize

Second, install Lean4-Mode itself:
@itemize
@item
Clone the @uref{https://github.com/leanprover-community/lean4-mode, Git repository of Lean4-Mode}.
@item
In your @uref{https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html, Emacs initialization file}, add the path to that local
repository to the @code{load-path} list.
@end itemize

@node Detailed and Concrete Instructions
@section Detailed and Concrete Instructions

Install Lean version 4.

Install Emacs version 27 or later.

Install the Emacs packages Dash, lsp-mode and Magit-Section.  Dash is
the only one of these packages that is available in the default @uref{https://elpa.gnu.org, GNU
Elpa} package-archive.  You can install the remaining packages either
from source or from @uref{https://melpa.org/#/getting-started, Melpa} package-archive.  For later approach, add
the following to your Emacs initialization file
(e.g. @samp{~/.emacs.d/init.el}):

@lisp
(require 'package)

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

(add-to-list 'package-selected-packages 'dash)
(add-to-list 'package-selected-packages 'lsp-mode)
(add-to-list 'package-selected-packages 'magit-section)

(package-refresh-contents)
(package-install-selected-packages 'no-confirm)
@end lisp

Clone the Git repository of Lean4-Mode:

@example
git clone https://github.com/leanprover-community/lean4-mode.git ~/path/to/lean4-mode
@end example

In your Emacs initialization file, add the path to your local
Lean4-Mode repository to the @code{load-path} list:
@lisp
(add-to-list 'load-path "~/path/to/lean4-mode")
@end lisp

Lean4-Mode should now already be enabled when you open a file with
@samp{.lean} extension.  But you can optionally also already load
Lean4-Mode on Emacs startup, e.g. in order to customize variables:
@lisp
(require 'lean4-mode)
@end lisp

@node Instructions for Source-Based Use-Package
@section Instructions for Source-Based Use-Package

If you use a source-based package-manager (e.g. @samp{package-vc.el},
Straight or Elpaca), then make sure to list the @samp{"data"} directory in
your Lean4-Mode package recipe.

If you use the @code{use-package} macro and intent to defer loading of
packages in order to improve your Emacs startup time, then make sure
to specify @code{lean4-mode} as a @samp{:command}.

Following subsections show concrete examples.

@menu
* Native @samp{vc} (Emacs 30 or later)::
* Doom-Emacs::
* Straight::
@end menu

@node Native @samp{vc} (Emacs 30 or later)
@subsection Native @samp{:vc} (Emacs 30 or later)

GNU Emacs comes with @samp{use-package.el} built-in since version 29.  And
since version 30, it also comes with a built-in @samp{:vc} keyword for the
@code{use-package} macro that utilizes @samp{package-vc.el} to install Emacs
packages from remote source repositories.

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

(use-package lean4-mode
  :commands lean4-mode
  :vc (:url "https://github.com/leanprover-community/lean4-mode.git"
       :rev :last-release
       ;; Or, if you prefer the bleeding edge version of Lean4-Mode:
       ;; :rev :newest
       ))
@end lisp

@node Doom-Emacs
@subsection Doom-Emacs

If you use Doom-Emacs, you can place the following code in your Doom
initialization file:

@lisp
(package! lean4-mode
  :recipe (:host github
           :repo "leanprover-community/lean4-mode"
           :files ("*.el" "data")))
@end lisp

@node Straight
@subsection Straight

If you use the Straight package manager through Use-Package, then
place the following code in your Emacs initialization file:

@lisp
(use-package lean4-mode
  :commands lean4-mode
  :straight (lean4-mode :type git :host github
                        :repo "leanprover-community/lean4-mode"
                        :files ("*.el" "data")))
@end lisp

@node Usage
@chapter Usage

If things are working correctly, you should see the word "Lean 4" in
Emacs mode-line when you open a file with @samp{.lean} extension.  Emacs
will ask you to identify the @emph{project} this file belongs to.  If you
then type @samp{#check id}, the word @samp{#check} will be underlined, and
hovering over it will show you the type of @code{id}.

To view the proof state, run @code{lean4-toggle-info} (@samp{C-c C-i}).  This
will display the @samp{*Lean Goals*} buffer (like the Lean Info-View pane
in VS-Code) in a separate window.

@multitable {aaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa}
@headitem Key
@tab Description
@tab Command
@item @samp{C-c C-k}
@tab Echo the keystroke needed to input the symbol at point
@tab @code{quail-show-key}
@item @samp{C-c C-d}
@tab Recompile and reload imports
@tab @code{lean4-refresh-file-dependencies}
@item @samp{C-c C-x} or @samp{C-c C-l}
@tab Execute Lean in stand-alone mode
@tab @code{lean4-std-exe}
@item @samp{C-c C-p C-l}
@tab Builds package with lake
@tab @code{lean4-lake-build}
@item @samp{C-c C-i}
@tab Toggle Info-View which shows goals and errors at point
@tab @code{lean4-toggle-info-buffer}
@end multitable

@menu
* lsp-mode::
* Flycheck::
@end menu

@node lsp-mode
@section lsp-mode

For key bindings from lsp-mode, see @uref{https://emacs-lsp.github.io/lsp-mode/page/keybindings/, its respective documentation} and
note that not all capabilities are supported by Lean4-Mode.

@node Flycheck
@section Flycheck

You may optionally use Lean4-Mode together with Flycheck.  In that
case, the mode-line will show @samp{FlyC:E/N}, indicating that there are
@samp{E} number of errors and @samp{N} number of notes.  Following keys will be
available by default (via @code{flycheck-mode-map}):

@multitable {aaaaaaaaa} {aaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaa}
@headitem Key
@tab Description
@tab Command
@item @samp{C-c ! n}
@tab Go to next error
@tab @code{flycheck-next-error}
@item @samp{C-c ! p}
@tab Go to previous error
@tab @code{flycheck-previous-error}
@end multitable

@node Configuration
@chapter Configuration

@menu
* lsp-mode: lsp-mode (1). 
* Flycheck: Flycheck (1). 
@end menu

@node lsp-mode (1)
@section lsp-mode

If you want breadcrumbs of namespaces and sections to be shown in the
header-line, set the user option @code{lsp-headerline-breadcrumb-enable} to
@code{t}.

@node Flycheck (1)
@section Flycheck

Flycheck is an optional but supported dependency of Lean4-Mode.  If
Flycheck is installed, lsp-mode and thus Lean4-Mode will by default
use it.  If you want to customize this behavior, e.g. if you'd like to
use Emacs' built-in Flymake package instead of Flycheck while keeping
later installed, then customize the @code{lsp-diagnostics-provider} user
option accordingly.

@node Common Pitfalls
@chapter Common Pitfalls

Lean4-Mode only supports version 4 of Lean.  For editing Lean version
3, use @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode}, which is also known as Lean-Mode due to historical
reasons.  In principle, it is fine to have both Lean3-Mode and
Lean4-Mode installed at the same time.  But note that Lean3-Mode uses
the prefix @samp{lean-} for its symbols.  E.g. you should not use
@samp{lean-}-prefixed commands in a buffer with Lean4-Mode as major mode.

@bye