diff --git a/server/index.js b/server/index.js index d85df14..fb3c9cf 100644 --- a/server/index.js +++ b/server/index.js @@ -30,8 +30,7 @@ class ClientConnection { constructor(ws){ console.log("Socket opened.") - this.ws = ws - this.ws.send("ok"); + this.ws = ws this.ws.on("message", (msg) => { this.send(JSON.parse(msg.toString("utf8"))); @@ -68,7 +67,7 @@ class ClientConnection { send(data) { const str = JSON.stringify(data) + "\n"; const byteLength = Buffer.byteLength(str, "utf-8"); - + this.lean.stdin.cork(); this.lean.stdin.write(str); this.lean.stdin.uncork(); @@ -83,4 +82,4 @@ wss.on("connection", function(ws) { // what should a websocket do on connecti // wss.handleUpgrade(request, socket, head, function done(ws) { // wss.emit('connection', ws, request); // }); -// }); \ No newline at end of file +// }); diff --git a/server/leanserver/GameServer/Communication.lean b/server/leanserver/GameServer/Communication.lean new file mode 100644 index 0000000..210abc9 --- /dev/null +++ b/server/leanserver/GameServer/Communication.lean @@ -0,0 +1,98 @@ +/- Inspired by `Lean/Data/Lsp/Communication.lean` -/ +import Lean.Data.JsonRpc + +/-! Reading/writing Game Server Protocol messages from/to IO handles. -/ + +namespace IO.FS.Stream + +open Lean +open Lean.JsonRpc + +section + +def readJsonLine (h : FS.Stream) : IO Json := do + let s ← h.getLine + ofExcept (Json.parse s) + +def readGspMessage (h : FS.Stream) : IO Message := do + let j ← h.readJsonLine + match fromJson? j with + | Except.ok m => pure m + | Except.error inner => + throw $ + userError s!"JSON '{j.compress}' did not have the format of a JSON-RPC message.\n{inner}" + +def readGspRequestAs (h : FS.Stream) (expectedMethod : String) (α) [FromJson α] + : IO (Request α) := do + let m ← h.readGspMessage + match m with + | Message.request id method params? => + if method = expectedMethod then + let j := toJson params? + match fromJson? j with + | Except.ok v => pure ⟨id, expectedMethod, v⟩ + | Except.error inner => + throw $ + userError s!"Unexpected param '{j.compress}' for method '{expectedMethod}'\n{inner}" + else + throw $ userError s!"Expected method '{expectedMethod}', got method '{method}'" + | _ => throw $ userError s!"Expected JSON-RPC request, got: '{(toJson m).compress}'" + +def readGspNotificationAs + (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α) [FromJson α] + : IO (Notification α) := do + let m ← h.readMessage nBytes + match m with + | Message.notification method params? => + if method = expectedMethod then + let j := toJson params? + match fromJson? j with + | Except.ok v => pure ⟨expectedMethod, v⟩ + | Except.error inner => + throw $ + userError s!"Unexpected param '{j.compress}' for method '{expectedMethod}'\n{inner}" + else + throw $ userError s!"Expected method '{expectedMethod}', got method '{method}'" + | _ => throw $ userError s!"Expected JSON-RPC notification, got: '{(toJson m).compress}'" + +def readGspResponseAs + (h : FS.Stream) (nBytes : Nat) (expectedID : RequestID) (α) [FromJson α] + : IO (Response α) := do + let m ← h.readMessage nBytes + match m with + | Message.response id result => + if id == expectedID then + match fromJson? result with + | Except.ok v => pure ⟨expectedID, v⟩ + | Except.error inner => throw $ userError s!"Unexpected result '{result.compress}'\n{inner}" + else + throw $ userError s!"Expected id {expectedID}, got id {id}" + | Message.notification .. => readResponseAs h nBytes expectedID α + | _ => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'" + +end + +section + variable [ToJson α] + + def writeGspMessage (h : FS.Stream) (m : Message) : IO Unit := do + h.writeMessage m + h.putStr "\n" + + def writeGspRequest (h : FS.Stream) (r : Request α) : IO Unit := + h.writeGspMessage r + + def writeGspNotification (h : FS.Stream) (n : Notification α) : IO Unit := + h.writeGspMessage n + + def writeGspResponse (h : FS.Stream) (r : Response α) : IO Unit := + h.writeGspMessage r + + def writeGspResponseError (h : FS.Stream) (e : ResponseError Unit) : IO Unit := + h.writeGspMessage (Message.responseError e.id e.code e.message none) + + def writeGspResponseErrorWithData (h : FS.Stream) (e : ResponseError α) : IO Unit := + h.writeGspMessage e +end + +end IO.FS.Stream diff --git a/server/leanserver/GameServer/Server.lean b/server/leanserver/GameServer/Server.lean index ff75d81..6eb0edb 100644 --- a/server/leanserver/GameServer/Server.lean +++ b/server/leanserver/GameServer/Server.lean @@ -1,5 +1,5 @@ /- -This is the Lean 4 game server. It offers a way to interact with Lean 4 which +This is the Lean 4 game server. It offers a way to interact with Lean 4 which is completely distinct from running the command-line lean or the language server protocol. It is based on lean-gym by Daniel Selsam. @@ -8,6 +8,7 @@ import Lean.Data.Json.Basic import GameServer.Utils import GameServer.EnvExtensions +import GameServer.Communication open Lean Meta Elab Tactic Std @@ -54,10 +55,10 @@ match (← getMCtx).findDecl? goal with return {objects := objects, assumptions := assumptions, goal := toString (← Meta.ppExpr mvarDecl.type), mvarid := goal } -def GameGoal.toJson (gameGoal : GameGoal) : MetaM Json := +def GameGoal.toJson (gameGoal : GameGoal) : MetaM Json := gameGoal.mvarid.withContext do - return Json.mkObj [("objects", Lean.ToJson.toJson (← gameGoal.objects.mapM Lean.LocalDecl.toJson)), - ("assumptions", Lean.ToJson.toJson (← gameGoal.assumptions.mapM Lean.LocalDecl.toJson)), + return Json.mkObj [("objects", Lean.ToJson.toJson (← gameGoal.objects.mapM Lean.LocalDecl.toJson)), + ("assumptions", Lean.ToJson.toJson (← gameGoal.assumptions.mapM Lean.LocalDecl.toJson)), ("goal", gameGoal.goal)] @@ -77,7 +78,7 @@ inductive Action where deriving ToJson, FromJson, Repr def Action.parse (s : String) : Action := - let e : Except String Action := + let e : Except String Action := try return ← fromJson? (← Json.parse s) catch _ => return Action.invalid s @@ -85,7 +86,7 @@ def Action.parse (s : String) : Action := | Except.ok a => a | _ => Action.info -def Action.get : IO Action := +def Action.get : IO Action := return Action.parse (← (← IO.getStdin).getLine) @@ -116,7 +117,7 @@ structure SavedState where abbrev LevelM := ReaderT GameLevel StateRefT (Array SavedState) TermElabM /-- Returns the most recent SavedState. -/ -def getState : LevelM SavedState := do +def getState : LevelM SavedState := do let some state := (← get).back? | throwError "Couldn't find tactic state" return state @@ -134,8 +135,8 @@ def Response.toJson (resp : Response) : MetaM Json := /-! ## Main running functions -/ /-- Dummy `Core.Context` value to be fed to `Lean.Core.CoreM.toIO` -/ -def coreCtx : Core.Context := { - currNamespace := Name.anonymous, +def coreCtx : Core.Context := { + currNamespace := Name.anonymous, openDecls := [], fileName := "", fileMap := { source := "", positions := #[0], lines := #[1] } } @@ -147,9 +148,9 @@ partial def runLevel (env : Environment) (GameName : Name) (levels : HashMap Nat let some lvl := levels.find? idx | throwError s!"Cannot find level {idx}" let mvar ← mkFreshExprMVar (some lvl.goal) (kind := MetavarKind.synthetic) let (_, mvar) ← mvar.mvarId!.introNP lvl.intro_nb - mvar.withContext do + mvar.withContext do let state := #[{tacticState := { term := ← Term.saveState, tactic := { goals := [mvar] }}}] - let levelM : LevelM Unit := do + let levelM : LevelM Unit := do let resp := {← mkResponse with message := lvl.introduction} let levelInfo : LevelInfo := { index := lvl.index, @@ -165,15 +166,15 @@ partial def runLevel (env : Environment) (GameName : Name) (levels : HashMap Nat let metaM : MetaM Unit := termElabM.run' (ctx := {}) try discard <| metaM.run'.toIO coreCtx { env := env } - catch + catch | .userError s => output s!"Could not run level {idx}: {s}" | _ => output s!"Could not run level {idx}" - + where mkResponse (errors : Array String := #[]) : LevelM Response := do let savedState ← getState - let goals := savedState.tacticState.tactic.goals + let goals := savedState.tacticState.tactic.goals return { goals := (← liftM $ goals.mapM Lean.MVarId.toGameGoal), message := savedState.message, errors := errors } /-- Try to parse the given String as a single line tactic invocation. Update the LevelM state only @@ -182,7 +183,7 @@ where runTactic (tacticString : String) : LevelM Response := do let lvl ← read let tacticNames := (lvl.tactics.map (·.name.toString)).toList - let tacName := (tacticString.trim.splitOn " ").headD "" + let tacName := (tacticString.trim.splitOn " ").headD "" if not (tacticNames.contains tacName) then mkResponse #["Unrecognized tactic"] else let savedState ← getState match Parser.runParserCategory (← getEnv) `tactic tacticString "" with @@ -191,7 +192,7 @@ where savedState.tacticState.term.restore let mvarId : MVarId := savedState.tacticState.tactic.goals.head! try - let unsolvedGoals ← Tactic.run mvarId do set savedState.tacticState.tactic + let unsolvedGoals ← Tactic.run mvarId do set savedState.tacticState.tactic evalTactic stx if (← getThe Core.State).messages.hasErrors then let messages := (← getThe Core.State).messages.getErrorMessages.toList.toArray @@ -211,7 +212,7 @@ where message := (← read).conclusion modify fun s => s.push {tacticState := savedState, message := message} mkResponse - catch ex => mkResponse #[← ex.toMessageData.toString] + catch ex => mkResponse #[← ex.toMessageData.toString] mainLoop : LevelM Unit := do match ← Action.get with @@ -227,25 +228,30 @@ where | Action.invalid s => output s!"{← { ← mkResponse with errors := #[s!"Invalid action: {s}"] : Response}.toJson}" mainLoop +#check (toJson "").compress open System Lean Std in -partial def runGame (GameName : Name) (paths : List FilePath): IO Unit := do - searchPathRef.set paths - let env ← importModules [{ module := `Init : Import }, { module := GameName : Import }] {} 0 - let termElabM : TermElabM Unit := do - let levels := levelsExt.getState env - let game := {← gameExt.get with nb_levels := levels.size } - mainLoop env game levels - let metaM : MetaM Unit := termElabM.run' (ctx := {}) - discard <| metaM.run'.toIO coreCtx { env := env } -where - mainLoop (env : Environment) (game : Game) (levels : HashMap Nat GameLevel): IO Unit := do - match ← Action.get with - | Action.info => output (toJson game) - | Action.loadLevel n => runLevel env GameName levels n - | Action.quit => IO.Process.exit 0 - | Action.invalid s => output s!"Invalid action: {s}" - | _ => output "Invalid action" - mainLoop env game levels - +partial def runGame (GameName : Name) : IO Unit := do + let hIn ← IO.getStdin + let hOut ← IO.getStdout + let hLog ← IO.getStderr + hLog.putStr s!"{toJson $ ← hIn.readGspMessage}" + hOut.writeGspNotification ⟨"Hello!", "s"⟩ +-- let env ← importModules [{ module := `Init : Import }, { module := GameName : Import }] {} 0 +-- let termElabM : TermElabM Unit := do +-- let levels := levelsExt.getState env +-- let game := {← gameExt.get with nb_levels := levels.size } +-- mainLoop env game levels +-- let metaM : MetaM Unit := termElabM.run' (ctx := {}) +-- discard <| metaM.run'.toIO coreCtx { env := env } +-- where +-- mainLoop (env : Environment) (game : Game) (levels : HashMap Nat GameLevel): IO Unit := do +-- match ← Action.get with +-- | Action.info => output (toJson game) +-- | Action.loadLevel n => runLevel env GameName levels n +-- | Action.quit => IO.Process.exit 0 +-- | Action.invalid s => output s!"Invalid action: {s}" +-- | _ => output "Invalid action" +-- mainLoop env game levels + end Server diff --git a/server/leanserver/GameServer/Worker.lean b/server/leanserver/GameServer/Worker.lean new file mode 100644 index 0000000..f44af77 --- /dev/null +++ b/server/leanserver/GameServer/Worker.lean @@ -0,0 +1,15 @@ +import Lean.Data.JsonRpc + +-- The worker implementation roughly follows `Lean/Server/FileWorker.lean`. + + +#check IO.bindTask + +#check Task +#check Task.CancelToken + +#check EIO.mapTask + +#check maybeTee + +#check IO.FS.Stream.writeMessage diff --git a/server/leanserver/Main.lean b/server/leanserver/Main.lean index e477189..68b7bf4 100644 --- a/server/leanserver/Main.lean +++ b/server/leanserver/Main.lean @@ -1,16 +1,30 @@ import GameServer.Server +-- TODO: Potentially it could be useful to pass in the `gameName` via the websocket connection + unsafe def main (args : List String) : IO Unit := do + -- Check if required arguments are given by the user if args.length != 2 then - throw (IO.userError "Expected two arguments: The name of the game module and the path to the game project.") - - let out ← IO.Process.output { cwd := args[1]!, cmd := "lake", args := #["env","printenv","LEAN_PATH"] } + throw (IO.userError $ "Expected two arguments:" ++ + "The name of the game module and the path to the game project.") + let gameName := args[0]! + let gameDir := args[1]! + -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`. + let out ← IO.Process.output + { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] } if out.exitCode != 0 then IO.eprintln out.stderr - else - let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim - let currentDir ← IO.currentDir - let paths := paths.map fun p => currentDir / (args[1]! : System.FilePath) / p - Server.runGame (Lean.Name.mkSimple args[0]!) paths + return + + -- Make the paths relative to the current directory + let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim + let currentDir ← IO.currentDir + let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p + + -- Set the search path + Lean.searchPathRef.set paths + + -- Run the game + Server.runGame gameName