Instalación del Lean Theorem Prover

1 Instalación

Instalación según Controlled installation of Lean and mathlib on Debian/Ubuntu

Cambiar a tmp
```
cd /tmp
```

Instalar git, curl, and python

sudo apt install git curl python3 python3-pip

El resultado es

curl ya está en su versión más reciente (7.68.0-1ubuntu2).
git ya está en su versión más reciente (1:2.25.1-1ubuntu3).
python3 ya está en su versión más reciente (3.8.2-0ubuntu2).
python3-pip ya está en su versión más reciente (20.0.2-5ubuntu1).

Instalar elan

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

El resultado es

tmp> curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
info: downloading installer

Welcome to Lean!

This will download and install Elan, a tool for managing different Lean 
versions used in packages you create or download. It will also install a 
default version of Lean and its package manager, leanpkg, for editing files not
belonging to any package.

It will add the leanpkg, lean, and elan commands to Elan's bin directory, 
located at:

  /home/jalonso/.elan/bin

This path will then be added to your PATH environment variable by modifying the
profile file located at:

  /home/jalonso/.profile

You can uninstall at any time with elan self uninstall and these changes will 
be reverted.

Current installation options:

     default toolchain: stable
  modify PATH variable: yes

1) Proceed with installation (default)
2) Customize installation
3) Cancel installation
1

info: updating existing elan installation


Elan is installed now. Great!

To get started you need Elan's bin directory ($HOME/.elan/bin) in your PATH 
environment variable. Next time you log in this will be done automatically.

To configure your current shell run source $HOME/.elan/env
tmp> source $HOME/.elan/env

Instalar con list-packages
- lean-mode
- company-lean
- yasnippet-lean
Instalar leanproject
```
sudo pip3 install mathlibtools
```

El resultado es

tmp> sudo pip3 install mathlibtools
Requirement already satisfied: mathlibtools in /usr/local/lib/python3.8/dist-packages (0.0.8)
Requirement already satisfied: PyGithub in /usr/local/lib/python3.8/dist-packages (from mathlibtools) (1.51)
Requirement already satisfied: networkx in /usr/local/lib/python3.8/dist-packages (from mathlibtools) (2.4)
Requirement already satisfied: Click in /usr/lib/python3/dist-packages (from mathlibtools) (7.0)
Requirement already satisfied: paramiko>=2.7.0 in /usr/local/lib/python3.8/dist-packages (from mathlibtools) (2.7.1)
Requirement already satisfied: pydot in /usr/local/lib/python3.8/dist-packages (from mathlibtools) (1.4.1)
Requirement already satisfied: toml>=0.10.0 in /usr/local/lib/python3.8/dist-packages (from mathlibtools) (0.10.1)
Requirement already satisfied: gitpython>=2.1.11 in /usr/local/lib/python3.8/dist-packages (from mathlibtools) (3.1.3)
Requirement already satisfied: requests in /usr/lib/python3/dist-packages (from mathlibtools) (2.22.0)
Requirement already satisfied: certifi in /usr/lib/python3/dist-packages (from mathlibtools) (2019.11.28)
Requirement already satisfied: tqdm in /usr/local/lib/python3.8/dist-packages (from mathlibtools) (4.46.1)
Requirement already satisfied: deprecated in /usr/local/lib/python3.8/dist-packages (from PyGithub->mathlibtools) (1.2.10)
Requirement already satisfied: pyjwt in /usr/lib/python3/dist-packages (from PyGithub->mathlibtools) (1.7.1)
Requirement already satisfied: decorator>=4.3.0 in /usr/local/lib/python3.8/dist-packages (from networkx->mathlibtools) (4.4.2)
Requirement already satisfied: pynacl>=1.0.1 in /usr/lib/python3/dist-packages (from paramiko>=2.7.0->mathlibtools) (1.3.0)
Requirement already satisfied: cryptography>=2.5 in /usr/lib/python3/dist-packages (from paramiko>=2.7.0->mathlibtools) (2.8)
Requirement already satisfied: bcrypt>=3.1.3 in /usr/lib/python3/dist-packages (from paramiko>=2.7.0->mathlibtools) (3.1.7)
Requirement already satisfied: pyparsing>=2.1.4 in /usr/lib/python3/dist-packages (from pydot->mathlibtools) (2.4.6)
Requirement already satisfied: gitdb<5,>=4.0.1 in /usr/local/lib/python3.8/dist-packages (from gitpython>=2.1.11->mathlibtools) (4.0.5)
Requirement already satisfied: wrapt<2,>=1.10 in /usr/local/lib/python3.8/dist-packages (from deprecated->PyGithub->mathlibtools) (1.12.1)
Requirement already satisfied: smmap<4,>=3.0.1 in /usr/local/lib/python3.8/dist-packages (from gitdb<5,>=4.0.1->gitpython>=2.1.11->mathlibtools) (3.0.4)

2 Prueba con proyectos

2.1 Prueba con un nuevo proyecto

Crear mi_proyecto
```
leanproject new mi_proyecto
```

El resultado es

tmp> leanproject new mi_proyecto
> cd mi_projecto
> git init -q
> git checkout -b lean-3.15.0
Cambiado a nueva rama 'lean-3.15.0'
configuring mi_projecto 0.1
Adding mathlib
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Clonando en '_target/deps/mathlib'...
remote: Enumerating objects: 29, done.        
remote: Counting objects: 100% (29/29), done.        
remote: Compressing objects: 100% (27/27), done.        
remote: Total 51787 (delta 12), reused 5 (delta 2), pack-reused 51758        
Recibiendo objetos: 100% (51787/51787), 22.31 MiB | 6.49 MiB/s, listo.
Resolviendo deltas: 100% (40014/40014), listo.
> git checkout --detach d9934b2681b12b9b5558b6913f80c037e1be7a9a    # in directory _target/deps/mathlib
HEAD está ahora en d9934b26 feat(linear_algebra/basic): curry is linear_equiv (#3012)
configuring mi_projecto 0.1
mathlib: trying to update _target/deps/mathlib to revision d9934b2681b12b9b5558b6913f80c037e1be7a9a
> git checkout --detach d9934b2681b12b9b5558b6913f80c037e1be7a9a    # in directory _target/deps/mathlib
HEAD está ahora en d9934b26 feat(linear_algebra/basic): curry is linear_equiv (#3012)
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/d9934b2681b12b9b5558b6913f80c037e1be7a9a.tar.xz to /home/jalonso/.mathlib/d9934b2681b12b9b5558b6913f80c037e1be7a9a.tar.xz
100% | 22.6M/22.6M [00:04<00:00, 5.32MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/

Cambiar a mi_proyecto/src
```
cd mi_proyecto/src
```

Crear el fichero test.lean con el siguiente contenido

import topology.basic

#check topological_space

Activar la ventana Lean Goal pulsando C-c C-g
Colocar el cursor sobre check y comprobar que sale el mensaje
```
topological_space : Type u_1 → Type u_1 
```
Obtener la documentación colocando el cursor sobre topological_space y pulsando M-.

2.2 Prueba con proyectos existentes

Cambiar a tmp
```
cd /tmp
```
Importar el proyecto tutorials
```
leanproject get tutorials
```

El resultado es

tmp> leanproject get tutorials
Cloning from git@github.com:leanprover-community/tutorials.git
configuring tuto 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Clonando en '_target/deps/mathlib'...
remote: Enumerating objects: 32, done.        
remote: Counting objects: 100% (32/32), done.        
remote: Compressing objects: 100% (29/29), done.        
remote: Total 51790 (delta 13), reused 7 (delta 3), pack-reused 51758        
Recibiendo objetos: 100% (51790/51790), 22.31 MiB | 9.31 MiB/s, listo.
Resolviendo deltas: 100% (40015/40015), listo.
> git checkout --detach e48c2af4f2f92c2331a912c588610db73085939d    # in directory _target/deps/mathlib
HEAD está ahora en e48c2af4 feat(data/padics/padic_norm): New padic_val_nat convenience functions (#2970)
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/e48c2af4f2f92c2331a912c588610db73085939d.tar.xz to /home/jalonso/.mathlib/e48c2af4f2f92c2331a912c588610db73085939d.tar.xz
100% 22.4M/22.4M [00:01<00:00, 16.2MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/