From e2c66fffcaa1bbde97c85f4a1c612bcb149d0660 Mon Sep 17 00:00:00 2001
From: Antonio De Lucreziis <antonio.delucreziis@gmail.com>
Date: Fri, 29 Sep 2023 19:21:53 +0200
Subject: [PATCH 1/2] mathlib support experiment

---
 .devcontainer/devcontainer.json |  6 +++-
 Prova/MathlibExample.lean       |  3 ++
 lake-manifest.json              | 52 +++++++++++++++++++++++++++++++++
 lakefile.lean                   |  3 ++
 4 files changed, 63 insertions(+), 1 deletion(-)
 create mode 100644 Prova/MathlibExample.lean
 create mode 100644 lake-manifest.json

diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
index 66c9583..ff2fbb6 100644
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -14,5 +14,9 @@
 				"leanprover.lean4"
 			]
 		}
-	}
+	},
+	"postCreateCommand": [
+		"lake update",
+		"lake exe cache get"
+	]
 }
diff --git a/Prova/MathlibExample.lean b/Prova/MathlibExample.lean
new file mode 100644
index 0000000..0849845
--- /dev/null
+++ b/Prova/MathlibExample.lean
@@ -0,0 +1,3 @@
+import Mathlib.Topology.Basic
+
+#check TopologicalSpace
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..c64c97f
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,52 @@
+{"version": 6,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "071f47d27115f6b801ba2e4ba42334817abf2446",
+    "opts": {},
+    "name": "mathlib",
+    "inputRev?": null,
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "opts": {},
+    "name": "Qq",
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "4f8b397237411249930791f1cba0a9d2880a02dd",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/mhuisi/lean4-cli.git",
+    "subDir?": null,
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/EdAyers/ProofWidgets4",
+    "subDir?": null,
+    "rev": "9f68f14df384f43b74aeb2908b97ae54a0ad9d95",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.17",
+    "inherited": true}}],
+ "name": "prova"}
diff --git a/lakefile.lean b/lakefile.lean
index 92e2815..3ffec2a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,6 +7,9 @@ package prova where
 lean_lib Prova where
   -- add library configuration options here
 
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
+    
 @[default_target]
 lean_exe «prova» where
   root := `Main

From 98733eaae82e91087c4f16b405f1445f08b735bd Mon Sep 17 00:00:00 2001
From: Antonio De Lucreziis <antonio.delucreziis@gmail.com>
Date: Fri, 29 Sep 2023 19:46:01 +0200
Subject: [PATCH 2/2] updated readme to tell about mathlib support

---
 README.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index dd611cd..3332525 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # Lean Codespace
 
-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.
+Questa repo contiene un semplice progetto in Lean con Mathlib che può essere lanciato con un click su GitHub CodeSpace provarlo senza dover installare nulla in locale.
 
 ## GitHub / GitHub Pro con Unipi
 
@@ -10,11 +10,11 @@ GitHub già offre 120h gratuite al mese di utilizzo di CodeSpace, inoltre [Unipi
 
 > :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.
+> - Le 120h o 180h sono "core hours" quindi con la macchina da 2 core sono complessivamente 60h o 90h effettive al mese (per far compilare tutto più velocemnte all'inizio conviene usare quella da 4 core ma poi si può passare a quella da 2). 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 `./Prova/MathlibExample.lean` e verificare che si apra il pannello laterale e che mettendo il mouse sopra `#check TopologicalSpace` venga mostrata la stringa `TopologicalSpace.{u} (α : Type u) : Type u` (all'inizio vengono compilate molte cose quindi potrebbe comparire per qualche minuto un underline blue sotto il primo import)
 
 ## Siti Utili