CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutSign UpSign In

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

| Download

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

Project: Xena
Views: 18536
License: APACHE
Tweet
Share
Share

Controlled installation of Lean and mathlib on Debian/Ubuntu

This document explains a more controlled installation procedure for Lean and mathlib on Linux distributions derived from Debian (Debian itself, Ubuntu, LMDE,...). There is a quicker way described in the main install page but it requires more trust. Of course you can get even more details about what is going on by reading the bash scripts that will be downloaded below: elan_init and remote-install-update-mathlib. All commands below should be typed inside a terminal.

  • Lean itself doesn't depend on much infrastructure, but supporting tools needed by most users require git, curl, and python. So the first step is:

    sudo apt install git curl python3 python3-pip

  • There are two editors you can use with Lean, VS Code and emacs. The recommended choice is Visual Studio Code.

    wget -O code.deb https://go.microsoft.com/fwlink/?LinkID=760868
sudo apt install ./code.deb
rm code.deb
code --install-extension jroesch.lean

    Now open VS Code, and verify Lean is working, for example by saving a file test.lean and entering #eval 1+1. A green line should appear underneath #eval 1+1, and hovering the mouse over it you should see 2 displayed.

    The alternative is to use Emacs, and its lean-mode.

    Everything else will be installed in user-space (no sudo required).

  • The next step installs a small tool called elan which will handle updating Lean according to the needs of your current project (hit Enter when a question is asked). It will live in $HOME/.elan and add a line to $HOME/.profile.

    curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh

  • Then we install a small tool called update-mathlib that which will handle updating mathlib according to the needs of your current project. It will live in $HOME/.mathlib and add a line to $HOME/.profile.

    curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash

You can now read instructions about creating and working on Lean projects