0b7d987699
@kha I have added support for opaque constants to the old C++ frontend, and made sure the new frontend can still parse `library/init/core.lean`. The kernel should enforce that opaque constants are really opaque, and the following example should fail ``` constant x : nat := 0 theorem foo : x = 0 := rfl ``` If it doesn't, it is a bug. Here are some remaining issues: 1- `environment.mk_empty` is currently an axiom because we cannot create an inhabitant of an opaque type. A possible solution is to use `option environment` instead of `environment`. 2- There is no support for opaque constants in the new frontend. However, I modified it to handle axioms, and fixed the literal values with decl_cmd_kind. I tried to mark some of my changes with comments, but it is probably much easier for you to just check the commit change list. 3- I did not add any support for automatically constructing `e` at `constant x : t := e`. I think we can do this later after we replace the old frontend with the new one. BTW, it took only a few minutes to provide the inhabitants manually. |
||
|---|---|---|
| .. | ||
| .gitignore | ||
| lean4-debug.el | ||
| lean4-dev.el | ||
| lean4-eri.el | ||
| lean4-flycheck.el | ||
| lean4-hole.el | ||
| lean4-info.el | ||
| lean4-input.el | ||
| lean4-leanpkg.el | ||
| lean4-mode.el | ||
| lean4-right-click.el | ||
| lean4-settings.el | ||
| lean4-syntax.el | ||
| lean4-type.el | ||
| lean4-util.el | ||
| LICENSE | ||
| README.md | ||
This is the Emacs mode for the Lean theorem prover.
Installation
lean-mode requires GNU Emacs 24.3 or newer. The recommended way to install it is via MELPA. If you have not already configured MELPA, put the following code in your Emacs init file (typically ~/.emacs.d/init.el):
(require 'package) ; You might already have this line
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))
(package-initialize) ; You might already have this line
See also MELPA: Getting Started.
With MELPA configured, you can M-x package-install the packages lean-mode and company-lean. The latter package gives you auto completion and is strongly recommended. There is a third package, helm-lean, which provides a searchable list of declarations on C-c C-d using the Helm interface. helm-lean requires Emacs 24.4 or newer.
For company-lean, you should also bind a key to trigger completion, if you have not already done so:
;; Trigger completion on Shift-Space
(global-set-key (kbd "S-SPC") #'company-complete)
Updating
For updating the Lean MELPA packages, use package-list-packages. See the section "Updating Packages" on MELPA: Getting Started for details.
Trying It Out
If things are working correctly, you should see the word Lean in the
Emacs mode line when you open a file with extension .lean. If you type
#check id
the word #check will be underlined, and hovering over it will show
you the type of id. The mode line will show FlyC:0/1, indicating
that there are no errors and one piece of information displayed.
Key Bindings and Commands
| Key | Function |
|---|---|
| M-. | jump to definition in source file (lean-find-definition) |
| M-, | jump back to position before M-. (xref-pop-marker-stack) |
| C-c C-k | shows the keystroke needed to input the symbol under the cursor |
| C-c C-x | execute lean in stand-alone mode (lean-std-exe) |
| C-c SPC | run a command on the hole at point (lean-hole) |
| C-c C-d | show a searchable list of definitions (helm-lean-definitions) |
| C-c C-g | toggle showing current tactic proof goal (lean-toggle-show-goal) |
| C-c C-n | toggle showing next error in dedicated buffer (lean-toggle-next-error) |
| C-c C-b | toggle showing output in inline boxes (lean-message-boxes-toggle) |
| C-c C-r | restart the lean server (lean-server-restart) |
| C-c C-s | switch to a different Lean version via elan (lean-server-switch-version) |
| C-c ! n | flycheck: go to next error |
| C-c ! p | flycheck: go to previous error |
| C-c ! l | flycheck: show list of errors |
In the default configuration, the Flycheck annotation FlyC:n/n indicates the
number of errors / responses from Lean; clicking on FlyC opens the Flycheck menu.
Message Boxes
To view the output of commands such as check and print in boxes in the buffer, enable the feature using C-c C-b.
If you then type
#check id
a box appears after the line showing the type of id. Customize lean-message-boxes-enabled-captions to choose categories of boxes.
In particular, add "trace output" to the list to see proof states and other traces in the buffer.
Known Issues and Possible Solutions
Unicode
If you experience a problem rendering unicode symbols on emacs, please download the following fonts and install them on your machine:
Then, have the following lines in your emacs setup to use DejaVu Sans Mono font:
(when (member "DejaVu Sans Mono" (font-family-list))
(set-face-attribute 'default nil :font "DejaVu Sans Mono-11"))
You may also need to install the emacs-unicode-fonts package, after which you should add the following lines to your emacs setup:
(require 'unicode-fonts)
(unicode-fonts-setup)
Contributions
Contributions are welcome!
Building from Source
When working on lean-mode itself, it is much easier to just require the sources than repeatedly building the MELPA packages:
(add-to-load-path "~/path/to/lean-mode/")
(require 'company-lean)
(require 'helm-lean)
Make sure you have the packages' dependencies listed on MELPA installed -- the easiest way to do this may be to just install the official Lean MELPA packages and making sure the require commands above are execute before package-initialize.