some stuff

client/public/worker.js

@@ -0,0 +1,93 @@
+var stderrBuffer = ""
+var messageBuffer = []
+var initialized = false;
+var flushing = false;
+
+var headerMode = true;
+var header="";
+var re = /Content-Length: (\d+)\r\n/i;
+var contentLength = 0;
+var content = []
+var utf8decoder = new TextDecoder();
+
+
+function flushMessageBuffer(){
+  if (initialized && !flushing) {
+    while(messageBuffer.length > 0) {
+      flushing = true;
+      var msg = messageBuffer.shift();
+      console.log(`Send message: ${msg}`);
+      Module.ccall('send_message', 'void', ['string'], [msg]);
+      console.log(`Message done: ${msg}`);
+    }
+    flushing = false;
+  }
+}
+
+var Module = {
+  "arguments": ["--worker"],
+  "preRun": [function() {
+    function stdin() {
+      return null;
+    }
+
+    function stdout(asciiCode) {
+      if (headerMode) {
+        header += String.fromCharCode(asciiCode)
+        if (header.endsWith('\r\n\r\n')) {
+          const found = header.match(re)
+          if (found == null) { console.error(`Invalid header: ${header}`) }
+          contentLength = parseInt(found[1])
+          content = []
+          headerMode = false
+        }
+      } else {
+        content.push(asciiCode)
+        if (content.length == contentLength) {
+          const message = utf8decoder.decode(new Uint8Array(content))
+          console.log(`Server: ${message}`)
+          postMessage(message);
+          headerMode = true
+          header = ''
+        }
+      }
+    }
+
+    function stderr(asciiCode) {
+      stderrBuffer += String.fromCharCode(asciiCode)
+    }
+
+    FS.init(stdin, stdout, stderr);
+  }],
+  "noInitialRun": true,
+  "onRuntimeInitialized": () => {
+    Module.ccall('main', 'void', [], []);
+    initialized = true;
+    if (stderrBuffer !== "") {
+      console.log(stderrBuffer);
+      stderrBuffer = ""
+    }
+    flushMessageBuffer();
+  }
+};
+
+importScripts("server.js")
+
+
+
+onmessage = (ev) => {
+  console.log(`Client: ${ev.data}`)
+  messageBuffer.push(ev.data);
+  flushMessageBuffer();
+}
+
+setInterval(() => {
+  if (stderrBuffer !== "") {
+    console.log(stderrBuffer);
+    stderrBuffer = ""
+  }
+}, 1000)
+
+setTimeout(() =>{
+
+},2000)

client/src/wasm.ts

@@ -0,0 +1,339 @@
+import { DataCallback, AbstractMessageReader, MessageReader } from 'vscode-jsonrpc/lib/common/messageReader.js';
+
+import { Message } from 'vscode-jsonrpc/lib/common/messages.js';
+import { AbstractMessageWriter, MessageWriter } from 'vscode-jsonrpc/lib/common/messageWriter.js';
+import { Emitter } from 'vscode-jsonrpc/lib/common/events.js';
+import { Disposable, IWebSocket } from 'vscode-ws-jsonrpc/.';
+
+declare var IO: any;
+
+export class WasmWriter implements MessageWriter {
+  protected errorCount = 0;
+  errorEmitter
+  closeEmitter
+  constructor(private worker: Worker) {
+    this.errorEmitter = new Emitter()
+    this.closeEmitter = new Emitter()
+}
+dispose() {
+    this.errorEmitter.dispose();
+    this.closeEmitter.dispose();
+}
+get onError() {
+    return this.errorEmitter.event;
+}
+fireError(error, message, count) {
+    this.errorEmitter.fire([this.asError(error), message, count]);
+}
+get onClose() {
+    return this.closeEmitter.event;
+}
+fireClose() {
+    this.closeEmitter.fire(undefined);
+}
+asError(error) {
+    if (error instanceof Error) {
+        return error;
+    }
+    else {
+        return new Error(`Writer received error. Reason: ${error.message}`);
+    }
+}
+
+  end(): void {
+  }
+
+  async write(msg: Message): Promise<void> {
+      try {
+          const content = JSON.stringify(msg);
+          this.worker.postMessage(content)
+      } catch (e) {
+          this.errorCount++;
+          this.fireError(e, msg, this.errorCount);
+      }
+  }
+}
+
+
+export class WasmReader implements MessageReader {
+  protected state: 'initial' | 'listening' | 'closed' = 'initial';
+  protected callback: DataCallback | undefined;
+  protected readonly events: { message?: any, error?: any }[] = [];
+
+  constructor(private worker: Worker) {
+    this.worker.onmessage = (ev) => {
+      this.readMessage(ev.data)
+    }
+      // this.socket.onMessage(message =>
+      //     this.readMessage(message)
+      // );
+      // this.socket.onError(error =>
+      //     this.fireError(error)
+      // );
+      // this.socket.onClose((code, reason) => {
+      //     if (code !== 1000) {
+      //         const error: Error = {
+      //             name: '' + code,
+      //             message: `Error during socket reconnect: code = ${code}, reason = ${reason}`
+      //         };
+      //         this.fireError(error);
+      //     }
+      //     this.fireClose();
+      // });
+    this.errorEmitter = new Emitter()
+    this.closeEmitter = new Emitter()
+    this.partialMessageEmitter = new Emitter()
+  }
+
+  protected errorCount = 0;
+  errorEmitter
+  closeEmitter
+  partialMessageEmitter
+
+dispose() {
+    this.errorEmitter.dispose();
+    this.closeEmitter.dispose();
+}
+get onError() {
+    return this.errorEmitter.event;
+}
+get onClose() {
+    return this.closeEmitter.event;
+}
+get onPartialMessage() {
+    return this.partialMessageEmitter.event;
+}
+firePartialMessage(info) {
+    this.partialMessageEmitter.fire(info);
+}
+asError(error) {
+    if (error instanceof Error) {
+        return error;
+    }
+    else {
+        return new Error(`Reader received error. Reason: ${error.message ? error.message : 'unknown'}`);
+    }
+}
+
+  listen(callback: DataCallback): Disposable {
+      if (this.state === 'initial') {
+          this.state = 'listening';
+          this.callback = callback;
+          while (this.events.length !== 0) {
+              const event = this.events.pop()!;
+              if (event.message) {
+                  this.readMessage(event.message);
+              } else if (event.error) {
+                  this.fireError(event.error);
+              } else {
+                  this.fireClose();
+              }
+          }
+      }
+      return {
+          dispose: () => {
+              if (this.callback === callback) {
+                  this.callback = undefined;
+              }
+          }
+      };
+  }
+
+  protected readMessage(message: any): void {
+      if (this.state === 'initial') {
+          this.events.splice(0, 0, { message });
+      } else if (this.state === 'listening') {
+          try {
+              const data = JSON.parse(message);
+              this.callback!(data);
+          } catch (err) {
+              const error: Error = {
+                  name: '' + 400,
+                  message: `Error during message parsing, reason = ${typeof err === 'object' ? (err as any).message : 'unknown'}`
+              };
+              this.fireError(error);
+          }
+      }
+  }
+
+  protected fireError(error: any): void {
+      if (this.state === 'initial') {
+          this.events.splice(0, 0, { error });
+      } else if (this.state === 'listening') {
+
+    this.errorEmitter.fire(this.asError(error));
+      }
+  }
+
+  protected fireClose(): void {
+      if (this.state === 'initial') {
+          this.events.splice(0, 0, {});
+      } else if (this.state === 'listening') {
+        this.closeEmitter.fire(undefined);
+      }
+      this.state = 'closed';
+  }
+}
+export class WebSocketMessageWriter implements MessageWriter {
+    protected errorCount = 0;
+    errorEmitter
+    closeEmitter
+
+    constructor(protected readonly socket: IWebSocket) {
+        this.errorEmitter = new Emitter();
+        this.closeEmitter = new Emitter();
+    }
+    dispose() {
+        this.errorEmitter.dispose();
+        this.closeEmitter.dispose();
+    }
+    get onError() {
+        return this.errorEmitter.event;
+    }
+    fireError(error, message, count) {
+        this.errorEmitter.fire([this.asError(error), message, count]);
+    }
+    get onClose() {
+        return this.closeEmitter.event;
+    }
+    fireClose() {
+        this.closeEmitter.fire(undefined);
+    }
+    asError(error) {
+        if (error instanceof Error) {
+            return error;
+        }
+        else {
+            return new Error(`Writer received error. Reason: ${(error.message) ? error.message : 'unknown'}`);
+        }
+    }
+    end(): void {
+    }
+
+    async write(msg: Message): Promise<void> {
+        console.log("WRITE",msg)
+        try {
+            const content = JSON.stringify(msg);
+            this.socket.send(content);
+        } catch (e) {
+            this.errorCount++;
+            this.fireError(e, msg, this.errorCount);
+        }
+    }
+}
+
+
+
+export class WebSocketMessageReader implements MessageReader {
+    protected state: 'initial' | 'listening' | 'closed' = 'initial';
+    protected callback: DataCallback | undefined;
+    protected readonly events: { message?: any, error?: any }[] = [];
+    errorEmitter
+    closeEmitter
+    partialMessageEmitter
+
+    constructor(protected readonly socket: IWebSocket) {
+        this.errorEmitter = new Emitter();
+        this.closeEmitter = new Emitter();
+        this.partialMessageEmitter = new Emitter();
+        this.socket.onMessage(message =>{
+            console.log("READ", message)
+            this.readMessage(message)
+        });
+        this.socket.onError(error =>
+            this.fireError(error)
+        );
+        this.socket.onClose((code, reason) => {
+            if (code !== 1000) {
+                const error: Error = {
+                    name: '' + code,
+                    message: `Error during socket reconnect: code = ${code}, reason = ${reason}`
+                };
+                this.fireError(error);
+            }
+            this.fireClose();
+        });
+    }
+    dispose() {
+        this.errorEmitter.dispose();
+        this.closeEmitter.dispose();
+    }
+    get onError() {
+        return this.errorEmitter.event;
+    }
+    get onClose() {
+        return this.closeEmitter.event;
+    }
+    get onPartialMessage() {
+        return this.partialMessageEmitter.event;
+    }
+    firePartialMessage(info) {
+        this.partialMessageEmitter.fire(info);
+    }
+    asError(error) {
+        if (error instanceof Error) {
+            return error;
+        }
+        else {
+            return new Error(`Reader received error. Reason: ${(error.message) ? error.message : 'unknown'}`);
+        }
+    }
+
+    listen(callback: DataCallback): Disposable {
+        if (this.state === 'initial') {
+            this.state = 'listening';
+            this.callback = callback;
+            while (this.events.length !== 0) {
+                const event = this.events.pop()!;
+                if (event.message) {
+                    this.readMessage(event.message);
+                } else if (event.error) {
+                    this.fireError(event.error);
+                } else {
+                    this.fireClose();
+                }
+            }
+        }
+        return {
+            dispose: () => {
+                if (this.callback === callback) {
+                    this.callback = undefined;
+                }
+            }
+        };
+    }
+
+    protected readMessage(message: any): void {
+        if (this.state === 'initial') {
+            this.events.splice(0, 0, { message });
+        } else if (this.state === 'listening') {
+            try {
+                const data = JSON.parse(message);
+                this.callback!(data);
+            } catch (err) {
+                const error: Error = {
+                    name: '' + 400,
+                    message: `Error during message parsing, reason = ${typeof err === 'object' ? (err as any).message : 'unknown'}`
+                };
+                this.fireError(error);
+            }
+        }
+    }
+
+    protected fireError(error: any): void {
+        if (this.state === 'initial') {
+            this.events.splice(0, 0, { error });
+        } else if (this.state === 'listening') {
+            this.errorEmitter.fire(this.asError(error));
+        }
+    }
+
+    protected fireClose(): void {
+        if (this.state === 'initial') {
+            this.events.splice(0, 0, {});
+        } else if (this.state === 'listening') {
+            this.closeEmitter.fire(undefined);
+        }
+        this.state = 'closed';
+    }
+}

index.html

@@ -33,6 +33,7 @@
       </p>
     </div>
   </noscript>
+  <script src="coi-serviceworker.js"></script>
   <script type="module" src="/client/src/index.tsx"></script>
 </body>
 

package-lock.json

@@ -24,6 +24,7 @@
         "@types/cytoscape": "^3.19.9",
         "@types/react-router-dom": "^5.3.3",
         "@vitejs/plugin-react-swc": "^3.4.0",
+        "coi-serviceworker": "^0.1.7",
         "cross-env": "^7.0.3",
         "cytoscape": "^3.23.0",
         "cytoscape-elk": "^2.1.0",
@@ -6533,6 +6534,11 @@
         "node": ">=6"
       }
     },
+    "node_modules/coi-serviceworker": {
+      "version": "0.1.7",
+      "resolved": "https://registry.npmjs.org/coi-serviceworker/-/coi-serviceworker-0.1.7.tgz",
+      "integrity": "sha512-bjSUqEngCPOkErY2vbyWsaIGCNRODYzlNycaREVw5s12/C8SM+RnRUUeX6pZbTtov6C52ZLY/+tvHK+BDxuUuA=="
+    },
     "node_modules/color-convert": {
       "version": "1.9.3",
       "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-1.9.3.tgz",

package.json

@@ -21,6 +21,7 @@
     "@types/cytoscape": "^3.19.9",
     "@types/react-router-dom": "^5.3.3",
     "@vitejs/plugin-react-swc": "^3.4.0",
+    "coi-serviceworker": "^0.1.7",
     "cross-env": "^7.0.3",
     "cytoscape": "^3.23.0",
     "cytoscape-elk": "^2.1.0",

wasm.sh

@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cd server
+
+mkdir -p .lake/toolchains
+if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst  ]
+then
+    wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_wasm32.tar.zst
+    tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst -C .lake/toolchains
+fi
+if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst  ]
+then
+    wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_x86.tar.zst
+    tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst -C .lake/toolchains
+fi
+
+# Linking will fail, but that's ok. We only need the c files.
+.lake/toolchains/lean-4.3.0-rc2-linux_x86/bin/lake build -f=lakefile32.lean
+
+
+lake build
+
+
+OUT_DIR=../client/public
+LEAN_SYSROOT=.lake/toolchains/lean-4.3.0-rc2-linux_wasm32
+LEAN_LIBDIR=$LEAN_SYSROOT/lib/lean
+
+emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR .lake/build/ir/GameServer/*.c -lInit -lLean -lleancpp -lleanrt \
+  -sFORCE_FILESYSTEM -lnodefs.js -s EXIT_RUNTIME=0 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto \
+  -sPTHREAD_POOL_SIZE_STRICT=2 \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Init"@/lib/Init \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Init.olean"@/lib/Init.olean \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Init.ilean"@/lib/Init.ilean \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean"@/lib/Lean \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.olean"@/lib/Lean.olean \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.ilean"@/lib/Lean.ilean \
+  --preload-file "./.lake/build32/lib"@/gamelib