diff --git a/server/index.mjs b/server/index.mjs index 30a91de..9c0c394 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -1,7 +1,7 @@ import { WebSocketServer } from 'ws'; import express from 'express' import path from 'path' -import { spawn } from 'child_process'; +import * as cp from 'child_process'; import * as url from 'url'; import * as rpc from 'vscode-ws-jsonrpc'; import * as jsonrpcserver from 'vscode-ws-jsonrpc/server'; @@ -34,7 +34,34 @@ if (isDevelopment) { cwd = "." } +/** We keep a queue of started Lean Server processes to be ready when a user arrives */ +const queue = [] +const queueLength = 5 + +/** start Lean Server processes to refill the queue */ +function fillQueue() { + while (queue.length < queueLength) { + const serverProcess = cp.spawn(cmd, cmdArgs, { cwd }) + serverProcess.on('error', error => + console.error(`Launching Lean Server failed: ${error}`) + ); + if (serverProcess.stderr !== null) { + serverProcess.stderr.on('data', data => + console.error(`Lean Server: ${data}`) + ); + } + + queue.push(serverProcess) + } +} + +fillQueue() + wss.addListener("connection", function(ws) { + + const ps = queue.shift() // Pick the first Lean process; it's likely to be ready immediately + fillQueue() + const socket = { onMessage: (cb) => { ws.on("message", cb) }, onError: (cb) => { ws.on("error", cb) }, @@ -44,7 +71,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, { cwd }); + const serverConnection = jsonrpcserver.createProcessStreamConnection(ps); socketConnection.forward(serverConnection, message => { console.log(`CLIENT: ${JSON.stringify(message)}`) return message; diff --git a/server/leanserver/GameServer/Watchdog.lean b/server/leanserver/GameServer/Watchdog.lean index bc0e09d..8c6fa10 100644 --- a/server/leanserver/GameServer/Watchdog.lean +++ b/server/leanserver/GameServer/Watchdog.lean @@ -102,6 +102,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do let i ← maybeTee "wdIn.txt" false i let o ← maybeTee "wdOut.txt" true o let e ← maybeTee "wdErr.txt" true e + let state := {env := ← createEnv, game := `TestGame} let initRequest ← i.readLspRequestAs "initialize" InitializeParams o.writeLspResponse { id := initRequest.id @@ -114,7 +115,6 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do : InitializeResult } } - let state := {env := ← createEnv, game := `TestGame} let context : ServerContext := { hIn := i hOut := o