diff --git a/client/public/worker.js b/client/public/worker.js new file mode 100644 index 0000000..8981378 --- /dev/null +++ b/client/public/worker.js @@ -0,0 +1,123 @@ + +const IO = { + _resolveGetLine: null, + _resolveRead: null, + _readPointer: null, + _nbytes: 0, + bufferStdIn : "", + putStrListeners: [], + listenPutStr(callback) { + this.putStrListeners.push(callback) + }, + putStr(str) { + console.log('PUTSTR' + str) + str = str.split('\n')[2] + this.putStrListeners.forEach((listener) => { + listener(str) + }) + }, + async getLine() { + return new Promise((resolve, reject) => { + this._resolveGetLine = resolve + this.flushStdIn(); + }); + }, + async read(ptr, nbytes) { + this._nbytes = nbytes + this._readPointer = ptr + return new Promise((resolve, reject) => { + this._resolveRead = resolve + this.flushStdIn(); + }); + }, + flushStdIn() { + if(this._resolveGetLine) { + var lineBreak = this.bufferStdIn.indexOf("\n") + if (lineBreak != -1) { + this._resolveGetLine(stringToNewUTF8(this.bufferStdIn.substring(0,lineBreak+1))) + this.bufferStdIn = this.bufferStdIn.substring(lineBreak+1) + this._resolveGetLine = null + } + } + if(this._resolveRead) { + // console.log(`read: ${this.bufferStdIn}`) + stringToUTF8(this.bufferStdIn, this._readPointer, this._nbytes); + this._resolveRead() + this.bufferStdIn = "" + this._resolveRead = null + } + }, + putLine(data) { + console.log("Client: ",data) + const str = data + '\r\n' + const byteLength = lengthBytesUTF8(str) + this.bufferStdIn += `Content-Length: ${byteLength}\r\n\r\n` + str + this.flushStdIn(); + } +} + + +var input = "" +var i = 0; + +function submit (ev) { +ev.preventDefault() +return false; +} + +var stdoutBuffer = "" +var stderrBuffer = "" + + +var Module = { + "arguments": ["--worker"], + "preRun": [function() { + function stdin() { + if (i < input.length) { + i++; + return input.charCodeAt(i);// Return ASCII code of character, or null if no input + } else { + return null + } + } + + function stdout(asciiCode) { + stdoutBuffer += String.fromCharCode(asciiCode) + } + + function stderr(asciiCode) { + stderrBuffer += String.fromCharCode(asciiCode) + } + + FS.init(stdin, stdout, stderr); + }] +}; + +importScripts("server.js") + + +onmessage = (ev) => { + IO.putLine(ev.data) +} + +IO.listenPutStr(message => { + postMessage(message) +}) + +setInterval(() => { + if (stdoutBuffer !== "") { + console.log(stdoutBuffer); + stdoutBuffer = "" + } + if (stderrBuffer !== "") { + console.error(stderrBuffer); + stderrBuffer = "" + } +}, 1000) + +setTimeout(() =>{ + Module.ccall('send_message', // name of C function + 'void', // return type + ['string'], // argument types + ['Hi there!']); // arguments +},2000) diff --git a/client/src/app.tsx b/client/src/app.tsx index c45f6d0..51e42ac 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -13,6 +13,8 @@ import { useWindowDimensions } from './window_width'; export const GameIdContext = React.createContext(undefined); +new Worker("worker.js") + function App() { const params = useParams() const gameId = "g/" + params.owner + "/" + params.repo 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 760e0f2..11a9aae 100644 --- a/package-lock.json +++ b/package-lock.json @@ -20,6 +20,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", @@ -6890,6 +6891,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 2042253..14d7134 100644 --- a/package.json +++ b/package.json @@ -16,6 +16,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/server/reverse-ffi/Makefile b/server/reverse-ffi/Makefile index 4ed645e..efe3a5c 100644 --- a/server/reverse-ffi/Makefile +++ b/server/reverse-ffi/Makefile @@ -1,16 +1,17 @@ -.PHONY: all run run-local lake +.PHONY: all run lake -all: run run-local + +OUT_DIR = ../../client/public +LEAN_SYSROOT ?= /home/alex/Projects/lean4/build/release/stage1 +LEAN_LIBDIR := $(LEAN_SYSROOT)/lib/lean + +all: $(OUT_DIR)/server.js # Link C binary against Lake package dynamic library lake: lake --dir=lib build -OUT_DIR = out -LEAN_SYSROOT ?= /home/alex/Projects/lean4/build/release/stage1 -LEAN_LIBDIR := $(LEAN_SYSROOT)/lib/lean - $(OUT_DIR): mkdir -p $@ @@ -19,18 +20,12 @@ ifneq ($(OS),Windows_NT) LINK_FLAGS=-Wl,-rpath,$(LEAN_LIBDIR) -Wl,-rpath,$(PWD)/lib/build/lib endif -$(OUT_DIR)/main: main.c lake | $(OUT_DIR) +$(OUT_DIR)/server.js: main.c lake | $(OUT_DIR) # Add library paths for Lake package and for Lean itself emcc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) lib/build/ir/RFFI.c -lInit -lLean -lleancpp -lleanrt $(LINK_FLAGS) \ - -sFORCE_FILESYSTEM -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto - -run: $(OUT_DIR)/main -ifeq ($(OS),Windows_NT) -# Add shared library paths to loader path dynamically - env PATH="lib/build/lib:$(shell cygpath $(LEAN_SYSROOT))/bin:$(PATH)" $(OUT_DIR)/main -else - $(OUT_DIR)/main -endif + -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 + + # Alternatively, we can copy all shared lib dependencies to the current directory # in order to avoid path set up and obtain a more portable executable diff --git a/server/reverse-ffi/lib/RFFI.lean b/server/reverse-ffi/lib/RFFI.lean index 9f91c2a..3ecfa1d 100644 --- a/server/reverse-ffi/lib/RFFI.lean +++ b/server/reverse-ffi/lib/RFFI.lean @@ -3,4 +3,6 @@ import Lean @[export my_length] def myLength (s : String) : IO Unit := do IO.println "hello" - return () -- IO.println Lean.origin + IO.println Lean.origin + IO.println s + return () diff --git a/server/reverse-ffi/main.c b/server/reverse-ffi/main.c index 5152424..6b6985f 100644 --- a/server/reverse-ffi/main.c +++ b/server/reverse-ffi/main.c @@ -25,9 +25,9 @@ int main() { return 1; // do not access Lean declarations if initialization failed } lean_io_mark_end_initialization(); +} - // actual program - - lean_object * s = lean_mk_string("hello!"); +void send_message(char* msg){ + lean_object * s = lean_mk_string(msg); my_length(s, lean_io_mk_world()); } diff --git a/server/reverse-ffi/test.sh b/server/reverse-ffi/test.sh index 7e3e645..0a6810f 100755 --- a/server/reverse-ffi/test.sh +++ b/server/reverse-ffi/test.sh @@ -2,4 +2,4 @@ set -ex ./clean.sh -make run +make diff --git a/vite.config.ts b/vite.config.ts index 59ade19..97921de 100644 --- a/vite.config.ts +++ b/vite.config.ts @@ -17,6 +17,10 @@ export default defineConfig({ { src: 'node_modules/@leanprover/infoview/dist/*.production.min.js', dest: '.' + }, + { + src: 'node_modules/coi-serviceworker/coi-serviceworker.js', + dest: '.' } ] })