Compare commits
1
Commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
bffc9fcefb |
@@ -478,6 +478,8 @@ section Initialization
|
|||||||
return (ctx,
|
return (ctx,
|
||||||
{ doc := doc
|
{ doc := doc
|
||||||
initHeaderStx := headerStx
|
initHeaderStx := headerStx
|
||||||
|
currHeaderStx := headerStx
|
||||||
|
importCachingTask? := none
|
||||||
pendingRequests := RBMap.empty
|
pendingRequests := RBMap.empty
|
||||||
rpcSessions := RBMap.empty
|
rpcSessions := RBMap.empty
|
||||||
})
|
})
|
||||||
|
|||||||
@@ -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 gameName := if args.length < 4 then defaultGameName else args[3]!
|
||||||
let workerPath := "./gameserver"
|
let workerPath := "./gameserver"
|
||||||
-- TODO: Do the following commands slow us down?
|
-- TODO: Do the following commands slow us down?
|
||||||
let srcSearchPath ← initSrcSearchPath (← getBuildDir)
|
let srcSearchPath ← initSrcSearchPath
|
||||||
let references ← IO.mkRef (← loadReferences)
|
let references ← IO.mkRef (← loadReferences)
|
||||||
let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
|
let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
|
||||||
let i ← maybeTee "wdIn.txt" false i
|
let i ← maybeTee "wdIn.txt" false i
|
||||||
|
|||||||
@@ -4,10 +4,10 @@
|
|||||||
[{"url": "https://github.com/leanprover/std4.git",
|
[{"url": "https://github.com/leanprover/std4.git",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": null,
|
"subDir": null,
|
||||||
"rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
|
"rev": "ce2db21d86502e00c4761da5ade58a61612de656",
|
||||||
"name": "std",
|
"name": "std",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "v4.3.0",
|
"inputRev": "v4.4.0-rc1",
|
||||||
"inherited": false,
|
"inherited": false,
|
||||||
"configFile": "lakefile.lean"}],
|
"configFile": "lakefile.lean"}],
|
||||||
"name": "GameServer",
|
"name": "GameServer",
|
||||||
|
|||||||
@@ -1 +1 @@
|
|||||||
leanprover/lean4:v4.3.0
|
leanprover/lean4:v4.4.0-rc1
|
||||||
|
|||||||
Reference in New Issue
Block a user