Lean Tutorial

• Web : https://leanprover.github.io/tutorial
• PDF : https://leanprover.github.io/tutorial/tutorial.pdf

Please note that this is the tutorial for Lean 2, which allows the use of homotopy type theory (HoTT). It is /not/ the tutorial for the current version of Lean.

How to Build

We use cask to install emacs dependencies (org-mode, lean-mode, htmlize) and pygments and minted to syntax-highlight Lean code in LaTeX. We assume that you already have emacs-24.3 or higher installed in your system.

sudo apt-get install mercurial python2.7 texlive-latex-recommended \
                     texlive-humanities texlive-xetex texlive-science \
                     texlive-latex-extra texlive-fonts-recommended texlive-luatex\
                     bibtex2html git make mercurial autoconf automake gcc curl
git clone https://github.com/leanprover/tutorial
cd tutorial
tar xvfz header/l3kernel.tar.gz -C ~/
make install-cask # after this, you need to add the cask binary to your $PATH
make install-pygments  
make

Automatic Build using Watchman

Using watchman, we can detect any changes on the org-files, and trigger re-builds automatically on the background.

To install watchman:

sudo apt-get install automake
make install-watchman

To enable watch:

make watch-on

To disable watch:

make watch-off

How to preview generated HTML files

It requires a webserver to preview generated HTML files. We can use Python's SimpleHTTPServer module:

tutorial $ python -m SimpleHTTPServer

The above command starts a HTTP server at tutorial directory (default port: 8000). For example, 01_Introduction.html is available at http://localhost:8000/01_Introduction.html.

Auto-reload HTML page

• Firefox: Auto Reload add-on

  • Tools > AutoReload Preferences
  • Create Reload Rule
  • Link .html in the filesystem

• Chrome: Tincr (does not work on Linux)

  • Right-click and choose "Inspect Element"
  • Go to "tincr" tab, choose "Http Web Server" for project type, then select Root directory.

Test Lean Code in .org files

1. Using Native Lean: First, you need to install Lean. Please follow the instructions at the download page. You can test all Lean code blocks in *.org files by executing the following command:

make test ```

To use a specific binary of Lean in test, please do the following: bash LEAN_BIN=/path/to/your/lean make test

2. Using Lean.JS:

make test_js
```