From c6277dea3191a4f3048d8d50fa337b8c8abb059b Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 19 Oct 2023 21:35:43 +0200 Subject: [PATCH] editor works basically --- client/public/index.html | 96 ++++++++ client/src/editor/leanclient.ts | 9 +- client/src/index.tsx | 2 +- client/src/wasm.ts | 341 ++++++++++++++++++++++++++ package.json | 2 +- server/LeanProject/lake-manifest.json | 18 +- server/WebsocketServer.js | 1 + server/index.js | 13 +- webpack.config.js | 4 + 9 files changed, 470 insertions(+), 16 deletions(-) create mode 100644 client/src/wasm.ts 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 @@

+ + 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(); +root.render(); 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 { + 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 { + 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',