diff --git a/package.json b/package.json index b67aa8f..1f6e009 100644 --- a/package.json +++ b/package.json @@ -54,7 +54,8 @@ "build": "npm run build_server && npm run build_client", "build_server": "server/build.sh", "build_client": "NODE_ENV=production webpack", - "production": "NODE_ENV=production node server/index.mjs" + "production": "NODE_ENV=production node server/index.mjs", + "update_lean": "cd server && (cd testgame && lake update) && cp testgame/lean-toolchain leanserver/lean-toolchain" }, "eslintConfig": { "extends": [ diff --git a/server/testgame/lake-manifest.json b/server/testgame/lake-manifest.json index 06dba30..b2d80c3 100644 --- a/server/testgame/lake-manifest.json +++ b/server/testgame/lake-manifest.json @@ -28,9 +28,9 @@ {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "9b15aa6f091a623f992d6fff76167864794ce350", + "rev": "a461e549ebaac0c9b6a83969bcaa982bff6adafc", "name": "mathlib", - "inputRev?": "9b15aa6f091a623f992d6fff76167864794ce350"}}, + "inputRev?": "master"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, @@ -40,7 +40,7 @@ {"git": {"url": "https://github.com/JLimperg/aesop", "subDir?": null, - "rev": "70c59fcfc63de90786d59222c32468dab87964c5", + "rev": "ddced06b6b76483fe8794f2b516c57980a08fcef", "name": "aesop", "inputRev?": "master"}}, {"git": @@ -59,6 +59,6 @@ {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "42bb39d34ec7dcb07580458efa4a7936bd5192b7", + "rev": "6196cf930a95664987eba8aee62ae7802d51428c", "name": "std", "inputRev?": "main"}}]} diff --git a/server/testgame/lakefile.lean b/server/testgame/lakefile.lean index c63997f..27631d6 100644 --- a/server/testgame/lakefile.lean +++ b/server/testgame/lakefile.lean @@ -4,7 +4,7 @@ open Lake DSL require GameServer from ".."/"leanserver" require mathlib from git - "https://github.com/leanprover-community/mathlib4.git"@"9b15aa6f091a623f992d6fff76167864794ce350" + "https://github.com/leanprover-community/mathlib4.git"@"master" --set_option tactic.hygienic false --set_option autoImplicit false