History

Soonho Kong 3775d07d5f fix(emacs/lean-company): use lean-grab-hname for findp auto-completion fix #214		2014-10-01 09:53:48 -07:00
..
features	test(emacs/features): add ecukes template	2014-09-11 12:33:49 -07:00
test	feat(emacs/lean-syntax): add more word constituents to syntax table	2014-09-30 15:41:18 -07:00
.gitignore	feat(emacs/Cask): add Cask file	2014-09-09 15:11:57 -07:00
Cask	chore(emacs/Cask): add ert-runner, ecukes	2014-09-11 11:12:05 -07:00
CMakeLists.txt	fix(emacs/CMakeLists.txt): add all *.el files when install	2014-09-14 23:15:24 -07:00
eri.el	feat(emacs/eri.el): add eri.el (from agda mode)	2014-08-30 14:57:34 -07:00
lean-changes.el	feat(emacs/lean-changes): handle before/after-revert	2014-09-12 14:25:08 -07:00
lean-cmd.el	feat(emacs/lean-changes): handle before/after-revert	2014-09-12 14:25:08 -07:00
lean-company.el	fix(emacs/lean-company): use lean-grab-hname for findp auto-completion	2014-10-01 09:53:48 -07:00
lean-debug.el	feat(emacs/lean-debug): add lean-debug minor-mode	2014-09-15 16:50:35 -07:00
lean-flycheck.el	fix(emacs/lean-flycheck): fix error/warning pattern to work on windows	2014-09-30 15:40:57 -07:00
lean-info.el	refactor(emacs/debug): rename lean-server-debug to lean-debug	2014-09-12 14:25:08 -07:00
lean-input.el	feat(emacs/lean-input): shortcut for long arrow	2014-09-26 17:50:33 -07:00
lean-mmm-lua.el	feat(lean-mode): enable mmm-parse-when-idle	2014-09-15 10:23:38 -07:00
lean-mode.el	fix(emacs/lean-mode): trigger eri-indent only at the beginning of line	2014-09-29 12:53:22 -07:00
lean-option.el	feat(emacs/lean-flycheck): detect and use flycheck error buffer width	2014-09-30 05:54:46 -07:00
lean-project.el	feat(emacs/lean-project): add lean-project-create to imenu	2014-09-10 15:19:11 -07:00
lean-require.el	chore(emacs/README.md): add 'f' as a required package for lean-mode	2014-09-13 23:35:38 -07:00
lean-server.el	fix(emacs/lean-type): change where to trigger eldoc	2014-09-17 00:24:30 -07:00
lean-settings.el	feat(emacs/lean-flycheck): detect and use flycheck error buffer width	2014-09-30 05:54:46 -07:00
lean-syntax.el	feat(emacs/lean-syntax): add more word constituents to syntax table	2014-09-30 15:41:18 -07:00
lean-tags.el	fix(emacs/lean-tags): support windows	2014-09-20 10:06:42 -07:00
lean-type.el	fix(emacs/lean-type): disable eldoc at flycheck error/warning	2014-09-20 10:20:47 -07:00
lean-util.el	fix(emacs/lean-company): use lean-grab-hname for findp auto-completion	2014-10-01 09:53:48 -07:00
lean-variable.el	feat(emacs/lean-option): save lean-options to lean-global-option-alist	2014-09-15 09:46:06 -07:00
Makefile	fix(emacs/Makefile): add missing Makefile	2014-09-14 23:14:42 -07:00
README.md	chore(emacs/README.md): add 'f' as a required package for lean-mode	2014-09-13 23:35:38 -07:00

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