-
Notifications
You must be signed in to change notification settings - Fork 29
/
lean4-mode.info
340 lines (251 loc) · 11 KB
/
lean4-mode.info
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
This is lean4-mode.info, produced by makeinfo version 7.1 from
lean4-mode.texi.
INFO-DIR-SECTION Emacs misc features
START-INFO-DIR-ENTRY
* Lean4-Mode: (lean4-mode). Emacs major mode for Lean language.
END-INFO-DIR-ENTRY
File: lean4-mode.info, Node: Top, Next: Installation, Up: (dir)
Lean4-Mode - Emacs major mode for Lean language
***********************************************
This package extends GNU Emacs (https://www.gnu.org/software/emacs/) by
providing a major mode for editing code written in version 4 of the
programming language and theorem prover Lean (https://lean-lang.org).
The Lean4-Mode source code is developed at Github
(https://github.com/leanprover-community/lean4-mode) and its issues
tracked there too. Further discussions and question-answering takes
place in the #Emacs channel
(https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs) of
Lean's Zulip chat.
For legacy version 3 of Lean, use the archived Lean3-Mode
(https://github.com/leanprover/lean3-mode) (also known as _Lean-Mode_).
* Menu:
* Installation::
* Usage::
* Configuration::
* Common Pitfalls::
-- 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 vc (Emacs 30 or later)::
* Doom-Emacs::
* Straight::
Usage
* lsp-mode::
* Flycheck::
Configuration
* lsp-mode: lsp-mode (1).
* Flycheck: Flycheck (1).
File: lean4-mode.info, Node: Installation, Next: Usage, Prev: Top, Up: Top
1 Installation
**************
* Menu:
* Brief and Generic Instructions::
* Detailed and Concrete Instructions::
* Instructions for Source-Based Use-Package::
File: lean4-mode.info, Node: Brief and Generic Instructions, Next: Detailed and Concrete Instructions, Up: Installation
1.1 Brief and Generic Instructions
==================================
First, install the dependencies of Lean4-Mode:
• Lean (https://lean-lang.org/lean4/doc/setup.html) (version 4)
• Emacs (version 27 or later)
• Emacs packages Dash (https://github.com/magnars/dash.el) (available
on GNU-Elpa), lsp-mode (https://emacs-lsp.github.io/lsp-mode), and
Magit-Section
(https://github.com/magit/magit/blob/main/lisp/magit-section.el)
(available on Melpa)
Second, install Lean4-Mode itself:
• Clone the Git repository of Lean4-Mode
(https://github.com/leanprover-community/lean4-mode).
• In your Emacs initialization file
(https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html),
add the path to that local repository to the ‘load-path’ list.
File: lean4-mode.info, Node: Detailed and Concrete Instructions, Next: Instructions for Source-Based Use-Package, Prev: Brief and Generic Instructions, Up: Installation
1.2 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 GNU Elpa
(https://elpa.gnu.org) package-archive. You can install the remaining
packages either from source or from Melpa
(https://melpa.org/#/getting-started) package-archive. For later
approach, add the following to your Emacs initialization file (e.g.
‘~/.emacs.d/init.el’):
(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)
Clone the Git repository of Lean4-Mode:
git clone https://github.com/leanprover-community/lean4-mode.git ~/path/to/lean4-mode
In your Emacs initialization file, add the path to your local
Lean4-Mode repository to the ‘load-path’ list:
(add-to-list 'load-path "~/path/to/lean4-mode")
Lean4-Mode should now already be enabled when you open a file with
‘.lean’ extension. But you can optionally also already load Lean4-Mode
on Emacs startup, e.g. in order to customize variables:
(require 'lean4-mode)
File: lean4-mode.info, Node: Instructions for Source-Based Use-Package, Prev: Detailed and Concrete Instructions, Up: Installation
1.3 Instructions for Source-Based Use-Package
=============================================
If you use a source-based package-manager (e.g. ‘package-vc.el’,
Straight or Elpaca), then make sure to list the ‘"data"’ directory in
your Lean4-Mode package recipe.
If you use the ‘use-package’ macro and intent to defer loading of
packages in order to improve your Emacs startup time, then make sure to
specify ‘lean4-mode’ as a ‘:command’.
Following subsections show concrete examples.
* Menu:
* Native vc (Emacs 30 or later)::
* Doom-Emacs::
* Straight::
File: lean4-mode.info, Node: Native vc (Emacs 30 or later), Next: Doom-Emacs, Up: Instructions for Source-Based Use-Package
1.3.1 Native ‘:vc’ (Emacs 30 or later)
--------------------------------------
GNU Emacs comes with ‘use-package.el’ built-in since version 29. And
since version 30, it also comes with a built-in ‘:vc’ keyword for the
‘use-package’ macro that utilizes ‘package-vc.el’ to install Emacs
packages from remote source repositories.
(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
))
File: lean4-mode.info, Node: Doom-Emacs, Next: Straight, Prev: Native vc (Emacs 30 or later), Up: Instructions for Source-Based Use-Package
1.3.2 Doom-Emacs
----------------
If you use Doom-Emacs, you can place the following code in your Doom
initialization file:
(package! lean4-mode
:recipe (:host github
:repo "leanprover-community/lean4-mode"
:files ("*.el" "data")))
File: lean4-mode.info, Node: Straight, Prev: Doom-Emacs, Up: Instructions for Source-Based Use-Package
1.3.3 Straight
--------------
If you use the Straight package manager through Use-Package, then place
the following code in your Emacs initialization file:
(use-package lean4-mode
:commands lean4-mode
:straight (lean4-mode :type git :host github
:repo "leanprover-community/lean4-mode"
:files ("*.el" "data")))
File: lean4-mode.info, Node: Usage, Next: Configuration, Prev: Installation, Up: Top
2 Usage
*******
If things are working correctly, you should see the word "Lean 4" in
Emacs mode-line when you open a file with ‘.lean’ extension. Emacs will
ask you to identify the _project_ this file belongs to. If you then
type ‘#check id’, the word ‘#check’ will be underlined, and hovering
over it will show you the type of ‘id’.
To view the proof state, run ‘lean4-toggle-info’ (‘C-c C-i’). This
will display the ‘*Lean Goals*’ buffer (like the Lean Info-View pane in
VS-Code) in a separate window.
Key Description Command
----------------------------------------------------------------------------------------------------------------------
‘C-c C-k’ Echo the keystroke needed to input the symbol at point ‘quail-show-key’
‘C-c C-d’ Recompile and reload imports ‘lean4-refresh-file-dependencies’
‘C-c C-x’ or ‘C-c C-l’ Execute Lean in stand-alone mode ‘lean4-std-exe’
‘C-c C-p C-l’ Builds package with lake ‘lean4-lake-build’
‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-toggle-info-buffer’
* Menu:
* lsp-mode::
* Flycheck::
File: lean4-mode.info, Node: lsp-mode, Next: Flycheck, Up: Usage
2.1 lsp-mode
============
For key bindings from lsp-mode, see its respective documentation
(https://emacs-lsp.github.io/lsp-mode/page/keybindings/) and note that
not all capabilities are supported by Lean4-Mode.
File: lean4-mode.info, Node: Flycheck, Prev: lsp-mode, Up: Usage
2.2 Flycheck
============
You may optionally use Lean4-Mode together with Flycheck. In that case,
the mode-line will show ‘FlyC:E/N’, indicating that there are ‘E’ number
of errors and ‘N’ number of notes. Following keys will be available by
default (via ‘flycheck-mode-map’):
Key Description Command
---------------------------------------------------------------
‘C-c ! n’ Go to next error ‘flycheck-next-error’
‘C-c ! p’ Go to previous error ‘flycheck-previous-error’
File: lean4-mode.info, Node: Configuration, Next: Common Pitfalls, Prev: Usage, Up: Top
3 Configuration
***************
* Menu:
* lsp-mode: lsp-mode (1).
* Flycheck: Flycheck (1).
File: lean4-mode.info, Node: lsp-mode (1), Next: Flycheck (1), Up: Configuration
3.1 lsp-mode
============
If you want breadcrumbs of namespaces and sections to be shown in the
header-line, set the user option ‘lsp-headerline-breadcrumb-enable’ to
‘t’.
File: lean4-mode.info, Node: Flycheck (1), Prev: lsp-mode (1), Up: Configuration
3.2 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 ‘lsp-diagnostics-provider’ user option
accordingly.
File: lean4-mode.info, Node: Common Pitfalls, Prev: Configuration, Up: Top
4 Common Pitfalls
*****************
Lean4-Mode only supports version 4 of Lean. For editing Lean version 3,
use Lean3-Mode (https://github.com/leanprover/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 ‘lean-’ for its symbols. E.g. you
should not use ‘lean-’-prefixed commands in a buffer with Lean4-Mode as
major mode.
Tag Table:
Node: Top223
Node: Installation1492
Node: Brief and Generic Instructions1735
Node: Detailed and Concrete Instructions2684
Node: Instructions for Source-Based Use-Package4341
Node: Native vc (Emacs 30 or later)5062
Node: Doom-Emacs5970
Node: Straight6396
Node: Usage6896
Node: lsp-mode8342
Node: Flycheck8627
Node: Configuration9237
Node: lsp-mode (1)9427
Node: Flycheck (1)9696
Node: Common Pitfalls10181
End Tag Table
Local Variables:
coding: utf-8
End: