Com començar a desenvolupar en Lean4?

Hi ha moltes maneres d’usar Lean4 i estan molt ben documentades a la web. Tot i així, jo el que trobo més senzill és:

Usar l’extensió de Lean4 de VSCode (disclaimer: no m’agrada especialment VSCode. He provat VSCodium i em va donar algun problema). També vaig intentar el NeoVim, que m’agrada més, però no me’n surto.
Seguir totes les passes de configuració
Clicar a la icona \(\forall\) que apareix a dalt a la dreta i a “create standalone project using mathlib”. Deixar que es descarregui tots els fitxers
Per exemple, si el nom és Pati ens crearà una carpeta amb la següent estructura:

├── lakefile.toml
├── lake-manifest.json
├── lean-toolchain
├── Pati
│   └── Basic.lean
├── Pati.lean
└── README.md

Anem afegint els fitxers que volem anar treallant a la carpeta Pati/
Quan els vulguem incoporporar al projecte, els afegim a Pati.lean, que és un fitxer que conté senzillament

import Pati.Basic

Atencio! Cada cop que inicialitzem un projecte com aquest es creen tots els fitxers necessaris per a la compilació de tota la llibreria. Per tant, és millor tenir pocs projectes amb motls fitxers diferents que no pas molts projectes de pocs fitxers.

Exemple: afegir un exemple

Per exemple, podem mirar d’incorporar l’exemple de live-lean.org de les propietats dels anells:

https://live.lean-lang.org/#url=https%3A%2F%2Flive.lean-lang.org%2Fapi%2Fexample%2FMathlibDemo%2FMathlibDemo%2FRing.lean


import Mathlib.Tactic.Ring -- import the `ring` tactic

-- let R be a commutative ring (for example the real numbers)
variable (R : Type) [CommRing R]

-- let x and y be elements of R
variable (x y : R)

-- then (x+y)*(x+2y)=x^2+3xy+2y^2

example : (x+y)*(x+2*y)=x^2+3*x*y+2*y^2 := by
  -- the `ring` tactic solves this goal automatically
  ring

Un cop a la infoview de la dreta de l’editor ens digui que està tot ok:

el podem donar per bo. Si volem que el projecte global el tingui en compte podem afegir una línia al fitxer arrel Pati.lean:

import Pati.Basic
/- Aqui els fitxers que tenim validats-/
import Pati.Example_live_lean_ring

És possible que ens digui que cal reiniciar el fitxer.

Bonus: sincronitzar el teu codi a un repositori

Tot i que per a la majoria de qüestions uso una solució al núvol per sincronitzar (com Nextcloud), per al codi i per a projectes en Lean4 en particular, uso un repositori en git, el més conegut dels quals és github, que pertany a Microsoft. A mi m’agrada molt més Codeberg que és un servei gratuït gestionat per una fundació sense ànim de lucre amb seu a Alemània.

Si ens fixem, quan hem creat un projecte, ens ha creat també uns fitxers ocults que es diuen .gitignore de carpetes que no es sincronitzaran. Com que la carpeta .lake, que és a on es guarda la nostra versió de lean4 amb les llibreries de mathlib, ocupa diverses gigues, no el podem ni l’hem de sincronitzar.

També hi ha una carpeta oculta anomenada .git on hi ha la configuració del repositori. Cal afegir una línia al fitxer .git/config que digui

[remote "origin"]
    url = https://codeberg.org/joaquimpuig/python-letitshine.git
    fetch = +refs/heads/*:refs/remotes/origin/*

El fitxer README.md s’ha de canviar perquè conté les configuracions per tenir accions del github, cosa que de moment, no uso.