Theorem Proving in Lean

• Web : https://leanprover.github.io/theorem_proving_in_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/theorem_proving_in_lean
cd theorem_proving_in_lean
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:

$ python -m SimpleHTTPServer

The above command starts a HTTP server at theorem_proving_in_lean 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

1. Using Lean.JS:

   make test_js