Windows版 LEAN のインストール方法
１．Windows版 LEANをダウンロード。
ファイル名 lean-0.2.0-windows.zip
解凍し、ディレクトリごと保存したい場所へコピー。
（例： C:\lean-0.2.0-windows ）
入手先 ⇒ こちら
リンク先にある Download the Lean zip file for Windows のうち、
Lean zip file for Windowsをクリックすると
lean-0.2.0-windows.zip
がダウンロードできる。
２．Emacs 24.3以降をインストール
入手先 ⇒ こちら
Emacsのインストール後、実行ファイルのあるパス（例：C:\emacs\bin）を環境変数に追加する。
３．Python3.5以降をインストール
入手先 ⇒ こちら
環境変数の設定不要。自動で行われる。
４．Emacsの設定。
Emacsの設定ファイル（例：init.el）に次を記入。
ただし、
Emacsのインストールディレクトリを C:\emacs-24.3
LEANのインストールディレクトリを C:\lean-0.2.0-windows
とした場合の設定。
(require ‘package)
(add-to-list ‘package-archives ‘(“melpa” . “http://melpa.milkbox.net/packages/”) t)
(when (< emacs-major-version 24) ;; For important compatibility libraries like cl-lib (add-to-list 'package-archives '("gnu" . "http://elpa.gnu.org/packages/"))) (package-initialize) ;; Install required/optional packages for lean-mode (defvar lean-mode-required-packages '(company dash dash-functional flycheck f fill-column-indicator s lua-mode mmm-mode)) (let ((need-to-refresh t)) (dolist (p lean-mode-required-packages) (when (not (package-installed-p p)) (when need-to-refresh (package-refresh-contents) (setq need-to-refresh nil)) (package-install p)))) ;; Set up lean-root path (setq lean-rootdir "\\lean-0.2.0-windows") (setq-local lean-emacs-path "\\lean-0.2.0-windows\\share\\emacs\\site-lisp\\lean") (add-to-list 'load-path (expand-file-name lean-emacs-path)) (require 'lean-mode) (custom-set-variables ;; custom-set-variables was added by Custom. ;; If you edit it by hand, you could mess it up, so be careful. ;; Your init file should contain only one such instance. ;; If there is more than one, they won't work right. ) (custom-set-faces ;; custom-set-faces was added by Custom. ;; If you edit it by hand, you could mess it up, so be careful. ;; Your init file should contain only one such instance. ;; If there is more than one, they won't work right. '(default ((t (:family "Meiryo UI" :foundry "outline" :slant normal :weight normal :height 98 :width normal))))) (require 'unicode-fonts) (unicode-fonts-setup)
５．起動テスト
lean-0.2.0-windows.zipの解答先の binディレクトリ内にある
leanemacs.bat
をダブルクリック。
無事に起動できると Emacs が LEANモードで立ち上がる。
↑ 成功時の画面。
参考」
http://leanprover.github.io/download/wininst/
