From 0de635a6c9b531f7536065b4abeb947ff60b6c78 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 24 May 2017 20:38:05 -0400 Subject: [PATCH] doc(ubuntu/emacs): update installation instructions --- doc/make/ubuntu-12.04-detailed.md | 4 ++-- src/emacs/README.md | 18 +++++++++--------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/doc/make/ubuntu-12.04-detailed.md b/doc/make/ubuntu-12.04-detailed.md index 26661a786..914aba322 100644 --- a/doc/make/ubuntu-12.04-detailed.md +++ b/doc/make/ubuntu-12.04-detailed.md @@ -56,7 +56,7 @@ Preparing working environment on Ubuntu 12.04 cmake -D CMAKE_BUILD_TYPE=Release -D BOOST=ON ../src make -### If you are using Emacs, here are some basic configurations +### If you are using Emacs, here are some basic configurations (optional) (custom-set-variables '(c-basic-offset 4) @@ -88,4 +88,4 @@ Preparing working environment on Ubuntu 12.04 ("\\<\\(constexpr\\)\\>" . font-lock-keyword-face) )) -You need to also set up the [Emacs Mode](../../src/emacs/README.md). +### 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 ee7ffccd1..351cb3085 100644 --- a/src/emacs/README.md +++ b/src/emacs/README.md @@ -19,8 +19,7 @@ packages, which can be installed via M-x package-install. [f]: https://github.com/rejeep/f.el [s]: https://github.com/magnars/s.el -The following packages are *optional*, but we recommend installing them -to use full features of ``lean-mode``. +The following packages are optional, but strongly recommended. - [company][company] - [flycheck][flycheck] @@ -46,7 +45,7 @@ found in different places on different systems: - 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: +On Windows, there are two additional complications: - It may be hard to figure out what Emacs considers to be your "home directory". @@ -57,7 +56,7 @@ 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: ```elisp @@ -81,15 +80,16 @@ Put the following code in your Emacs init file: (package-install p)))) ``` -Then choose your installation method from the following scenarios, and -add the corresponding code to your init file: +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/lean") ;; <=== YOU NEED TO MODIFY THIS +(setq lean-rootdir "~/projects/lean2") ;; <=== YOU NEED TO MODIFY THIS (setq-local lean-emacs-path (concat (file-name-as-directory lean-rootdir) (file-name-as-directory "src") @@ -149,7 +149,7 @@ 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 +you type, an asterisk should briefly appear after ``FlyC``, indicating that your file is being checked. @@ -177,7 +177,7 @@ Key Bindings and Commands The Flycheck annotation `FlyC:n/n` indicates the number of errors / responses from Lean. An asterisk `*FlyC:n/n` indicates that checking is in progress. Clicking on `FlyC` opens the Flycheck menu. -To profile Lean performace on the file in the buffer, enter M-x lean-execute or choose +To profile Lean performace on the file in the buffer, enter M-x lean-execute or choose `Lean execute` from the Lean menu, and add the option `--profile`.