communicate via JSON RPC

client/src/App.tsx

@@ -22,21 +22,17 @@ function App() {
 	const [nbLevels, setNbLevels] = useState(0)
 	const [curLevel, setCurLevel] = useState(0)
 	const [finished, setFinished] = useState(false)
-	const [rpcConnection, setRpcConnection] = useState(null)
+	const [rpcConnection, setRpcConnection] = useState<null|rpc.MessageConnection>(null)
 
 	const socketUrl = 'ws://' + window.location.host + '/websocket/'
 
-	const { sendJsonMessage, getWebSocket } = useWebSocket(socketUrl, {
+	useWebSocket(socketUrl, {
 		onOpen: function (ev) {
     	const logger = new rpc.ConsoleLogger();
       const socket = rpc.toSocket(ev.target as WebSocket);
 			let rpcConnection = rpc.createWebSocketConnection(socket, logger)
       setRpcConnection(rpcConnection);
 			rpcConnection.listen();
-			rpcConnection.onNotification("Hello!", () => {
-				console.log("Yes"); // This prints Hello World
-			});
-			rpcConnection.sendNotification("Hello!", 'Hello World');
 		}
 	})
 
@@ -56,14 +52,14 @@ function App() {
 		setCurLevel(1)
 	}
 
-	// let mainComponent;
+	let mainComponent;
-	// if (finished) {
+	if (finished) {
-	//   mainComponent = <GoodBye message={conclusion} />
+	  mainComponent = <GoodBye message={conclusion} />
-	// } else if (curLevel > 0) {
+	} else if (curLevel > 0) {
-	//   mainComponent = <Level sendJsonMessage={sendJsonMessage} lastMessage={lastMessage} lastJsonMessage={lastJsonMessage} nbLevels={nbLevels} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
+	  mainComponent = <Level rpcConnection={rpcConnection} nbLevels={nbLevels} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
-	// } else {
+	} else {
-  //     mainComponent = <Welcome sendJsonMessage={sendJsonMessage} lastMessage={lastMessage} lastJsonMessage={lastJsonMessage} setNbLevels={setNbLevels} setTitle={setTitle} startGame={startGame} setConclusion={setConclusion}/>
+    mainComponent = <Welcome rpcConnection={rpcConnection} setNbLevels={setNbLevels} setTitle={setTitle} startGame={startGame} setConclusion={setConclusion}/>
-	// }
+	}
 
   return (
     <div className="App">
@@ -79,7 +75,7 @@ function App() {
 				</Typography>
 				</Toolbar>
 			</AppBar>
-			{/* {mainComponent} */}
+			{mainComponent}
 		</MathJaxContext>
     </div>
   )

client/src/components/Level.tsx

@@ -11,10 +11,18 @@ import LeftPanel from './LeftPanel';
 import InputZone from './InputZone';
 import Message from './Message';
 import TacticState from './TacticState';
+import * as rpc from 'vscode-ws-jsonrpc';
 
+interface LevelProps {
+  rpcConnection: null|rpc.MessageConnection;
+  nbLevels: any;
+	level: any;
+	setCurLevel: any;
+	setLevelTitle: any;
+	setFinished: any
+}
 
-
+function Level({ rpcConnection, nbLevels, level, setCurLevel, setLevelTitle, setFinished }: LevelProps) {
-function Level({ sendJsonMessage, lastMessage, lastJsonMessage, nbLevels, level, setCurLevel, setLevelTitle, setFinished }) {
 	const [index, setIndex] = useState(level) // Level number
 	const [tacticDocs, setTacticDocs] = useState([])
 	const [lemmaDocs, setLemmaDocs] = useState([])
@@ -30,46 +38,40 @@ function Level({ sendJsonMessage, lastMessage, lastJsonMessage, nbLevels, level,
 
 	const [completed, setCompleted] = useState(false)
 
-	// The next function will be called when the level changes
+	const processResponse = (res:any) => {
-	useEffect(() => {
+		setLeanData(res);
-		sendJsonMessage({ "loadLevel": level });
+		setErrors(res.errors);
-	}, [level, sendJsonMessage])
+		if (res.message !== "" && res.errors?.length === 0) {
-
+			setMessage(res.message)
-	// The next function will be called when a message arrives or the level title changes
-	useEffect(() => {
-		console.log(lastMessage)
-		console.log(lastJsonMessage)
-		if ("nb_levels" in lastJsonMessage) { return } // this is an old message from starting the game
-		const data = lastJsonMessage;
-		if ("title" in data) { // This is the level metadata coming in
-			setLevelTitle("Level " + data["index"] + ": " + data["title"])
-			setIndex(parseInt(data["index"]))
-			setTacticDocs(data["tactics"])
-			setLemmaDocs(data["lemmas"])
-		}
-
-		if (data["message"] !== "" && data.errors.length === 0) {
-			setMessage(data["message"])
 			setMessageOpen(true)
 		}
-		setLeanData(data);
+		if (res.goals?.length === 0 && res.errors?.length === 0) {
-		setErrors(data.errors);
-		if (data.goals.length === 0 && data.errors.length === 0) {
 			setCompleted(true)
 		}
+	}
 
-	}, [lastJsonMessage, lastMessage, setLevelTitle])
+	// The next function will be called when the level changes
-
+	useEffect(() => {
+		if (rpcConnection) {
+			rpcConnection.sendRequest("loadLevel", {number: level}).then((res) => {
+				setLevelTitle("Level " + res["index"] + ": " + res["title"])
+				setIndex(parseInt(res["index"]))
+				setTacticDocs(res["tactics"])
+				setLemmaDocs(res["lemmas"])
+				processResponse(res)
+			});
+		}
+	}, [level, rpcConnection])
 
 	function sendTactic(input) {
-		sendJsonMessage({ "runTactic": input });
+		rpcConnection.sendRequest("runTactic", {tactic: input}).then(processResponse);
 		setLastTactic(input);
 		setHistory(history.concat([input]));
 	}
 
 	function undo() {
 		if (errors.length === 0) {
-			sendJsonMessage('undo');
+			rpcConnection.sendRequest('undo').then(processResponse);
 		}
 		if (history.length > 1) {
 			setLastTactic(history[history.length - 1]);
@@ -112,4 +114,4 @@ function Level({ sendJsonMessage, lastMessage, lastJsonMessage, nbLevels, level,
 	)
 }
 
-export default Level
+export default Level

client/src/components/Welcome.tsx

@@ -6,32 +6,44 @@ import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
+import * as rpc from 'vscode-ws-jsonrpc';
 
 import { Box, Typography, Button, CircularProgress, Grid } from '@mui/material';
 
+interface WelcomeProps {
+  rpcConnection: null|rpc.MessageConnection;
+  setNbLevels: any;
+	setTitle: any;
+	startGame: any;
+	setConclusion: any;
+}
 
-function Welcome({ sendJsonMessage, lastJsonMessage, lastMessage, setNbLevels, setTitle, startGame, setConclusion }) {
+type infoResultType = {
+	title: string,
+	nb_levels: any[],
+	conclusion: string
+}
 
-	const [leanData, setLeanData] = useState({})
+const infoRequestType = new rpc.RequestType0<infoResultType, void>("info")
+
+function Welcome({ rpcConnection, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) {
+
+	const [leanData, setLeanData] = useState<null|infoResultType>(null)
 
-	// Will run at the very beginning
 	useEffect(() => {
-		sendJsonMessage('info')
+		if (rpcConnection) { // Will run in the beginning as soon as RPC connection is established
-	}, [sendJsonMessage])
+			rpcConnection.sendRequest(infoRequestType).then((res: infoResultType) =>{
-
+				setLeanData(res)
-	// Will run when a Json message arrives
+				setNbLevels(res.nb_levels)
-	useEffect(() => {
+				setTitle(res.title)
-		if (lastJsonMessage != null && lastJsonMessage.hasOwnProperty("nb_levels")) {
+				document.title = res.title
-			setLeanData(lastJsonMessage)
+				setConclusion(res.conclusion)
-			setNbLevels(lastJsonMessage.nb_levels)
+			});
-			setTitle(lastJsonMessage.title)
-			document.title = lastJsonMessage.title
-			setConclusion(lastJsonMessage.conclusion)
 		}
-	}, [lastJsonMessage, setNbLevels, setTitle, setConclusion])
+	}, [rpcConnection, setLeanData, setNbLevels, setTitle, setConclusion])
 
 	let content
-	if ("introduction" in leanData) {
+	if (leanData) {
 		content = (<Box sx={{ m: 3 }}>
 			<Typography variant="body1" component="div">
 			  <MathJax>

server/index.js

@@ -33,6 +33,7 @@ class ClientConnection {
         this.ws = ws
 
         this.ws.on("message", (msg) => {
+            console.log(msg.toString("utf8"));
             this.send(JSON.parse(msg.toString("utf8")));
         })
 

server/leanserver/GameServer/Communication.lean

@@ -76,8 +76,8 @@ section
   variable [ToJson α]
 
   def writeGspMessage (h : FS.Stream) (m : Message) : IO Unit := do
-    h.writeMessage m
+    h.putStr ((toJson m).compress ++ "\n")
-    h.putStr "\n"
+    h.flush
 
   def writeGspRequest (h : FS.Stream) (r : Request α) : IO Unit :=
     h.writeGspMessage r

server/leanserver/GameServer/Server.lean

@@ -142,7 +142,15 @@ def coreCtx : Core.Context := {
   fileMap := { source := "", positions := #[0], lines := #[1] } }
 
 
-partial def runLevel (env : Environment) (GameName : Name) (levels : HashMap Nat GameLevel) (idx : Nat) : IO Unit := do
+structure RunTacticParams where
+  tactic : String
+deriving FromJson
+
+structure LoadLevelParams where
+  number : Nat
+deriving FromJson
+
+partial def runLevel (requestId : JsonRpc.RequestID) (env : Environment) (GameName : Name) (levels : HashMap Nat GameLevel) (idx : Nat) : IO Unit := do
   let levelName : Name := s!"Level{toString idx}"
   let termElabM : TermElabM Unit := do
     let some lvl := levels.find? idx | throwError s!"Cannot find level {idx}"
@@ -160,7 +168,8 @@ partial def runLevel (env : Environment) (GameName : Name) (levels : HashMap Nat
                 errors := resp.errors,
                 goals := resp.goals,
                 message := resp.message }
-          output (← levelInfo.toJson)
+          let hOut ← IO.getStdout
+          hOut.writeGspResponse ⟨requestId, ← levelInfo.toJson⟩
           mainLoop
       levelM.run lvl |>.run' state
   let metaM : MetaM Unit := termElabM.run' (ctx := {})
@@ -215,43 +224,66 @@ where
         catch ex => mkResponse #[← ex.toMessageData.toString]
 
   mainLoop : LevelM Unit := do
-    match ← Action.get with
+    let hIn ← IO.getStdin
-    | Action.runTactic tac => do let resp ← runTactic tac; output s!"{← resp.toJson}"
+    let hOut ← IO.getStdout
-    | Action.loadLevel n => runLevel env GameName levels n
+    let hLog ← IO.getStderr
-    | Action.undo => do modify fun s => s.pop; output s!"{← (← mkResponse).toJson}"
+    let m ← hIn.readGspMessage
-    | Action.restartLevel => runLevel env GameName levels idx
+    match m with
-    | Action.prev => runLevel env GameName levels idx.pred
+    | .request id "runTactic" params => do
-    | Action.next => runLevel env GameName levels idx.succ
+      match fromJson? (toJson (params)) with
-    | Action.quit => IO.Process.exit 0
+      | Except.ok (v : RunTacticParams) =>
-    | Action.restartGame => output "Can't restart game now"
+        let resp ← runTactic v.tactic
-    | Action.info => output "Can't get info now"
+        hOut.writeGspResponse ⟨id, ← resp.toJson⟩
-    | Action.invalid s => output s!"{← { ← mkResponse with errors := #[s!"Invalid action: {s}"] : Response}.toJson}"
+      | Except.error inner =>
+        hLog.putStr s!"Invalid params: {inner}"
+        hLog.flush
+    | .request id "loadLevel" (some params) =>
+      match fromJson? (toJson (params)) with
+      | Except.ok (v : LoadLevelParams) =>
+        runLevel id env GameName levels v.number
+      | Except.error inner =>
+        hLog.putStr s!"Invalid params: {inner}"
+        hLog.flush
+    | .request id "undo" _ => do
+       modify fun s => s.pop
+       hOut.writeGspResponse ⟨id, ← (← mkResponse).toJson⟩
+    | _ =>
+      hLog.putStr s!"Invalid action: {toJson m}"
+      hLog.flush
     mainLoop
 
-#check (toJson "").compress
-
 open System Lean Std in
 partial def runGame (GameName : Name) : IO Unit := do
-  let hIn ← IO.getStdin
+  let env ← importModules [{ module := `Init : Import }, { module := GameName : Import }] {} 0
-  let hOut ← IO.getStdout
+  let termElabM : TermElabM Unit := do
-  let hLog ← IO.getStderr
+    let levels := levelsExt.getState env
-  hLog.putStr s!"{toJson $ ← hIn.readGspMessage}"
+    let game := {← gameExt.get with nb_levels := levels.size }
-  hOut.writeGspNotification ⟨"Hello!", "s"⟩
+    mainLoop env game levels
---   let env ← importModules [{ module := `Init : Import }, { module := GameName : Import }] {} 0
+  let metaM : MetaM Unit := termElabM.run' (ctx := {})
---   let termElabM : TermElabM Unit := do
+  discard <| metaM.run'.toIO coreCtx { env := env }
---     let levels := levelsExt.getState env
+where
---     let game := {← gameExt.get with nb_levels := levels.size }
+  mainLoop (env : Environment) (game : Game) (levels : HashMap Nat GameLevel): IO Unit := do
---     mainLoop env game levels
+    let hIn ← IO.getStdin
---   let metaM : MetaM Unit := termElabM.run' (ctx := {})
+    let hOut ← IO.getStdout
---   discard <| metaM.run'.toIO coreCtx { env := env }
+    let hLog ← IO.getStderr
--- where
+    let m ← hIn.readGspMessage
---   mainLoop (env : Environment) (game : Game) (levels : HashMap Nat GameLevel): IO Unit := do
+    match m with
---     match ← Action.get with
+    | .request id "info" params =>
---     | Action.info => output (toJson game)
+      hOut.writeGspResponse ⟨id, game⟩
---     | Action.loadLevel n => runLevel env GameName levels n
+    | .request id "loadLevel" (some params) =>
---     | Action.quit => IO.Process.exit 0
+      match fromJson? (toJson (params)) with
---     | Action.invalid s => output s!"Invalid action: {s}"
+      | Except.ok (v : LoadLevelParams) =>
---     | _ => output "Invalid action"
+        runLevel id env GameName levels v.number
---     mainLoop env game levels
+      | Except.error inner =>
+        hLog.putStr s!"Invalid params: {inner}"
+        hLog.flush
+    | .request id m _ =>
+      hOut.writeGspResponseError
+        ⟨id, JsonRpc.ErrorCode.methodNotFound, s!"Method not found: {m}", none⟩
+    | _ =>
+      hLog.putStr s!"Invalid action: {toJson m}"
+      hLog.flush
+
+    mainLoop env game levels
 
 end Server

webpack.config.js

@@ -44,7 +44,6 @@ module.exports = env => {
     output: {
       path: path.resolve(__dirname, "client/dist/"),
       filename: "bundle.js",
-      sourceMapFilename: "[name].js.map"
     },
     devServer: {
       proxy: {