Taller de Lean 4

Repositori del Taller de Lean 4 impartit a la Facultat de Ciències Matemàtiques de la Universitat de València.

Com treballar amb aquest repositori

Per a treballar amb aquest repositori recomanem utilitzar l'editor Visual Studio Code amb les extensions recomanades per a Lean 4:

• lean4
• Paperproof

Aquestes i altres extensions estan incloses en el fitxer de recomanacions d'extensions de Visual Studio Code que es pot trobar a la carpeta .vscode d'aquest repositori.

La instal·lació de Lean 4 es pot fer automaticament amb la propia extensió de Lean 4, però també es pot fer manualment seguint les instruccions de la web de Lean 4.

Podeu trobar altres requirements i detalls al blog del Taller de Lean 4.

Entorn de Lean i altres requeriments

Per tal d'activar l'entorn de treball, només cal executar la següent comanda en la terminal:

lake update # <- Per baixar i actualitzar les dependències
lake build # <- Per compilar el nostre i codi i poder accedir a ell

Si treballeu amb Visual Studio Code, és possible que aparega un pop-up que indica que és necessari fer un rebuild de les dependències. Feu click al botó de Rebuild per a fer-ho.

Flux de treball

Una idea per a treballar a les sessions amb el codi actualitzat del repositori és, en primer lloc, clonar el repositori:

git clone https://github.com/encosllo/TallerLean4

A continuació, cal obrir un terminal a la carpeta del repositori i crear una branca local nova amb el vostre nom:

git branch <nom> # <- Crear la branca
git switch <nom> # <- Canviar a la branca

Ara ja podeu treballar a la branca local i fer els vostres commits, preferiblement en fitxers diferents als que ja estan en el repositori per tal de no tindre conflictes amb actualitzacions futures.

Quan vulgueu actualitzar el vostre repositori amb les actualitzacions del repositori remot, podeu fer un rebase de la branca remota main:

git rebase origin/main

Inicialització

Clonem el repositori

git clone https://github.com/encosllo/TallerLean4

A continuació actualitzem el sistema

lake exe cache get

Recordeu obrir la carpeta on esteu treballant al Visual Studio Code.