more

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)

client/src/app.tsx

@@ -13,6 +13,8 @@ import { useWindowDimensions } from './window_width';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
+new Worker("worker.js")
+
 function App() {
   const params = useParams()
   const gameId = "g/" + params.owner + "/" + params.repo

index.html

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

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",

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

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 ()

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());
 }

server/reverse-ffi/test.sh

@@ -2,4 +2,4 @@ set -ex
 
 ./clean.sh
 
-make run
+make

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: '.'
         }
       ]
     })