update lakefile

2023-04-25 18:58:28 +02:00
parent 9f1bb21b27
commit 5da0c41dfa
2 changed files with 8 additions and 3 deletions
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -19,8 +19,12 @@
    "rev": "071464ac36e339afb7a87640aa1f8121f707a59a",
    "name": "aesop",
    "inputRev?": "master"}},
-  {"path":
-   {"name": "GameServer", "dir": "./../game/lean4game/server/leanserver"}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/lean4game.git",
+    "subDir?": "server/leanserver",
+    "rev": "9fa94ecc5ca1c398479fb6026b03fcac46928bd7",
+    "name": "GameServer",
+    "inputRev?": "main"}},
  {"git":
   {"url": "https://github.com/leanprover/std4",
    "subDir?": null,
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,7 +1,8 @@
 import Lake
 open Lake DSL

-require GameServer from ".."/"game"/"lean4game"/"server"/"leanserver"
+require GameServer from  git
+  "https://github.com/leanprover-community/lean4game.git"@"main"/"server"/"leanserver"

 require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "fc4a489c2af75f687338fe85c8901335360f8541"