diff --git a/client/public/index.html b/client/public/index.html
index 1ed3a7d5..526b3190 100644
--- a/client/public/index.html
+++ b/client/public/index.html
@@ -24,6 +24,102 @@
       </a>
     </p>
   </noscript>
+  <script>
+
+    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);
+    }};
+    </script>
+    <script src="bin/lean.js"></script>
   <script src="bundle.js"></script>
 </body>
 
diff --git a/client/src/editor/leanclient.ts b/client/src/editor/leanclient.ts
index cddd5dfa..9ef612e7 100644
--- a/client/src/editor/leanclient.ts
+++ b/client/src/editor/leanclient.ts
@@ -20,7 +20,7 @@ import {
   State
 } from 'monaco-languageclient'
 import * as ls from 'vscode-languageserver-protocol'
-import { toSocket, WebSocketMessageReader, WebSocketMessageWriter } from 'vscode-ws-jsonrpc'
+import { toSocket } from 'vscode-ws-jsonrpc'
 
 import {
   // toolchainPath, lakePath, addServerEnvPaths, serverArgs, serverLoggingEnabled, serverLoggingPath, shouldAutofocusOutput,
@@ -39,6 +39,7 @@ import { join } from 'path'
 import { SemVer } from 'semver'
 // import { fileExists, isFileInFolder } from './utils/fsHelper'
 import { c2pConverter, p2cConverter, patchConverters } from './utils/converters'
+import { WasmReader, WasmWriter, WebSocketMessageWriter, WebSocketMessageReader } from '../wasm'
 
 const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&')
 
@@ -104,7 +105,7 @@ export class LeanClient implements Disposable {
   constructor (private readonly socketUrl: string, workspaceFolder: WorkspaceFolder | undefined, folderUri: Uri,
     public readonly showRestartMessage: () => void) {
     // this.storageManager = storageManager
-    // this.outputChannel = outputChannel
+    // this.outputChannel WebSocketMessageWriter= outputChannel
     this.workspaceFolder = workspaceFolder // can be null when opening adhoc files.
     this.folderUri = folderUri
     // this.elanDefaultToolchain = elanDefaultToolchain
@@ -323,8 +324,8 @@ export class LeanClient implements Disposable {
               })
               websocket.addEventListener('open', () => {
                 const socket = toSocket(websocket)
-                const reader = new WebSocketMessageReader(socket)
-                const writer = new WebSocketMessageWriter(socket)
+                const reader = new WasmReader()
+                const writer = new WasmWriter()
                 resolve({
                   reader,
                   writer
diff --git a/client/src/index.tsx b/client/src/index.tsx
index f28e07c3..a0fc92ee 100644
--- a/client/src/index.tsx
+++ b/client/src/index.tsx
@@ -5,4 +5,4 @@ import App from './App';
 
 const container = document.getElementById('root');
 const root = createRoot(container!);
-root.render(<React.StrictMode><App /></React.StrictMode>);
+root.render(<App />);
diff --git a/client/src/wasm.ts b/client/src/wasm.ts
new file mode 100644
index 00000000..ddaac4eb
--- /dev/null
+++ b/client/src/wasm.ts
@@ -0,0 +1,341 @@
+
+
+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() {
+    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);
+          IO.putLine(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() {
+    IO.listenPutStr(message => {
+      this.readMessage(message)
+    })
+      // 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';
+    }
+}
diff --git a/package.json b/package.json
index 85f121e4..624c1c25 100644
--- a/package.json
+++ b/package.json
@@ -60,7 +60,7 @@
   },
   "scripts": {
     "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
-    "start_server": "cd server && NODE_ENV=development nodemon ./index.js",
+    "start_server": "cd server && NODE_ENV=development node ./index.js",
     "start_client": "NODE_ENV=development webpack-dev-server --hot",
     "build": "npm run build_server && npm run build_client",
     "build_server": "server/build.sh",
diff --git a/server/LeanProject/lake-manifest.json b/server/LeanProject/lake-manifest.json
index 68b90c72..88a15753 100644
--- a/server/LeanProject/lake-manifest.json
+++ b/server/LeanProject/lake-manifest.json
@@ -4,19 +4,11 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "943f6a16d27a44766b2f93ca241caa09fa35467f",
+    "rev": "b0b0f7c0c82098a6c0e7cc658c99aebd5f5ac5de",
     "opts": {},
     "name": "mathlib",
     "inputRev?": "master",
     "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
@@ -48,5 +40,13 @@
     "opts": {},
     "name": "proofwidgets",
     "inputRev?": "v0.0.18",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "a093d7a6ac721071d8ba3774b0318063928cd3e2",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
     "inherited": true}}],
  "name": "leanProject"}
diff --git a/server/WebsocketServer.js b/server/WebsocketServer.js
index 92b52e4f..013451c0 100644
--- a/server/WebsocketServer.js
+++ b/server/WebsocketServer.js
@@ -87,6 +87,7 @@ class ClientConnection {
 
   send (data) {
     const str = JSON.stringify(data) + '\r\n'
+    console.log(JSON.stringify(data))
     const byteLength = Buffer.byteLength(str, 'utf-8')
     if (this.lean === null || this.lean.stdin === null) { throw Error('Lean not running yet.') }
     this.lean.stdin.cork()
diff --git a/server/index.js b/server/index.js
index 23950fee..453212b2 100644
--- a/server/index.js
+++ b/server/index.js
@@ -13,7 +13,18 @@ const crtFile = process.env.SSL_CRT_FILE
 const keyFile = process.env.SSL_KEY_FILE
 
 const app = express()
-app.use(express.static(path.join(__dirname, '../client/dist/')))
+app.use(express.static(path.join(__dirname, '../client/dist/'), {
+  setHeaders: function(res, path) {
+
+    res.set("Cross-Origin-Opener-Policy", "same-origin");
+    res.set("Cross-Origin-Embedder-Policy", "require-corp");
+    // res.set("Access-Control-Allow-Origin", "*");
+    // res.set("Access-Control-Allow-Headers", "Content-Type,X-Requested-With");
+    // res.set("Access-Control-Allow-Methods","PUT,POST,GET,DELETE,OPTIONS");
+    // res.set("X-Powered-By",' 3.2.1')
+    // res.type("application/json");
+    // res.type("jpg");
+  }}))
 app.use(nocache())
 
 let server;
diff --git a/webpack.config.js b/webpack.config.js
index 3c6ec5fb..1509f944 100644
--- a/webpack.config.js
+++ b/webpack.config.js
@@ -64,6 +64,10 @@ module.exports = env => {
       filename: "bundle.js",
     },
     devServer: {
+      headers: {
+        'Cross-Origin-Opener-Policy': 'same-origin',
+        'Cross-Origin-Embedder-Policy': 'require-corp'
+      },
       proxy: {
         '/websocket': {
            target: 'ws://localhost:8080',