fix path issues

server/index.mjs

@@ -23,13 +23,15 @@ const wss = new WebSocketServer({ server })
 const environment = process.env.NODE_ENV
 const isDevelopment = environment === 'development'
 
-let cmd, cmdArgs;
+let cmd, cmdArgs, cwd;
 if (isDevelopment) {
-    cmd = "./leanserver/build/bin/gameserver";
+    cmd = "lake";
-    cmdArgs = ["--server"];
+    cmdArgs = ["exe", "gameserver", "--server"];
+    cwd = "./leanserver"
 } else{
     cmd = "docker";
     cmdArgs = ["run", "--runtime=runsc", "--network=none", "--rm", "-i", "testgame:latest"];
+    cwd = "."
 }
 
 wss.addListener("connection", function(ws) {
@@ -42,7 +44,7 @@ wss.addListener("connection", function(ws) {
     const reader = new rpc.WebSocketMessageReader(socket);
     const writer = new rpc.WebSocketMessageWriter(socket);
     const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
-    const serverConnection = jsonrpcserver.createServerProcess('Lean Server', cmd, cmdArgs);
+    const serverConnection = jsonrpcserver.createServerProcess('Lean Server', cmd, cmdArgs, { cwd });
     socketConnection.forward(serverConnection, message => {
         console.log(`CLIENT: ${JSON.stringify(message)}`)
         return message;

server/leanserver/GameServer/FileWorker.lean

@@ -84,14 +84,15 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
       fileMap      := inputCtx.fileMap
       tacticCache? := some tacticCacheNew
     }
+    IO.FS.writeFile "test.txt" s!"{tacticStx}"
     let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get scope.opts) <| liftM (m := BaseIO) do
       Elab.Command.catchExceptions
         (getResetInfoTrees *> do
-          let level := `level1
+          -- let level := `level1
           let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[]
           let tacticStx := (tacticStx.getArgs.push done).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
-          let cmdStx ← `(command| example : $(mkIdent level) := by {unfold $(mkIdent level); $(⟨tacticStx⟩)} )
+          let cmdStx ← `(command| example : 0 = 0 := by {$(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
         cmdCtx cmdStateRef
     let postNew := (← tacticCacheNew.get).post

server/leanserver/GameServer/Watchdog.lean

@@ -107,7 +107,7 @@ def initAndRunWatchdogAux : GameServerM Unit := do
     | throwServerError "Got `shutdown` request, expected an `exit` notification"
 
 def createEnv : IO Environment := do
-  let gameDir := "testgame"
+  let gameDir := "../testgame"
 
   -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
   let out ← IO.Process.output
@@ -128,8 +128,8 @@ def createEnv : IO Environment := do
   return env
 
 def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
+  let workerPath := "./build/bin/gameserver"
   -- TODO: Do the following commands slow us down?
-  let workerPath ← findWorkerPath
   let srcSearchPath ← initSrcSearchPath (← getBuildDir)
   let references ← IO.mkRef (← loadReferences)
   let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)