b538b3e0bf
If we have a singleton auto-complete candidate (e.g. proof_irrel) and it does not matched with input prefix (e.g. foo), we add the input prefix (foo) as an extra candidate to prevent the candidate (proof_irrel) from being automatically selected and completed. |
||
|---|---|---|
| .. | ||
| features | ||
| test | ||
| .gitignore | ||
| Cask | ||
| CMakeLists.txt | ||
| eri.el | ||
| lean-changes.el | ||
| lean-cmd.el | ||
| lean-company.el | ||
| lean-debug.el | ||
| lean-flycheck.el | ||
| lean-info.el | ||
| lean-input.el | ||
| lean-mmm-lua.el | ||
| lean-mode.el | ||
| lean-option.el | ||
| lean-project.el | ||
| lean-require.el | ||
| lean-server.el | ||
| lean-settings.el | ||
| lean-syntax.el | ||
| lean-tags.el | ||
| lean-type.el | ||
| lean-util.el | ||
| lean-variable.el | ||
| Makefile | ||
| README.md | ||
lean-mode
Emacs mode for lean theorem prover
Requirement
lean-mode requires Emacs 24 and following
packages which can be installed via M-x package-install.
The following packages are optional but we recommend to install them
to use full features of lean-mode.
Install
Put the following elisp code on your emacs setup (e.g. .emacs.d/init.el):
(require 'package)
(add-to-list 'package-archives
'("melpa" . "http://melpa.milkbox.net/packages/") t)
(package-initialize)
(package-refresh-contents)
;; Install required/optional packages for lean-mode
(defvar lean-mode-required-packages
'(company dash dash-functional flycheck whitespace-cleanup-mode
f fill-column-indicator s lua-mode mmm-mode))
(dolist (p lean-mode-required-packages)
(when (not (package-installed-p p))
(package-install p)))
;; Set up lean-root path
(setq lean-rootdir "~/projects/lean")
(setq-local lean-emacs-path
(concat (file-name-as-directory lean-rootdir)
(file-name-as-directory "src")
"emacs"))
(add-to-list 'load-path (expand-file-name lean-emacs-path))
(require 'lean-mode)
;; Customization for lean-mode
(customize-set-variable 'lean-delete-trailing-whitespace t)
(customize-set-variable 'lean-flycheck-use t)
(customize-set-variable 'lean-eldoc-use t)
If experience a problem reading unicode characters on emacs, consider having the following setup:
(when (member "DejaVu Sans Mono" (font-family-list))
(set-face-attribute 'default nil :font "DejaVu Sans Mono-11"))
Key Bindings
| Key | Function |
|---|---|
| C-c C-x | lean-std-exe |
| C-c C-l | lean-std-exe |
| C-c C-t | lean-eldoc-documentation-function |
| C-c C-f | lean-fill-placeholder |
| M-. | lean-find-tag |
| TAB | lean-tab-indent-or-complete |
| C-c C-o | lean-set-option |
| C-c C-e | lean-eval-cmd |
Contribution
Contribution is welcome!
If your contribution is a bug fix, create your topic branch from
master. If it is a new feature, check if there exists a
WIP(work-in-progress) branch (vMAJOR.MINOR-wip). If it does, use
that branch, otherwise use master.
Install Cask if you haven't already, then:
$ cd /path/to/lean/src/emacs
$ cask
Run all tests with:
$ make