support arbitrary docker containers as games

pull/79/head
Alexander Bentkamp 3 years ago
parent 161c88d58f
commit 9ba5acef4d

@ -16,7 +16,7 @@ function App() {
const params = useParams();
return (
<div className="app">
<GameIdContext.Provider value={params.gameId}>
<GameIdContext.Provider value={"g/" + params.owner + "/" + params.repo}>
<Outlet />
</GameIdContext.Provider>
</div>

@ -23,7 +23,7 @@
<div class="game-list">
<div class="game" onclick="location.href='#/game/adam';" style="cursor: pointer;">
<div class="game" onclick="location.href='#/g/hhu-adam/Robo';" style="cursor: pointer;">
<div class="wrapper">
<div class="title">Formaloversum</div>
<div class="short-description">Erkunde das Leansche Universum mit deinem Robo,
@ -66,7 +66,7 @@
</table>
</div>
<div class="game" onclick="location.href='#/game/nng';" style="cursor: pointer;">
<div class="game" onclick="location.href='#/g/hhu-adam/NNG4';" style="cursor: pointer;">
<div class="wrapper">
<div class="title">Natural Number Game</div>
<div class="short-description">

@ -47,8 +47,7 @@ function GameTile({
let navigate = useNavigate();
const routeChange = () =>{
let path = `game/${gameId}`;
navigate(path);
navigate(gameId);
}
return <div className="game" onClick={routeChange}>
@ -108,7 +107,7 @@ function LandingPage() {
<GameTile
title="Formaloversum"
gameId="adam"
gameId="g/hhu-adam/Robo"
intro="Erkunde das Leansche Universum mit deinem Robo, welcher dir bei der Verständigung mit den Formalosophen zur Seite steht."
description="
Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet danach verschiedene Bereiche des Bachelorstudiums an.
@ -120,7 +119,7 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet
<GameTile
title="Natural Number Game"
gameId="nng"
gameId="g/hhu-adam/NNG4"
intro="The classical introduction game for Lean."
description="In this game you recreate the natural numbers $\mathbb{N}$ from the Peano axioms,
learning the basics about theorem proving in Lean.

@ -221,8 +221,8 @@ function PlayableLevel({worldId, levelId}) {
</div>
}
{levelId >= gameInfo.data?.worldSize[worldId] ?
<Button to={`/game/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
<Button to={`/game/${gameId}/world/${worldId}/level/${levelId + 1}`}>
<Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
<Button to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}>
Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>}
</div>}
@ -257,8 +257,8 @@ function Introduction({worldId}) {
</div>
<div className="conclusion">
{0 == gameInfo.data?.worldSize[worldId] ?
<Button to={`/game/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
<Button to={`/game/${gameId}/world/${worldId}/level/1`}>
<Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
<Button to={`/${gameId}/world/${worldId}/level/1`}>
Start&nbsp;<FontAwesomeIcon icon={faArrowRight} />
</Button>}
</div>
@ -272,7 +272,7 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle}) {
return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
<div>
<Button to={`/game/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button>
<Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button>
<span className="app-bar-title">
{gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
</span>
@ -282,10 +282,10 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle}) {
{levelTitle}
</span>
<Button disabled={levelId <= 0} inverted={true}
to={`/game/${gameId}/world/${worldId}/level/${levelId - 1}`}
to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
><FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous</Button>
<Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} inverted={true}
to={`/game/${gameId}/world/${worldId}/level/${levelId + 1}`}
to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}
>Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>
</div>

@ -39,7 +39,7 @@ function LevelIcon({ worldId, levelId, position }) {
// TODO: relative positioning?
return (
<Link to={`/game/${gameId}/world/${worldId}/level/${levelId}`}>
<Link to={`/${gameId}/world/${worldId}/level/${levelId}`}>
<circle fill={completed ? "green" :"#999"} cx={x} cy={y} r={r} />
</Link>
)
@ -76,13 +76,13 @@ function Welcome() {
for (let i = 1; i <= gameInfo.data.worldSize[id]; i++) {
svgElements.push(
<LevelIcon
key={`/game/${gameId}/world/${id}/level/${i}`}
key={`/${gameId}/world/${id}/level/${i}`}
position={position} worldId={id} levelId={i} />
)
}
svgElements.push(
<Link key={`world${id}`} to={`/game/${gameId}/world/${id}/level/0`}>
<Link key={`world${id}`} to={`/${gameId}/world/${id}/level/0`}>
<circle className="world-circle" cx={s*position.x} cy={s*position.y} r={R}
fill="#1976d2"/>
<foreignObject className="world-title-wrapper" x={s*position.x} y={s*position.y}

@ -22,19 +22,18 @@ const router = createHashRouter([
{
path: "/",
element: <LandingPage />,
// loader: () => redirect("/game/adam")
},
{
path: "/game/:gameId",
path: "/g/:owner/:repo",
element: <App />,
errorElement: <ErrorPage />,
children: [
{
path: "/game/:gameId",
path: "/g/:owner/:repo",
element: <Welcome />,
},
{
path: "/game/:gameId/world/:worldId/level/:levelId",
path: "/g/:owner/:repo/world/:worldId/level/:levelId",
element: <Level />,
},
],

@ -66,10 +66,10 @@
"start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
"start_server": "cd server && lake build && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"",
"start_client": "NODE_ENV=development webpack-dev-server --hot",
"build": "npm run build_server && npm run build_client",
"build_server": "server/build.sh",
"build_client": "NODE_ENV=production webpack",
"build": "NODE_ENV=production webpack",
"production": "NODE_ENV=production node server/index.mjs",
"build_robo": "rm -rf ./Robo && git clone https://github.com/hhu-adam/Robo && docker build ./Robo --file ./Robo/Dockerfile --tag github-hhu-adam:Robo && rm -rf ./Robo",
"build_nng": "rm -rf ./NNG4 && git clone https://github.com/hhu-adam/NNG4 && docker build ./NNG4 --file ./NNG4/Dockerfile --tag github-hhu-adam:NNG4 && rm -rf ./NNG4",
"update_lean": "./UPDATE_LEAN.sh"
},
"eslintConfig": {

@ -1,22 +0,0 @@
#!/usr/bin/env sh
# Operate in the directory where this file is located
cd $(dirname $0)
# Build Adam
( rm -rf adam
git clone https://github.com/hhu-adam/Robo adam/
cd adam
docker rmi adam:latest || true
docker build \
--rm -f Dockerfile -t adam:latest .
)
# Build NNG
( rm -rf nng
git clone https://github.com/hhu-adam/NNG4 nng/
cd nng
docker rmi nng:latest || true
docker build \
--rm -f Dockerfile -t nng:latest .
)

@ -9,14 +9,20 @@ import os from 'os';
import anonymize from 'ip-anonymize';
import { importTrigger, importStatus } from './import.mjs'
/** Preloaded games. The keys refer to the docker tags of the virtual machines.
* The number `queueLength` determines how many instances of the docker container
* get started before any user shows up to have them up and running immediately.
* The values `name`, `module`, and `dir` are just used for development where we
* use a project directory instead of a docker container.
*/
const games = {
adam: {
"github-hhu-adam:Robo": {
name: "Adam",
module: "Adam",
dir: "../../../../Robo",
queueLength: 5
},
nng: {
"github-hhu-adam:NNG4": {
name: "NNG",
module: "NNG",
dir: "../../../../NNG4",
@ -50,17 +56,18 @@ const isDevelopment = environment === 'development'
/** We keep queues of started Lean Server processes to be ready when a user arrives */
const queue = {}
const queueLength = 5
function startServerProcess(gameId) {
const serverProcess = isDevelopment
? cp.spawn("./gameserver",
["--server", games[gameId].dir, games[gameId].module, games[gameId].name],
function startServerProcess(tag) {
let serverProcess
if (isDevelopment && games[tag]?.dir) {
serverProcess = cp.spawn("./gameserver",
["--server", games[tag].dir, games[tag].module, games[tag].name],
{ cwd: "./build/bin/" })
: cp.spawn("docker",
["run", "--runtime=runsc", "--network=none", "--rm", "-i", `${gameId}:latest`,
"./gameserver", "--server", "/game/", games[gameId].module, games[gameId].name],
} else {
serverProcess = cp.spawn("docker",
["run", "--runtime=runsc", "--network=none", "--rm", "-i", `${tag}`],
{ cwd: "." })
}
serverProcess.on('error', error =>
console.error(`Launching Lean Server failed: ${error}`)
);
@ -73,32 +80,35 @@ function startServerProcess(gameId) {
}
/** start Lean Server processes to refill the queue */
function fillQueue(gameId) {
while (queue[gameId].length < games[gameId].queueLength) {
const serverProcess = startServerProcess(gameId)
queue[gameId].push(serverProcess)
function fillQueue(tag) {
while (queue[tag].length < games[tag].queueLength) {
const serverProcess = startServerProcess(tag)
queue[tag].push(serverProcess)
}
}
for (let gameId in games) {
queue[gameId] = []
fillQueue(gameId)
if (!isDevelopment) { // Don't use queue in development
for (let tag in games) {
queue[tag] = []
fillQueue(tag)
}
}
const urlRegEx = new RegExp("^/websocket/(.*)$")
const urlRegEx = /^\/websocket\/g\/([\w.-]+)\/([\w.-]+)$/
wss.addListener("connection", function(ws, req) {
const reRes = urlRegEx.exec(req.url)
if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; }
const gameId = reRes[1]
if (!games[gameId]) { console.error(`Unknown game: ${gameId}`); return; }
const owner = reRes[1]
const repo = reRes[2]
const tag = `github-${owner}:${repo}`
let ps;
if (isDevelopment) { // Don't use queue in development
ps = startServerProcess(gameId)
if (!queue[tag] || queue[tag].length == 0) {
ps = startServerProcess(tag)
} else {
ps = queue[gameId].shift() // Pick the first Lean process; it's likely to be ready immediately
fillQueue(gameId)
ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately
fillQueue(tag)
}
socketCounter += 1;

Loading…
Cancel
Save