bump mathlib

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
-    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
+    "rev": "65bba7286e2395f3163fd0277110578f19b8170f",
     "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.13",
+    "inputRev?": "v0.0.16",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
@@ -20,10 +20,10 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "7d308680dc444730e84a86c72357ad9a7aea9c4b",
+    "rev": "f203f2e0caf1d9ea25b7f2e4b8c2afebd2c6967b",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "7d308680dc444730e84a86c72357ad9a7aea9c4b",
+    "inputRev?": "v4.1.0",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
@@ -44,15 +44,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean4game.git",
     "subDir?": "server",
-    "rev": "6970f10e30f70ecede1042201e9bd1d838ad1934",
+    "rev": "cc4321ff3f7cbf43747114cd56197a1b2bb0c457",
     "opts": {},
     "name": "GameServer",
-    "inputRev?": "6970f10e30f70ecede1042201e9bd1d838ad1934",
+    "inputRev?": "main",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "e8c27f7d90ee71470558efd1bc197fe55068c748",
+    "rev": "67855403d60daf181775fa1ec63b04e70bcc3921",
     "opts": {},
     "name": "std",
     "inputRev?": "main",

lakefile.lean

@@ -19,19 +19,17 @@ open Lean in
   modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
    : Elab.Command.CommandElabM Unit)
 
--- require mathlib from git
---   "https://github.com/leanprover-community/mathlib4" @ "88e129706828e01b7622d6635af1ca6667e25bac"
-
--- `Game` fix:
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4" @ "7d308680dc444730e84a86c72357ad9a7aea9c4b"
+  "https://github.com/leanprover-community/mathlib4" @ "v4.1.0"
 
 -- NOTE: We abuse the `trace.debug` option to toggle messages in VSCode on and
 -- off when calling `lake build`. Ideally there would be a better way using `logInfo` and
 -- an option like `lean4game.verbose`.
 package Game where
-  moreLeanArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=false", "-Dtrace.debug=false"]
-  moreServerArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=true", "-Dtrace.debug=true"]
+  moreLeanArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=false",
+    "-Dtrace.debug=false"]
+  moreServerArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=true",
+    "-Dtrace.debug=true"]
   weakLeanArgs := #[]
 
 @[default_target]