Questa repo contiene un semplice progetto in Lean con preimpostato un ambiente GitHub CodeSpace per poterlo usare senza dover installare nulla in locale.
Questa repo contiene un semplice progetto in Lean che può essere lanciato con un click su GitHub CodeSpace provarlo senza dover installare nulla in locale.
## GitHub / GitHub Pro con Unipi
## GitHub / GitHub Pro con Unipi
@ -8,7 +8,11 @@ GitHub già offre 120h gratuite al mese di utilizzo di CodeSpace, inoltre [Unipi
[](https://github.com/codespaces/new?skip_quickstart=true&hide_repo_select=true&ref=main&repo=698191991&machine=standardLinux32gb&location=WestEurope)
[](https://github.com/codespaces/new?skip_quickstart=true&hide_repo_select=true&ref=main&repo=698191991&machine=standardLinux32gb&location=WestEurope)
> :warning: **Achtung** :warning: Per non sprecare subito tutte le ore di utilizzo quando si ha finito di utilizzare il CodeSpace ricordarsi di spegnerlo dalla pagina <https://github.com/codespaces>, dalla lista di CodeSpaces se c'è scritto ancora **"Active"** premere sui tre puntini e fare **"Stop Container"**.
> :warning: **Achtung** :warning:
>
> - Le 120h o 180h sono "core hours" quindi con la macchina da 2 core sono complessivamente 60h o 90h effettive al mese (le opzioni sono 2 o 4 core ma già quella da 2 dovrebbe bastare). Essenzialmente conviene usare con parsimonia le ore di questi GitHub CodeSpaces.
>
> - In particolare quando si ha finito di utilizzare il codespace ricordarsi di spegnerlo dalla pagina <https://github.com/codespaces>, dalla lista di codespaces se c'è scritto ancora **"Active"** premere sui tre puntini e fare **"Stop Container"**.
Per provare che tutto funzioni andare in `./Main.lean` e verificare che si apra il pannello laterale e che mettendo il mouse sopra `#eval` venga mostrata la stringa `Hello, World!`.
Per provare che tutto funzioni andare in `./Main.lean` e verificare che si apra il pannello laterale e che mettendo il mouse sopra `#eval` venga mostrata la stringa `Hello, World!`.
