Merge branch 'main' of github.com:leanprover-community/lean4game

2023-05-13 15:21:13 +02:00
parent c6e224dc40 6cda39a778
commit 572be60c65
12 changed files with 1593 additions and 252 deletions
@@ -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 .
-)
@@ -0,0 +1,128 @@
+import { spawn } from 'child_process'
+import fs from 'fs';
+import request from 'request'
+import decompress from 'decompress'
+import requestProgress from 'request-progress'
+import { Octokit } from 'octokit';
+
+const TOKEN = process.env.LEAN4GAME_GITHUB_TOKEN
+const octokit = new Octokit({
+  auth: TOKEN
+})
+
+const progress = {}
+
+async function runProcess(id, cmd, args, cwd) {
+  return new Promise((resolve, reject) => {
+    const ls = spawn(cmd, args, {cwd});
+
+    ls.stdout.on('data', (data) => {
+      progress[id].output += data.toString()
+    });
+
+    ls.stderr.on('data', (data) => {
+      progress[id].output += data.toString()
+    });
+
+    ls.on('close', (code) => {
+      resolve()
+    });
+  })
+}
+
+async function download(id, url, dest) {
+  return new Promise((resolve, reject) => {
+    // The options argument is optional so you can omit it
+    requestProgress(request({
+      url,
+      headers: {
+        'User-Agent': 'abentkamp',
+        'X-GitHub-Api-Version': '2022-11-28',
+        'Authorization': 'Bearer '+TOKEN
+      }
+    }))
+    .on('progress', function (state) {
+      progress[id].output += `Downloaded ${Math.round(state.size.transferred/1024/1024)}MB\n`
+    })
+    .on('error', function (err) {
+      reject(err)
+    })
+    .on('end', function () {
+      resolve()
+    })
+    .pipe(fs.createWriteStream(dest));
+  })
+}
+
+async function doImport (owner, repo, id) {
+  progress[id].output += `Import starting in a few seconds...\n`
+  await new Promise(resolve => setTimeout(resolve, 3000))
+  let artifactId = null
+  try {
+    const artifacts = await octokit.request('GET /repos/{owner}/{repo}/actions/artifacts', {
+      owner,
+      repo,
+      headers: {
+        'X-GitHub-Api-Version': '2022-11-28'
+      }
+    })
+    // choose latest artifact
+    const artifact = artifacts.data.artifacts
+      .reduce((acc, cur) => acc.created_at < cur.created_at ? cur : acc)
+    artifactId = artifact.id
+    const url = artifact.archive_download_url
+    if (!fs.existsSync("tmp")){
+      fs.mkdirSync("tmp");
+    }
+    progress[id].output += `Download from ${url}\n`
+    await download(id, url, `tmp/artifact_${artifactId}.zip`)
+    progress[id].output += `Download finished.\n`
+    progress[id].output += `Unpacking ZIP.\n`
+    const files = await decompress(`tmp/artifact_${artifactId}.zip`, `tmp/artifact_${artifactId}`)
+    if (files.length != 1) { throw Error(`Unexpected number of files in ZIP: ${files.length}`) }
+    progress[id].output += `Unpacking TAR.\n`
+    const files_inner = await decompress(`tmp/artifact_${artifactId}/${files[0].path}`, `tmp/artifact_${artifactId}_inner`)
+    let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
+    manifest = JSON.parse(manifest);
+    if (manifest.length !== 1) {
+      throw `Unexpected manifest: ${JSON.stringify(manifest)}`
+    }
+    manifest[0].RepoTags = [`github-${owner}:${repo}`]
+    fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest));
+    await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`)
+    await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`])
+    progress[id].done = true
+    progress[id].output += `Done.\n`
+  } catch (e) {
+    progress[id].output += `Error: ${e.toString()}\n${e.stack}`
+  } finally {
+    if (artifactId) {
+      fs.rmSync(`tmp/artifact_${artifactId}.zip`, {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}`, {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}_inner`, {force: true, recursive: true});
+      fs.rmSync(`tmp/archive_${artifactId}.tar`, {force: true, recursive: true});
+    }
+    progress[id].done = true
+  }
+}
+
+export const importTrigger = (req, res) => {
+  const owner = req.params.owner
+  const repo = req.params.repo
+  const id = req.params.owner + '/' + req.params.repo
+  if(!/^[\w.-]+\/[\w.-]+$/.test(id)) { res.send(`Invalid repo name ${id}`); return }
+
+  if(!progress[id] || progress[id].done) {
+    progress[id] = {output: "", done: false}
+    doImport(owner, repo, id)
+  }
+
+  res.redirect(`/import/status/${owner}/${repo}`)
+}
+
+export const importStatus = (req, res) => {
+  const owner = req.params.owner
+  const repo = req.params.repo
+  const id = req.params.owner + '/' + req.params.repo
+  res.send(`<html><head><meta http-equiv="refresh" content="5"></head><body><pre>${progress[id]?.output ?? "Nothing here."}</pre></body></html>`)
+}
@@ -7,15 +7,22 @@ import * as rpc from 'vscode-ws-jsonrpc';
 import * as jsonrpcserver from 'vscode-ws-jsonrpc/server';
 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",
@@ -30,8 +37,14 @@ const app = express()

 const PORT = process.env.PORT || 8080;

+var router = express.Router();
+
+router.get('/import/status/:owner/:repo', importStatus)
+router.get('/import/trigger/:owner/:repo', importTrigger)
+
 const server = app
  .use(express.static(path.join(__dirname, '../client/dist/')))
+  .use('/', router)
  .listen(PORT, () => console.log(`Listening on ${PORT}`));

 const wss = new WebSocketServer({ server })
@@ -43,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}`)
    );
@@ -66,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;