diff --git a/README.md b/README.md
index 68b20d2b8..84178151b 100644
--- a/README.md
+++ b/README.md
@@ -18,13 +18,9 @@ Requirements
- [GMP (GNU multiprecision library)](http://gmplib.org/)
- [MPFR (GNU MPFR Library)](http://www.mpfr.org/)
- [Lua 5.2 or 5.1](http://www.lua.org), or [LuaJIT 2.0](http://luajit.org)
-- (optional) [gperftools](https://code.google.com/p/gperftools/)
-- (optional) [Boost](http://www.boost.org) (version >= 1.54), we can
- build Lean using boost::thread instead of std::thread. When using
- Boost, Lean can modify the thread stack size.
-Installing required packages at
---------------------------------
+Installing
+----------
_Windows_
@@ -32,8 +28,8 @@ _Windows_
_Linux_
-- [Ubuntu 12.04 or newer](doc/make/ubuntu-12.04.md)
- [Ubuntu 12.04 or newer (detailed)](doc/make/ubuntu-12.04-detailed.md)
+- [Ubuntu 12.04 or newer (brief)](doc/make/ubuntu-12.04.md)
- [Fedora 19](doc/make/fedora-19.md)
_OS X_
diff --git a/doc/make/ubuntu-12.04-detailed.md b/doc/make/ubuntu-12.04-detailed.md
index 2ae52c3cc..ae6f41253 100644
--- a/doc/make/ubuntu-12.04-detailed.md
+++ b/doc/make/ubuntu-12.04-detailed.md
@@ -3,12 +3,9 @@ Preparing working environment on Ubuntu 12.04
### Install basic packages
- sudo apt-get install git
- sudo apt-get install libgmp-dev
- sudo apt-get install libmpfr-dev
+ sudo apt-get install git libgmp-dev libmpfr-dev emacs -y
sudo add-apt-repository ppa:kalakris/cmake -y
- sudo apt-get install cmake
- sudo apt-get install liblua5.2.0 lua5.2-0 lua5.2-dev
+ sudo apt-get install cmake liblua5.2.0 lua5.2-0 lua5.2-dev -y
sudo add-apt-repository ppa:ubuntu-toolchain-r/test -y
sudo update-alternatives --remove-all gcc
@@ -19,14 +16,10 @@ Preparing working environment on Ubuntu 12.04
### Optional packages
- sudo apt-get install gitg
- sudo apt-get install valgrind
- sudo apt-get install doxygen
- sudo apt-get install kcachegrind
+ sudo apt-get install gitg ninja-build valgrind doxygen kcachegrind
sudo add-apt-repository --yes ppa:boost-latest/ppa
- sudo apt-get install libboost1.54-dev
- sudo apt-get install libboost-thread1.54-dev
+ sudo apt-get install libboost1.54-dev libboost-thread1.54-dev
### Fork Lean on github : https://github.com/leanprover/lean2
@@ -48,12 +41,20 @@ Preparing working environment on Ubuntu 12.04
cmake -D CMAKE_BUILD_TYPE=Release ../src
make
-### Alternatively, build Lean using Boost
+### Alternative ways to build
+Using Ninja (to speed up build)
+
+ cmake -DCMAKE_BUILD_TYPE=RELEASE -G Ninja ../src
+ ninja
+
+Using Boost (to speed up build)
- cd lean2
- mkdir -p build
- cd build
cmake -D CMAKE_BUILD_TYPE=Release -D BOOST=ON ../src
make
+Build in debug mode
+
+ cmake -DCMAKE_BUILD_TYPE=DEBUG ../src
+ make
+
### You need to also set up the [Emacs Mode](../../src/emacs/README.md).
diff --git a/src/emacs/README.md b/src/emacs/README.md
index b8133319e..a1144fc89 100644
--- a/src/emacs/README.md
+++ b/src/emacs/README.md
@@ -1,63 +1,17 @@
-Emacs mode for [lean theorem prover][Lean]
-
-[lean]: https://github.com/leanprover/lean
-
-
-Requirements
-============
-
-``lean-mode`` requires [Emacs 24][emacs24] and the following
-packages, which can be installed via M-x package-install.
-
- - [dash][dash]
- - [dash-functional][dash]
- - [f][f]
- - [s][s]
-
-[emacs24]: http://www.gnu.org/software/emacs
-[dash]: https://github.com/magnars/dash.el
-[f]: https://github.com/rejeep/f.el
-[s]: https://github.com/magnars/s.el
-
-The following packages are optional, but strongly recommended.
-
- - [company][company]
- - [flycheck][flycheck]
- - [fill-column-indicator][fci]
-
-Both the optional and required packages will be installed for you
-automatically the first time you use ``lean-mode``, if you follow the
-installation instructions below.
-
-[company]: http://company-mode.github.io/
-[flycheck]: http://www.flycheck.org/manual/latest/index.html
-[fci]: https://github.com/alpaker/Fill-Column-Indicator
+Emacs mode for the [Lean 2 theorem prover][Lean2]. ``lean-mode`` requires [Emacs 24][emacs24]
+[Lean2]: https://github.com/leanprover/lean2
Installation
============
-When Emacs is started, it loads startup information from a special
-initialization file, often called an "init file." The init file can be
-found in different places on different systems:
+Open your emacs init file. Do this by running Emacs and go to the file using C-c C-f
+(control-C, control-F) and then entering ``~/.emacs``. Now paste the following code into this file (assuming you built Lean from source).
-- Emacs will check for a file named ``.emacs`` in your home directory.
-- With GNU Emacs, it is common to use ``.emacs.d/init.el`` instead.
-- With Aquamacs, it is common to use ``~/Library/Preferences/Aquamacs Emacs/Preferences.el``.
+Note: You paste text in Emacs using C-y (control-Y). See [this wiki page][emacs-copy-paste]. See [this reference sheet][emacs-ref] for other basic Emacs commands.
-On Windows, there are two additional complications:
-
-- It may be hard to figure out what Emacs considers to be your "home
- directory".
-- The file explorer may not let you create a file named ``.emacs``,
- since it begins with a period.
-
-One solution is to run Emacs itself and create the file using C-c C-f
-(control-C, control-F) and then entering ``~/.emacs``. (The tilde
-indicates your home directory.) On Windows, you can also name the file
-``_emacs``.
-
-Put the following code in your Emacs init file:
+[emacs-ref]: https://www.emacswiki.org/emacs/EmacsNewbieKeyReference
+[emacs-copy-paste]: https://www.emacswiki.org/emacs/CopyAndPaste
```elisp
(require 'package)
@@ -78,16 +32,7 @@ Put the following code in your Emacs init file:
(package-refresh-contents)
(setq need-to-refresh nil))
(package-install p))))
-```
-Then choose your installation method from the following scenarios, and add the corresponding code to
-your init file: (note: you need to change the directory in the following code snippets to the
-directory of your clone of the repository).
-
-Case 1: Build Lean from source
------------------------------
-
-```elisp
;; Set up lean-root path
(setq lean-rootdir "~/projects/lean2") ;; <=== YOU NEED TO MODIFY THIS
(setq-local lean-emacs-path
@@ -98,9 +43,14 @@ Case 1: Build Lean from source
(require 'lean-mode)
```
-Case 2: Install Lean via apt-get on Ubuntu or via dpkg on Debian
-----------------------------------------------------------------
+Then modify the directory in `(setq lean-rootdir "~/projects/lean2")` to your Lean folder. Now close Emacs C-x C-c and open Emacs again.
+Emacs will install all required packages now for you.
+If you didn't build Lean 2 from source, but installed it, replace `;; Set up lean-root path` and everything below with the following snippets, depending on how you got Lean 2.
+
+
+Installed Lean 2 via apt-get on Ubuntu or via dpkg on Debian
+----------------------------------------------------------------
```elisp
;; Set up lean-root path
(setq lean-rootdir "/usr")
@@ -110,7 +60,7 @@ Case 2: Install Lean via apt-get on Ubuntu or via dpkg on Debian
```
-Case 3: Install Lean via homebrew on OS X
+Installed Lean 2 via homebrew on OS X
-----------------------------------------
```elisp
@@ -126,7 +76,7 @@ location, please run `brew info lean`, and it will tell you where the
lean-mode files are located. With that information, update the
`lean-emacs-path` variable accordingly.
-Case 4: Install Lean in Windows
+Installed Lean 2 in Windows
-------------------------------
```elisp
;; Set up lean-root path
@@ -136,30 +86,31 @@ Case 4: Install Lean in Windows
(require 'lean-mode)
```
-
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` (for the
-standard Lean mode) or `.hlean` (for hott mode). If you type
-```lean
-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. Whenever
-you type, an asterisk should briefly appear after ``FlyC``, indicating that
-your file is being checked.
+Emacs mode line (at the bottom of the window) when you open a file with extension `.lean` (for the
+standard Lean mode) or `.hlean` (for hott mode).
-If you get an error which contains `failed to lock file`, you need to create a `.project` file:
+If you create a new Lean file, you have to create a `.project` file in that folder:
- open a `.lean` or `.hlean` file
- go to menu-bar (top of screen) -> Lean -> Create a new project
- click open
- it will ask "standard or hott": type which mode you want to use and press enter
-- now it has created a project file (which manages imports and so on for files outside the library), and if you go back to your `.lean` or `.hlean` file these error messages will disappear.
+- Go back to your `.lean` or `.hlean` file (you can close the `.project` file using C-x k RET (RET is enter)). You might need to close and reopen Emacs for the error messages to disappear.
+You can check a file using the shortcut C-c C-x. There is also on-the-fly checking, if you type in a new file
+```lean
+print id
+```
+the word ``print`` 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 0 errors and 1 message. Whenever
+you type, an asterisk should briefly appear after ``FlyC``, indicating that
+your file is being checked.
+Some unicode characters might look weird (or make a line very high). See below to fix that.
Key Bindings and Commands
=========================
@@ -190,7 +141,7 @@ To profile Lean performace on the file in the buffer, enter M-x lean-execut
Some basic configurations (optional)
-====================================
+------------------------------------
```lisp
(custom-set-variables
@@ -222,6 +173,12 @@ Some basic configurations (optional)
'(("\\<\\(thread_local\\)\\>" . font-lock-warning-face)
("\\<\\(constexpr\\)\\>" . font-lock-keyword-face)
))
+
+(require 'ido)
+(ido-mode t)
+(setq completion-ignored-extensions
+ (append '(".ilean" ".olean" ".clean" ".d") completion-ignored-extensions))
+
```
Known Issues and Possible Solutions
@@ -233,8 +190,11 @@ Unicode
If you experience a problem rendering unicode symbols on emacs,
please download the following fonts and install them on your machine:
+ - [Dejavu Fonts](https://sourceforge.net/projects/dejavu/files/dejavu/2.37/dejavu-fonts-ttf-2.37.tar.bz2/download)
+
+Alternatively, download:
+
- [Quivira.ttf](http://www.quivira-font.com/files/Quivira.ttf)
- - [Dejavu Fonts](http://sourceforge.net/projects/dejavu/files/dejavu/2.35/dejavu-fonts-ttf-2.35.tar.bz2)
- [NotoSans](https://github.com/googlei18n/noto-fonts/blob/master/hinted/NotoSans-Regular.ttc?raw=true)
- [NotoSansSymbols](https://github.com/googlei18n/noto-fonts/blob/master/unhinted/NotoSansSymbols-Regular.ttf?raw=true)
@@ -245,7 +205,7 @@ Then, have the following lines in your emacs setup to use `DejaVu Sans Mono` fon
(set-face-attribute 'default nil :font "DejaVu Sans Mono-11"))
```
-You may also need to install [emacs-unicode-fonts](https://github.com/rolandwalker/unicode-fonts) package.
+Also install [emacs-unicode-fonts](https://github.com/rolandwalker/unicode-fonts) package.
- Run `M-x package-refresh-contents`, `M-x package-install`, and type `unicode-fonts`.
- Add the following lines in your emacs setup:
@@ -255,6 +215,57 @@ You may also need to install [emacs-unicode-fonts](https://github.com/rolandwalk
(unicode-fonts-setup)
```
+
+Installing packages manually
+----------------------------
+
+If you want to install the packages manually, you can use M-x package-install to install the following packages:
+
+ - [dash][dash]
+ - [dash-functional][dash]
+ - [f][f]
+ - [s][s]
+
+[emacs24]: http://www.gnu.org/software/emacs
+[dash]: https://github.com/magnars/dash.el
+[f]: https://github.com/rejeep/f.el
+[s]: https://github.com/magnars/s.el
+
+The following packages are optional, but strongly recommended.
+
+ - [company][company]
+ - [flycheck][flycheck]
+ - [fill-column-indicator][fci]
+
+Both the optional and required packages will be installed for you
+automatically the first time you use ``lean-mode``, if you follow the
+installation instructions below.
+
+[company]: http://company-mode.github.io/
+[flycheck]: http://www.flycheck.org/manual/latest/index.html
+[fci]: https://github.com/alpaker/Fill-Column-Indicator
+
+Init file
+---------
+
+The init file can be found in different places on different systems:
+
+- Emacs will check for a file named ``.emacs`` in your home directory.
+- With GNU Emacs, it is common to use ``.emacs.d/init.el`` instead.
+- With Aquamacs, it is common to use ``~/Library/Preferences/Aquamacs Emacs/Preferences.el``.
+
+On Windows, there are two additional complications:
+
+- It may be hard to figure out what Emacs considers to be your "home
+ directory".
+- The file explorer may not let you create a file named ``.emacs``,
+ since it begins with a period.
+
+One solution is to run Emacs itself and create the file using C-c C-f
+(control-C, control-F) and then entering ``~/.emacs``. (The tilde
+indicates your home directory.) On Windows, you can also name the file
+``_emacs``.
+
Contributions
=============