mathlib support experiment

.devcontainer/devcontainer.json

@@ -14,5 +14,9 @@
 				"leanprover.lean4"
 			]
 		}
-	}
+	},
+	"postCreateCommand": [
+		"lake update",
+		"lake exe cache get"
+	]
 }

Prova/MathlibExample.lean

@@ -0,0 +1,3 @@
+import Mathlib.Topology.Basic
+
+#check TopologicalSpace

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"}

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