initial commit

.devcontainer/Dockerfile

@@ -0,0 +1,9 @@
+ARG VARIANT="jammy"
+FROM mcr.microsoft.com/vscode/devcontainers/base:0-${VARIANT}
+
+RUN apt-get update && apt-get install -yq build-essential nodejs npm
+
+USER vscode
+RUN echo $HOME
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSfL | sh -s -- --default-toolchain leanprover/lean4:stable -y
+RUN echo 'export PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.profile

.devcontainer/devcontainer.json

@@ -0,0 +1,18 @@
+{
+	"name": "Ubuntu",
+	"build": {
+		"dockerfile": "Dockerfile",
+		"args": { "VARIANT": "ubuntu-22.04" }
+	},
+	"remoteUser": "vscode",
+	"features": {
+		"git": "os-provided"
+	},
+	"customizations": {
+		"vscode": {
+			"extensions": [
+				"leanprover.lean4"
+			]
+		}
+	}
+}

.gitignore

@@ -0,0 +1,3 @@
+/build
+/lakefile.olean
+/lake-packages/*

Main.lean

@@ -0,0 +1,6 @@
+import Prova 
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
+
+#eval main

Prova.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Prova` library.
+-- Import modules here that should be built as part of the library.
+import Prova.Basic

Prova/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

README.md

@@ -0,0 +1,8 @@
+# Lean Codespace
+
+Progetto ricavato dalla repo: <https://github.com/leanprover/lean4-samples>
+
+## GitHub Pro con Unipi
+
+[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=452801263&machine=standardLinux32gb&location=WestEurope)
+

lakefile.lean

@@ -0,0 +1,16 @@
+import Lake
+open Lake DSL
+
+package prova where
+  -- add package configuration options here
+
+lean_lib Prova where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «prova» where
+  root := `Main
+  -- Enables the use of the Lean interpreter by the executable (e.g.,
+  -- `runFrontend`) at the expense of increased binary size on Linux.
+  -- Remove this line if you do not need such functionality.
+  supportInterpreter := true

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:stable