<commit_before>[![Build Status](https://travis-ci.org/leanprover/tutorial.svg?branch=master)](https://travis-ci.org/leanprover/tutorial)

Lean Tutorial
=============

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


How to Build
------------

We use [cask][cask] to install emacs dependencies ([org-mode][org-mode], [lean-mode][lean-mode], [htmlize][htmlize]) and [pygments][pygments] and [minted][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
```

[cask]: https://github.com/cask/cask
[org-mode]: http://orgmode.org/
[lean-mode]: https://github.com/leanprover/lean/tree/master/src/emacs
[htmlize]: https://github.com/emacsmirror/htmlize
[pygments]: http://pygments.org/<commit_msg>adding a warning that this is the tutorial for the HoTT snapshot<commit_after>[![Build Status](https://travis-ci.org/leanprover/tutorial.svg?branch=master)](https://travis-ci.org/leanprover/tutorial)

Lean Tutorial
=============

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

Please note that this is the tutorial for the snapshot of Lean which allows the use of homotopy type theory. It is /not/ the [[https://github.com/leanprover/introduction_to_lean][tutorial]] for the [[https://github.com/leanprover/lean][active development branch]].

How to Build
------------

We use [cask][cask] to install emacs dependencies ([org-mode][org-mode], [lean-mode][lean-mode], [htmlize][htmlize]) and [pygments][pygments] and [minted][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
```

[cask]: https://github.com/cask/cask
[org-mode]: http://orgmode.org/
[lean-mode]: https://github.com/leanprover/lean/tree/master/src/emacs
[htmlize]: https://github.com/emacsmirror/htmlize
[pygments]: http://pygments.org/
{'fraction_non_alphanumeric': 0.14046822742474915, 'fraction_numerical': 0.0046822742474916385, 'mean_word_length': 3.717665615141956, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 18, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2507751', 'n_tokens_mistral': 1004, 'n_tokens_neox': 966, 'n_words': 240}