diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 43abb73..28c9ec6 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -478,6 +478,8 @@ section Initialization return (ctx, { doc := doc initHeaderStx := headerStx + currHeaderStx := headerStx + importCachingTask? := none pendingRequests := RBMap.empty rpcSessions := RBMap.empty }) diff --git a/server/GameServer/Watchdog.lean b/server/GameServer/Watchdog.lean index 11273b0..e9f938e 100644 --- a/server/GameServer/Watchdog.lean +++ b/server/GameServer/Watchdog.lean @@ -103,7 +103,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do let gameName := if args.length < 4 then defaultGameName else args[3]! let workerPath := "./gameserver" -- TODO: Do the following commands slow us down? - let srcSearchPath ← initSrcSearchPath (← getBuildDir) + let srcSearchPath ← initSrcSearchPath let references ← IO.mkRef (← loadReferences) let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap) let i ← maybeTee "wdIn.txt" false i diff --git a/server/lake-manifest.json b/server/lake-manifest.json index 2554a52..9dd23f3 100644 --- a/server/lake-manifest.json +++ b/server/lake-manifest.json @@ -4,10 +4,10 @@ [{"url": "https://github.com/leanprover/std4.git", "type": "git", "subDir": null, - "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087", + "rev": "ce2db21d86502e00c4761da5ade58a61612de656", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "v4.3.0", + "inputRev": "v4.4.0-rc1", "inherited": false, "configFile": "lakefile.lean"}], "name": "GameServer", diff --git a/server/lean-toolchain b/server/lean-toolchain index 5cadc9d..91ccf6a 100644 --- a/server/lean-toolchain +++ b/server/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.3.0 +leanprover/lean4:v4.4.0-rc1