diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 58dab42..62b8651 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -13,7 +13,9 @@ "overrideCommand": true, "onCreateCommand": { "npm_install": "(cd ~/lean4game && npm install)", - "lake_build": "(cd ~/game && lake update -R && lake build" + // BUG: Apparently `&& lake exe cache get` was needed here because the update hook was broken. + // should been fixed in https://github.com/leanprover-community/mathlib4/pull/8755 + "lake_build": "(cd ~/game && lake update -R && lake exe cache get && lake build)" }, "postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start", "customizations": { diff --git a/lake-manifest.json b/lake-manifest.json index 1401dbe..3c7f598 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,24 +1,24 @@ {"version": 7, "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/lean4game.git", - "type": "git", - "subDir": "server", - "rev": "241ef4b67a5c95e33a4101769bb34ae45a66b82c", - "name": "GameServer", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.3.0-rc2", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/std4", + [{"url": "https://github.com/leanprover/std4.git", "type": "git", "subDir": null, "rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.3.0-rc2", "inherited": true, "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/lean4game.git", + "type": "git", + "subDir": "server", + "rev": "622e9d389768e8abb5b3103a65d07165587a27ad", + "name": "GameServer", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.3.0-rc2", + "inherited": false, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null,