From afae75e41ffc0dc06fe50e112cfce67d779da573 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 1 Feb 2024 21:52:36 +0100 Subject: [PATCH] some stuff --- client/public/worker.js | 93 +++++++++++ client/src/wasm.ts | 339 ++++++++++++++++++++++++++++++++++++++++ index.html | 1 + package-lock.json | 6 + package.json | 1 + wasm.sh | 37 +++++ 6 files changed, 477 insertions(+) create mode 100644 client/public/worker.js create mode 100644 client/src/wasm.ts create mode 100755 wasm.sh diff --git a/client/public/worker.js b/client/public/worker.js new file mode 100644 index 0000000..d238568 --- /dev/null +++ b/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) diff --git a/client/src/wasm.ts b/client/src/wasm.ts new file mode 100644 index 0000000..db665e9 --- /dev/null +++ b/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 { + 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 { + 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'; + } +} diff --git a/index.html b/index.html index 7da8849..c02845f 100644 --- a/index.html +++ b/index.html @@ -33,6 +33,7 @@

+ diff --git a/package-lock.json b/package-lock.json index 7f459aa..3523f6f 100644 --- a/package-lock.json +++ b/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", diff --git a/package.json b/package.json index 8ac56a5..98d4843 100644 --- a/package.json +++ b/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", diff --git a/wasm.sh b/wasm.sh new file mode 100755 index 0000000..927b15d --- /dev/null +++ b/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