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

NOTES.md

@@ -188,3 +188,10 @@ Activate config:
   sudo nginx -t
   sudo nginx -s reload
 ```
+
+
+## Install `unzip` for Importing Docker Images
+
+```
+sudo apt-get install unzip
+```

package.json

@@ -17,7 +17,6 @@
     "cytoscape-elk": "^2.1.0",
     "cytoscape-klay": "^3.1.4",
     "debounce": "^1.2.1",
-    "decompress": "^4.2.1",
     "express": "^4.18.2",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
     "lean4web": "github:hhu-adam/lean4web",

server/import.mjs

@@ -1,10 +1,15 @@
 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';
 
+import { fileURLToPath } from 'url';
+import path from 'path';
+
+const __filename = fileURLToPath(import.meta.url);
+const __dirname = path.dirname(__filename);
+
 const TOKEN = process.env.LEAN4GAME_GITHUB_TOKEN
 const octokit = new Octokit({
   auth: TOKEN
@@ -77,11 +82,7 @@ async function doImport (owner, repo, id) {
     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`)
+    await runProcess(id, "/bin/bash", [`${__dirname}/unpack.sh`, artifactId],".")
     let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
     manifest = JSON.parse(manifest);
     if (manifest.length !== 1) {

server/unpack.sh

@@ -0,0 +1,13 @@
+#/bin/bash
+
+ARTIFACT_ID=$1
+
+echo "Unpacking ZIP."
+unzip -o tmp/artifact_${ARTIFACT_ID}.zip -d tmp/artifact_${ARTIFACT_ID}
+echo "Unpacking TAR."
+for f in tmp/artifact_${ARTIFACT_ID}/* #Should only be one file
+do
+  echo "Unpacking $f"
+  mkdir tmp/artifact_${ARTIFACT_ID}_inner
+  tar -xvf $f -C tmp/artifact_${ARTIFACT_ID}_inner
+done