Add line of contact for upload issues and set reserve disc space as environment variable.

.dockerignore

@@ -1,8 +0,0 @@
-node_modules
-client/dist
-games/
-server/.lake
-**/.DS_Store
-logs/
-relay/prev_cpu_metric
-test.ecosystem.config.cjs

Dockerfile

@@ -1,29 +0,0 @@
-FROM node:23-bookworm
-
-RUN apt update && apt upgrade -y
-RUN apt install -y bubblewrap
-
-WORKDIR /app
-
-# Install elan
-RUN curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz && \
-    ./elan-init -y
-
-ENV PATH="/root/.elan/bin:${PATH}"
-
-# Copy package files
-COPY package.json package-lock.json ./
-
-# Install dependencies
-RUN npm install
-
-# Copy project files
-COPY . .
-
-# Build the project
-RUN npm run build
-
-EXPOSE 8080
-
-# Set the entrypoint
-CMD ["npm", "run", "production"]

README.md

@@ -1,35 +1,3 @@
-# lean4game fork
-
-Questo è un fork di **lean4game** con supporto per essere self-hostato con Docker.
-
-## Deployment con Docker Compose
-
-Dopo aver clonato questa repo, per prima cosa serve creare [un token di API per GitHub](https://github.com/settings/developers) per permettere a lean4game di importare da solo i vari "game". Possiamo mettere questo token ed il nostro nome utente in un file `.env` come segue
-
-```
-export LEAN4GAME_GITHUB_USER='...'
-export LEAN4GAME_GITHUB_TOKEN='...'
-```
-
-poi per lanciare tutto con docker compose basta eseguire
-
-```bash
-$ source .env
-$ docker compose up -d
-```
-
-Questo comando lancierà lean4game su `http://locahost:8080`.
-
-### Aggiungere Giochi
-
-Per scaricare nuovi giochi basta fare una chiamata al seguente url
-
-- `https://{host}/import/trigger/{org}/{repo}` 
-
-Ad esempio per scaricare <https://github.com/leanprover-community/nng4> basta andare all'indirizzo `https://{host}/import/trigger/leanprover-community/nng4` per aggiungere _Natural Number Game_.
-
----
-
 # Lean 4 Game
 
 This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).

docker-compose.yml

@@ -1,14 +0,0 @@
-services:
-  lean4game:
-    build: .
-    privileged: true # needed to run bubblewrap inside docker
-    environment:
-      - LEAN4GAME_GITHUB_USER=${LEAN4GAME_GITHUB_USER}
-      - LEAN4GAME_GITHUB_TOKEN=${LEAN4GAME_GITHUB_TOKEN}
-    ports:
-      - "8080:8080"
-    volumes:
-      - games_data:/app/games
-
-volumes:
-  games_data:

ecosystem.config.cjs

@@ -6,6 +6,8 @@ module.exports = {
     env: {
       LEAN4GAME_GITHUB_USER: "",
       LEAN4GAME_GITHUB_TOKEN: "",
+      RES_DISC_SPACE_PERCENTAGE: 1.0,
+      ISSUE_CONTACT: "",
       NODE_ENV: "production",
       PORT: 8002
     },

relay/import.mjs

@@ -1,22 +1,26 @@
 import { spawn } from 'child_process'
-import fs from 'fs';
+import fs, { stat } from 'fs';
 import request from 'request'
 import requestProgress from 'request-progress'
 import { Octokit } from 'octokit';
 
 import { fileURLToPath } from 'url';
-import path from 'path';
+import path, { resolve } from 'path';
+import { error } from 'console';
 
 const __filename = fileURLToPath(import.meta.url);
 const __dirname = path.dirname(__filename);
 
 const TOKEN = process.env.LEAN4GAME_GITHUB_TOKEN
 const USERNAME = process.env.LEAN4GAME_GITHUB_USER
+const MEM_THRESHOLD = process.env.RES_DISC_SPACE_PERCENTAGE
+const CONTACT = process.env.ISSUE_CONTACT
 const octokit = new Octokit({
   auth: TOKEN
 })
 
 const progress = {}
+var exceedingMemoryLimit = false
 
 async function runProcess(id, cmd, args, cwd) {
   return new Promise((resolve, reject) => {
@@ -36,6 +40,28 @@ async function runProcess(id, cmd, args, cwd) {
   })
 }
 
+
+async function checkAgainstDiscMemory(artifact, maxPercentage) {
+  return new Promise((resolve, reject) => {
+  fs.statfs("/", (err, stats) => {
+    if (err) {
+      console.log(err);
+      reject()
+    }
+    let artifactBytes = artifact.size_in_bytes;
+    let totalBytes = stats.blocks * stats.bsize;
+    let freeBytes = stats.bfree * stats.bsize;
+    let usedBytes = totalBytes - freeBytes;
+    let maxUsedBytes = totalBytes * maxPercentage;
+    if (usedBytes + artifactBytes >= maxUsedBytes) {
+      exceedingMemoryLimit = true;
+    }
+    resolve()
+  });
+  })
+}
+
+
 async function download(id, url, dest) {
   return new Promise((resolve, reject) => {
     // The options argument is optional so you can omit it
@@ -49,7 +75,9 @@ async function download(id, url, dest) {
       }
     }))
     .on('progress', function (state) {
-      progress[id].output += `Downloaded ${Math.round(state.size.transferred/1024/1024)}MB\n`
+      console.log('progress', state);
+      transferredDataSize = Math.round(state.size.transferred/1024/1024)
+      progress[id].output += `Downloaded ${transferredDataSize}MB\n`
     })
     .on('error', function (err) {
       reject(err)
@@ -73,9 +101,16 @@ async function doImport (owner, repo, id) {
         '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)
+
+    await checkAgainstDiscMemory(artifact, MEM_THRESHOLD);
+
+    if (exceedingMemoryLimit === true) {
+      throw new Error(`Uploading file of size ${Math.round(artifact.size_in_bytes / 1024 / 1024)} (MB) would exceed allocated memory on the server.\n
+      Please notify server admins via <a href=${CONTACT}>the LEAN zulip instance</a> to resolve this issue.`);
+    }
+
     artifactId = artifact.id
     const url = artifact.archive_download_url
     // Make sure the download folder exists
@@ -91,7 +126,6 @@ async function doImport (owner, repo, id) {
 
     await runProcess(id, "/bin/bash", [path.join(__dirname, "unpack.sh"), artifactId, owner.toLowerCase(), repo.toLowerCase()], path.join(__dirname, ".."))
 
-
     // let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
     // manifest = JSON.parse(manifest);
     // if (manifest.length !== 1) {