disable automatic compilation of lean files
This commit is contained in:
+1
-1
@@ -56,7 +56,7 @@
|
|||||||
},
|
},
|
||||||
"scripts": {
|
"scripts": {
|
||||||
"start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
|
"start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
|
||||||
"start_server": "cd server && NODE_ENV=development nodemon -e mjs,lean --exec \"(cd leanserver && lake build) && (cd testgame && lake exe cache get && lake build) && node ./index.mjs\"",
|
"start_server": "cd server && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"",
|
||||||
"start_client": "NODE_ENV=development webpack-dev-server --hot",
|
"start_client": "NODE_ENV=development webpack-dev-server --hot",
|
||||||
"build": "npm run build_server && npm run build_client",
|
"build": "npm run build_server && npm run build_client",
|
||||||
"build_server": "server/build.sh",
|
"build_server": "server/build.sh",
|
||||||
|
|||||||
+21
-13
@@ -38,19 +38,23 @@ if (isDevelopment) {
|
|||||||
const queue = []
|
const queue = []
|
||||||
const queueLength = 5
|
const queueLength = 5
|
||||||
|
|
||||||
|
function startServerProcess() {
|
||||||
|
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}`)
|
||||||
|
);
|
||||||
|
}
|
||||||
|
return serverProcess
|
||||||
|
}
|
||||||
|
|
||||||
/** start Lean Server processes to refill the queue */
|
/** start Lean Server processes to refill the queue */
|
||||||
function fillQueue() {
|
function fillQueue() {
|
||||||
while (queue.length < queueLength) {
|
while (queue.length < queueLength) {
|
||||||
const serverProcess = cp.spawn(cmd, cmdArgs, { cwd })
|
const serverProcess = startServerProcess()
|
||||||
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)
|
queue.push(serverProcess)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -58,9 +62,13 @@ function fillQueue() {
|
|||||||
fillQueue()
|
fillQueue()
|
||||||
|
|
||||||
wss.addListener("connection", function(ws) {
|
wss.addListener("connection", function(ws) {
|
||||||
|
let ps;
|
||||||
const ps = queue.shift() // Pick the first Lean process; it's likely to be ready immediately
|
if (isDevelopment) { // Don't use queue in development
|
||||||
fillQueue()
|
ps = startServerProcess()
|
||||||
|
} else {
|
||||||
|
ps = queue.shift() // Pick the first Lean process; it's likely to be ready immediately
|
||||||
|
fillQueue()
|
||||||
|
}
|
||||||
|
|
||||||
const socket = {
|
const socket = {
|
||||||
onMessage: (cb) => { ws.on("message", cb) },
|
onMessage: (cb) => { ws.on("message", cb) },
|
||||||
|
|||||||
Reference in New Issue
Block a user