diff --git a/client/src/App.tsx b/client/src/App.tsx index 02de1d9..400eb2b 100644 --- a/client/src/App.tsx +++ b/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) 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; - // if (finished) { - // mainComponent = - // } else if (curLevel > 0) { - // mainComponent = - // } else { - // mainComponent = - // } + let mainComponent; + if (finished) { + mainComponent = + } else if (curLevel > 0) { + mainComponent = + } else { + mainComponent = + } return (
@@ -79,7 +75,7 @@ function App() { - {/* {mainComponent} */} + {mainComponent}
) diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index aa9bbfb..b2ae295 100644 --- a/client/src/components/Level.tsx +++ b/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({ sendJsonMessage, lastMessage, lastJsonMessage, nbLevels, level, setCurLevel, setLevelTitle, setFinished }) { +function Level({ rpcConnection, nbLevels, level, setCurLevel, setLevelTitle, setFinished }: LevelProps) { 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 - useEffect(() => { - sendJsonMessage({ "loadLevel": level }); - }, [level, sendJsonMessage]) - - // 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"]) + const processResponse = (res:any) => { + setLeanData(res); + setErrors(res.errors); + if (res.message !== "" && res.errors?.length === 0) { + setMessage(res.message) setMessageOpen(true) } - setLeanData(data); - setErrors(data.errors); - if (data.goals.length === 0 && data.errors.length === 0) { + if (res.goals?.length === 0 && res.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 \ No newline at end of file +export default Level diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx index c231385..47ebb74 100644 --- a/client/src/components/Welcome.tsx +++ b/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; +} + +type infoResultType = { + title: string, + nb_levels: any[], + conclusion: string +} -function Welcome({ sendJsonMessage, lastJsonMessage, lastMessage, setNbLevels, setTitle, startGame, setConclusion }) { +const infoRequestType = new rpc.RequestType0("info") - const [leanData, setLeanData] = useState({}) +function Welcome({ rpcConnection, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) { - // Will run at the very beginning - useEffect(() => { - sendJsonMessage('info') - }, [sendJsonMessage]) + const [leanData, setLeanData] = useState(null) - // Will run when a Json message arrives useEffect(() => { - if (lastJsonMessage != null && lastJsonMessage.hasOwnProperty("nb_levels")) { - setLeanData(lastJsonMessage) - setNbLevels(lastJsonMessage.nb_levels) - setTitle(lastJsonMessage.title) - document.title = lastJsonMessage.title - setConclusion(lastJsonMessage.conclusion) + if (rpcConnection) { // Will run in the beginning as soon as RPC connection is established + rpcConnection.sendRequest(infoRequestType).then((res: infoResultType) =>{ + setLeanData(res) + setNbLevels(res.nb_levels) + setTitle(res.title) + document.title = res.title + setConclusion(res.conclusion) + }); } - }, [lastJsonMessage, setNbLevels, setTitle, setConclusion]) + }, [rpcConnection, setLeanData, setNbLevels, setTitle, setConclusion]) let content - if ("introduction" in leanData) { + if (leanData) { content = ( diff --git a/server/index.js b/server/index.js index fb3c9cf..84f7fa9 100644 --- a/server/index.js +++ b/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"))); }) diff --git a/server/leanserver/GameServer/Communication.lean b/server/leanserver/GameServer/Communication.lean index 210abc9..a149cdf 100644 --- a/server/leanserver/GameServer/Communication.lean +++ b/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 "\n" + h.putStr ((toJson m).compress ++ "\n") + h.flush def writeGspRequest (h : FS.Stream) (r : Request α) : IO Unit := h.writeGspMessage r diff --git a/server/leanserver/GameServer/Server.lean b/server/leanserver/GameServer/Server.lean index 6eb0edb..0f49556 100644 --- a/server/leanserver/GameServer/Server.lean +++ b/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 - | Action.runTactic tac => do let resp ← runTactic tac; output s!"{← resp.toJson}" - | Action.loadLevel n => runLevel env GameName levels n - | Action.undo => do modify fun s => s.pop; output s!"{← (← mkResponse).toJson}" - | Action.restartLevel => runLevel env GameName levels idx - | Action.prev => runLevel env GameName levels idx.pred - | Action.next => runLevel env GameName levels idx.succ - | Action.quit => IO.Process.exit 0 - | Action.restartGame => output "Can't restart game now" - | Action.info => output "Can't get info now" - | Action.invalid s => output s!"{← { ← mkResponse with errors := #[s!"Invalid action: {s}"] : Response}.toJson}" + let hIn ← IO.getStdin + let hOut ← IO.getStdout + let hLog ← IO.getStderr + let m ← hIn.readGspMessage + match m with + | .request id "runTactic" params => do + match fromJson? (toJson (params)) with + | Except.ok (v : RunTacticParams) => + let resp ← runTactic v.tactic + hOut.writeGspResponse ⟨id, ← resp.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 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 + 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 + let hIn ← IO.getStdin + let hOut ← IO.getStdout + let hLog ← IO.getStderr + let m ← hIn.readGspMessage + match m with + | .request id "info" params => + hOut.writeGspResponse ⟨id, game⟩ + | .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 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 diff --git a/webpack.config.js b/webpack.config.js index 76a9e1e..244e4bd 100644 --- a/webpack.config.js +++ b/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: {