aziis98
/
lean-codespace
mirror of https://github.com/aziis98/lean-codespace
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
Questa repository contiene un semplice progetto in Lean che può essere lanciato con un click su GitHub CodeSpaces
You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
15 Commits
1 Branch
0 Tags
43 KiB
Lean 68.3%
Dockerfile 31.7%
 
 
main
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '611e6bc751'
${ noResults }
Go to file
Antonio De Lucreziis 611e6bc751
updated the readme 		1 year ago
.devcontainer initial commit 1 year ago
Prova initial commit 1 year ago
.gitignore initial commit 1 year ago
Main.lean ehm fix 1 year ago
Prova.lean initial commit 1 year ago
README.md updated the readme 1 year ago
lakefile.lean initial commit 1 year ago
lean-toolchain initial commit 1 year ago

README.md

Lean Codespace

Questa repo contiene un semplice progetto in Lean che può essere lanciato con un click su GitHub CodeSpaces (ambiente di sviluppo nel cloud dal browser) provarlo senza dover installare nulla in locale.

GitHub / GitHub Pro con Unipi

GitHub già offre 120h gratuite al mese di utilizzo di CodeSpaces, inoltre Unipi con GitHub Pro ci fa arrivare a 180h gratuite di utilizzo al mese.

Open in GitHub Codespaces

⚠️ Achtung ⚠️

  • 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!.

Siti Utili