bump to v4.4.0

hhu-adam · Dec 25, 2023 · 66d1ddb · 66d1ddb
1 parent b3a2a10
commit 66d1ddb
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 13 deletions.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,25 +4,25 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
+   "rev": "af7f36db6e7e9e395710a70635f915e8e3a0e69b",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
+   "inputRev": "v4.4.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean4game.git",
    "type": "git",
    "subDir": "server",
-   "rev": "d5697d052e5154b909f379073a591ebf66eb3e22",
+   "rev": "8cdac88b5adab9cd77d737bc3a0e64e965ca08cd",
    "name": "GameServer",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
+   "inputRev": "v4.4.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
+   "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,7 +31,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1",
+   "rev": "646be3a3604d0f2a3c1800cb4279a36493474b18",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -58,10 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d",
+   "rev": "cf8e23a62939ed7cc530fbb68e83539730f32f86",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
+   "inputRev": "v4.4.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Game",

diff --git a/lakefile.lean b/lakefile.lean
@@ -46,10 +46,10 @@ package Game where
     "-Dtactic.hygienic=false",
     "-Dlinter.unusedVariables.funArgs=false",
     "-Dtrace.debug=false"]
-  moreServerArgs := #[
-    "-Dtactic.hygienic=false",
-    "-Dlinter.unusedVariables.funArgs=true",
-    "-Dtrace.debug=true"]
+  moreServerOptions := #[
+    ⟨`tactic.hygienic, false⟩,
+    ⟨`linter.unusedVariables.funArgs, true⟩,
+    ⟨`trace.debug, true⟩]
   weakLeanArgs := #[]
 
 @[default_target]

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.4.0