bump mathlib-demo and add a lean-option

Author: joneugster

Projects/mathlib-demo/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0ae30b68e680199367b2d4de739cbfdd6032b480",
+   "rev": "37f686cf27093bcbde5a9eb2f1519ef730de1828",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a",
+   "rev": "4dfba8b20a5ce570b9ef8bae969dd163782f9793",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d",
+   "rev": "8d29bc2c3ebe1f863c2f02df816b4f3dd1b65226",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "08372f1ec11df288ff76621ead7b0b575cb29355",
+   "rev": "c20832d6f0b3186a97ea9361cec0a5b87dd152a3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
+   "rev": "ea953247aac573c9b5adea60bacd3e085f58aca4",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.53",
+   "inputRev": "v0.0.56",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ec060e0e10c685be8af65f288e23d026c9fde245",
+   "rev": "57185dfad68d78356f9462af984882d6f262aa5d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
+   "rev": "aa4c87abed970d9dfad2506000d99d30b02f476b",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,17 +75,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b8e143008dc1e5f28f48a8aa8de63deaf4fe8068",
+   "rev": "c509e875522185203ad651695f27ab05a0109158",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
+   "rev": "aff4176e5c41737a0d73be74ad9feb6a889bfa98",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

Projects/mathlib-demo/lakefile.toml

@@ -1,6 +1,9 @@
 name = "mathlibLatest"
 defaultTargets = ["MathlibLatest"]
 
+[leanOptions]
+pp.unicode.fun = true
+
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"

Projects/mathlib-demo/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.18.0-rc1
+leanprover/lean4:v4.19.0-rc2

Projects/mathlib-demo/mathlib-demo.lean

@@ -0,0 +1,3 @@
+-- The Lean server and vscode-lean4 have several bugs when there isn't actually a
+-- physical file on the disk which the editor opened.
+-- As a workaround we add this dummy file, but ideally this could be fixed in core.