From 3d79c4ea60e85b8c48807bb9a751db0d7a4eb616 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Fri, 10 Nov 2023 20:25:25 +0100 Subject: [PATCH] connect wasm to monaco --- client/public/worker.js | 29 +- client/src/app.tsx | 2 - client/src/connection.ts | 2 +- client/src/leanclient.ts | 612 +++++++++++++++++++++++++++++++ client/src/wasm.ts | 341 +++++++++++++++++ server/reverse-ffi/lib/RFFI.lean | 34 +- server/reverse-ffi/main.c | 4 +- 7 files changed, 1006 insertions(+), 18 deletions(-) create mode 100644 client/src/leanclient.ts create mode 100644 client/src/wasm.ts diff --git a/client/public/worker.js b/client/public/worker.js index 8981378..60f0e99 100644 --- a/client/public/worker.js +++ b/client/public/worker.js @@ -67,7 +67,17 @@ return false; var stdoutBuffer = "" var stderrBuffer = "" - +var messageBuffer = [] +var initialized = false; + +function flushMessageBuffer(){ + if (initialized) { + while(messageBuffer.length > 0) { + var msg = messageBuffer.shift(); + Module.ccall('send_message', 'void', ['string'], [msg]); + } + } +} var Module = { "arguments": ["--worker"], @@ -90,14 +100,22 @@ var Module = { } FS.init(stdin, stdout, stderr); - }] + }], + "noInitialRun": true, + "onRuntimeInitialized": () => { + Module.ccall('main', 'number', [], []); + initialized = true; + flushMessageBuffer(); + } }; importScripts("server.js") + onmessage = (ev) => { - IO.putLine(ev.data) + messageBuffer.push(ev.data); + flushMessageBuffer(); } IO.listenPutStr(message => { @@ -116,8 +134,5 @@ setInterval(() => { }, 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 51e42ac..c45f6d0 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -13,8 +13,6 @@ 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/client/src/connection.ts b/client/src/connection.ts index 3a132a8..1dae0c1 100644 --- a/client/src/connection.ts +++ b/client/src/connection.ts @@ -4,7 +4,7 @@ import * as React from 'react'; import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import { LeanClient } from 'lean4web/client/src/editor/leanclient'; +import { LeanClient } from './leanclient'; export class Connection { private game: string = undefined // We only keep a connection to a single game at a time diff --git a/client/src/leanclient.ts b/client/src/leanclient.ts new file mode 100644 index 0000000..11dca5e --- /dev/null +++ b/client/src/leanclient.ts @@ -0,0 +1,612 @@ +/* This file is based on `vscode-lean4/src/leanclient.ts` */ + +import { + TextDocument, EventEmitter, Diagnostic, + DocumentHighlight, Range, DocumentHighlightKind, workspace, + Disposable, Uri, ConfigurationChangeEvent, OutputChannel, DiagnosticCollection, + WorkspaceFolder, window +} from 'vscode' +import { + DidChangeTextDocumentParams, + DidCloseTextDocumentParams, + DidOpenTextDocumentNotification, + DocumentFilter, + InitializeResult, + MonacoLanguageClient as LanguageClient, + LanguageClientOptions, + PublishDiagnosticsParams, + CloseAction, ErrorAction, + RevealOutputChannelOn, +} from 'monaco-languageclient' +import { State } from 'vscode-languageclient' +import * as ls from 'vscode-languageserver-protocol' +import { toSocket } from 'vscode-ws-jsonrpc' + +import { + // toolchainPath, lakePath, addServerEnvPaths, serverArgs, serverLoggingEnabled, serverLoggingPath, shouldAutofocusOutput, + getElaborationDelay + // lakeEnabled +} from 'lean4web/client/src/editor/config' +// import { assert } from './utils/assert' +import { LeanFileProgressParams, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api' +// import { LocalStorageService } from './utils/localStorage' +// import { batchExecute } from './utils/batch' +// import { readLeanVersion } from './utils/projectInfo' +import * as fs from 'fs' +import { URL } from 'url' +import { join } from 'path' +// import { logger } from './utils/logger' +import { SemVer } from 'semver' +// import { fileExists, isFileInFolder } from './utils/fsHelper' +import { c2pConverter, p2cConverter, patchConverters } from 'lean4web/client/src/editor/utils/converters' +import { WasmReader, WasmWriter, WebSocketMessageWriter, WebSocketMessageReader } from './wasm' + +const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&') + +export type ServerProgress = Map + +export function getFullRange (diag: Diagnostic): Range { + return (diag as any)?.fullRange || diag.range +} + +export class LeanClient implements Disposable { + running: boolean = false + private client: LanguageClient | undefined + // private toolchainPath: string + // private readonly outputChannel: OutputChannel + // private readonly storageManager: LocalStorageService + private readonly workspaceFolder: WorkspaceFolder | undefined + private readonly folderUri: Uri + private readonly subscriptions: Disposable[] = [] + private noPrompt: boolean = false + private showingRestartMessage: boolean = false + // private readonly elanDefaultToolchain: string + + private readonly didChangeEmitter = new EventEmitter() + didChange = this.didChangeEmitter.event + + private readonly diagnosticsEmitter = new EventEmitter() + diagnostics = this.diagnosticsEmitter.event + + private readonly didSetLanguageEmitter = new EventEmitter() + didSetLanguage = this.didSetLanguageEmitter.event + + private readonly didCloseEmitter = new EventEmitter() + didClose = this.didCloseEmitter.event + + private readonly customNotificationEmitter = new EventEmitter<{ method: string, params: any }>() + /** Fires whenever a custom notification (i.e. one not defined in LSP) is received. */ + customNotification = this.customNotificationEmitter.event + + /** saved progress info in case infoview is opened, it needs to get all of it. */ + progress: ServerProgress = new Map() + + private readonly progressChangedEmitter = new EventEmitter<[string, LeanFileProgressProcessingInfo[]]>() + progressChanged = this.progressChangedEmitter.event + + private readonly stoppedEmitter = new EventEmitter() + stopped = this.stoppedEmitter.event + + private readonly restartedEmitter = new EventEmitter() + restarted = this.restartedEmitter.event + + private readonly restartingEmitter = new EventEmitter() + restarting = this.restartingEmitter.event + + private readonly restartedWorkerEmitter = new EventEmitter() + restartedWorker = this.restartedWorkerEmitter.event + + private readonly serverFailedEmitter = new EventEmitter() + serverFailed = this.serverFailedEmitter.event + + /** Files which are open. */ + private readonly isOpen: Map = new Map() + + constructor (private readonly socketUrl: string, workspaceFolder: WorkspaceFolder | undefined, folderUri: Uri, + public readonly showRestartMessage: () => void) { + // this.storageManager = storageManager + // this.outputChannel WebSocketMessageWriter= outputChannel + this.workspaceFolder = workspaceFolder // can be null when opening adhoc files. + this.folderUri = folderUri + // this.elanDefaultToolchain = elanDefaultToolchain + // this.subscriptions.push(workspace.onDidChangeConfiguration((e) => this.configChanged(e))) + } + + dispose (): void { + this.subscriptions.forEach((s) => s.dispose()) + if (this.isStarted()) void this.stop() + } + + // async showRestartMessage (restartFile: boolean = false): Promise { + // // if (!this.showingRestartMessage) { + // // this.showingRestartMessage = true + // // let restartItem: string + // // let messageTitle: string + // // if (!restartFile) { + // // restartItem = 'Restart Lean Server' + // // messageTitle = 'Lean Server has stopped unexpectedly.' + // // } else { + // // restartItem = 'Restart Lean Server on this file' + // // messageTitle = 'The Lean Server has stopped processing this file.' + // // } + // // const item = await this.showErrorMessage(messageTitle, restartItem) + // // this.showingRestartMessage = false + // // if (item === restartItem) { + // // void this.start() + // // // if (restartFile && (window.activeTextEditor != null)) { + // // // await this.restartFile(window.activeTextEditor.document) + // // // } else { + // // // void this.start() + // // // } + // // } + // // } + // } + + async restart (): Promise { + const startTime = Date.now() + + console.log('[LeanClient] Restarting Lean Server') + if (this.isStarted()) { + await this.stop() + } + + this.restartingEmitter.fire(undefined) + // this.toolchainPath = this.storageManager.getLeanPath() + // if (!this.toolchainPath) this.toolchainPath = toolchainPath() + // let version = this.storageManager.getLeanVersion() + // const env = addServerEnvPaths(process.env) + // if (serverLoggingEnabled()) { + // env.LEAN_SERVER_LOG_DIR = serverLoggingPath() + // } + + // let executable = lakePath() || + // (this.toolchainPath ? join(this.toolchainPath, 'bin', 'lake') : 'lake') + + // check if the lake process will start (skip it on scheme: 'untitled' files) + // let useLake = lakeEnabled() && this.folderUri && this.folderUri.scheme === 'file' + // if (useLake) { + // let knownDate = false + // const lakefile = Uri.joinPath(this.folderUri, 'lakefile.lean') + // if (!await fileExists(new URL(lakefile.toString()))) { + // useLake = false + // } else { + // // see if we can avoid the more expensive checkLakeVersion call. + // const date = await this.checkToolchainVersion(this.folderUri) + // if (date != null) { + // // Feb 16 2022 is when the 3.1.0.pre was released. + // useLake = date >= new Date(2022, 1, 16) + // knownDate = true + // } + // if (useLake && !knownDate) { + // useLake = await this.checkLakeVersion(executable, version) + // } + // } + // } + + // if (!useLake) { + // executable = (this.toolchainPath) ? join(this.toolchainPath, 'bin', 'lean') : 'lean' + // } + + // const cwd = this.folderUri?.fsPath + // if (!cwd && !version) { + // // Fixes issue #227, for adhoc files it would pick up the cwd from the open folder + // // which is not what we want. For adhoc files we want the (default) toolchain instead. + // version = this.elanDefaultToolchain + // } + + // let options = version ? ['+' + version] : [] + // if (useLake) { + // options = options.concat(['serve', '--']) + // } else { + // options = options.concat(['--server']) + // } + + // Add folder name to command-line so that it shows up in `ps aux`. + // if (cwd) { + // options.push('' + cwd) + // } else { + // options.push('untitled') + // } + + // const serverOptions: ServerOptions = { + // command: executable, + // args: options.concat(serverArgs()), + // options: { + // cwd, + // env + // } + // } + + const clientOptions: LanguageClientOptions = { + // use a language id as a document selector + documentSelector: ['lean4'], + initializationOptions: { + editDelay: getElaborationDelay(), hasWidgets: true + }, + connectionOptions: { + maxRestartCount: 0, + cancellationStrategy: undefined as any + }, + // disable the default error handler + errorHandler: { + error: () => ({ action: ErrorAction.Continue }), + closed: () => ({ action: CloseAction.DoNotRestart }) + }, + middleware: { + handleDiagnostics: (uri, diagnostics, next) => { + next(uri, diagnostics) + if (this.client == null) return + const uri_ = c2pConverter.asUri(uri) + const diagnostics_ = [] + for (const d of diagnostics) { + const d_: ls.Diagnostic = { + ...c2pConverter.asDiagnostic(d) + } + diagnostics_.push(d_) + } + this.diagnosticsEmitter.fire({ uri: uri_, diagnostics: diagnostics_ }) + }, + + // didOpen: async () => { + // // Note: as per the LSP spec: An open notification must not be sent more than once + // // without a corresponding close notification send before. This means open and close + // // notification must be balanced and the max open count for a particular textDocument + // // is one. So this even does nothing the notification is handled by the + // // openLean4Document method below after the 'lean4' languageId is established and + // // it has weeded out documents opened to invisible editors (like 'git:' schemes and + // // invisible editors created for Ctrl+Hover events. A side effect of unbalanced + // // open/close notification is leaking 'lean --worker' processes. + // // See https://github.com/microsoft/vscode/issues/78453). + + // }, + + didChange: async (data, next) => { + await next(data) + if (!this.running || (this.client == null)) return // there was a problem starting lean server. + const params = c2pConverter.asChangeTextDocumentParams(data) + this.didChangeEmitter.fire(params) + }, + + didClose: async (doc, next) => { + if (!this.isOpen.delete(doc.uri.toString())) { + return + } + await next(doc) + if (!this.running || (this.client == null)) return // there was a problem starting lean server. + const params = c2pConverter.asCloseTextDocumentParams(doc) + this.didCloseEmitter.fire(params) + }, + + provideDocumentHighlights: async (doc, pos, ctok, next) => { + const leanHighlights = await next(doc, pos, ctok) + if (leanHighlights?.length) return leanHighlights + + // vscode doesn't fall back to textual highlights, + // so we need to do that manually + await new Promise((res) => setTimeout(res, 250)) + if (ctok.isCancellationRequested) return + + const wordRange = doc.getWordRangeAtPosition(pos) + if (wordRange == null) return + const word = doc.getText(wordRange) + + const highlights: DocumentHighlight[] = [] + const text = doc.getText() + const nonWordPattern = '[`~@$%^&*()-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\\\|;:\",./\\s]|^|$' + const regexp = new RegExp(`(?<=${nonWordPattern})${escapeRegExp(word)}(?=${nonWordPattern})`, 'g') + for (const match of text.matchAll(regexp)) { + const start = doc.positionAt(match.index ?? 0) + highlights.push({ + range: new Range(start, start.translate(0, match[0].length)), + kind: DocumentHighlightKind.Text + }) + } + + return highlights + } + } + } + if (!this.client) { + this.client = new LanguageClient({ + id: 'lean4', + name: 'Lean 4', + clientOptions, + connectionProvider: { + get: async () => { + return await new Promise((resolve, reject) => { + const worker = new Worker("worker.js") + const reader = new WasmReader(worker) + const writer = new WasmWriter(worker) + resolve({ + reader, + writer + }) + }) + } + } + }) + } else { + await this.client.start() + } + + + // HACK: Prevent monaco from panicking when the Lean server crashes + this.client.handleFailedRequest = (type, token: any, error: any, defaultValue, showNotification?: boolean) => { + return defaultValue + } + + let insideRestart = true + patchConverters(this.client.protocol2CodeConverter, this.client.code2ProtocolConverter) + try { + this.client.onDidChangeState(async (s) => { + // see https://github.com/microsoft/vscode-languageserver-node/issues/825 + if (s.newState === State.Starting) { + console.log('[LeanClient] starting') + } else if (s.newState === State.Running) { + const end = Date.now() + console.log(`[LeanClient] running, started in ${end - startTime} ms`) + this.running = true // may have been auto restarted after it failed. + if (!insideRestart) { + this.restartedEmitter.fire(undefined) + } + } else if (s.newState === State.Stopped) { + this.running = false + console.log('[LeanClient] has stopped or it failed to start') + if (!this.noPrompt) { + // only raise this event and show the message if we are not the ones + // who called the stop() method. + this.stoppedEmitter.fire({ message: 'Lean server has stopped.', reason: '' }) + await this.showRestartMessage() + } + } + }) + await this.client.start() + // tell the new client about the documents that are already open! + // for (const key of this.isOpen.keys()) { + // const doc = this.isOpen.get(key) + // if (doc != null) this.notifyDidOpen(doc) + // } + // if we got this far then the client is happy so we are running! + this.running = true + } catch (error) { + console.log(error) + this.serverFailedEmitter.fire('' + error) + insideRestart = false + return + } + + // HACK(WN): Register a default notification handler to fire on custom notifications. + // A mechanism to do this is provided in vscode-jsonrpc. One can register a `StarNotificationHandler` + // here: https://github.com/microsoft/vscode-languageserver-node/blob/b2fc85d28a1a44c22896559ee5f4d3ba37a02ef5/jsonrpc/src/common/connection.ts#L497 + // which fires on any LSP notifications not in the standard, for example the `$/lean/..` ones. + // However this mechanism is not exposed in vscode-languageclient, so we hack around its implementation. + const starHandler = (method: string, params_: any) => { + if (method === '$/lean/fileProgress' && (this.client != null)) { + const params = params_ as LeanFileProgressParams + const uri = p2cConverter.asUri(params.textDocument.uri) + this.progressChangedEmitter.fire([uri.toString(), params.processing]) + // save the latest progress on this Uri in case infoview needs it later. + this.progress.set(uri, params.processing) + } + + this.customNotificationEmitter.fire({ method, params: params_ }) + } + // eslint-disable-next-line @typescript-eslint/no-unsafe-argument + this.client.onNotification(starHandler as any, () => {}) + + // Reveal the standard error output channel when the server prints something to stderr. + // The vscode-languageclient library already takes care of writing it to the output channel. + // let stderrMsgBoxVisible = false; + // (this.client)._serverProcess.stderr.on('data', async (chunk: Buffer) => { + // if (shouldAutofocusOutput()) { + // this.client?.outputChannel.show(true) + // } else if (!stderrMsgBoxVisible) { + // stderrMsgBoxVisible = true + // const outputItem = 'Show stderr output' + // const outPrompt = `Lean server printed an error:\n${chunk.toString()}` + // if (await window.showErrorMessage(outPrompt, outputItem) === outputItem) { + // this.outputChannel.show(false) + // } + // stderrMsgBoxVisible = false + // } + // }) + + this.restartedEmitter.fire(undefined) + insideRestart = false + } + + async openLean4Document (doc: TextDocument) { + if (this.isOpen.has(doc.uri.toString())) return + if (!await this.isSameWorkspace(doc.uri)) { + // skip it, this file belongs to a different workspace... + return + } + + this.isOpen.set(doc.uri.toString(), doc) + + if (!this.running) return // there was a problem starting lean server. + + // didOpenEditor may have also changed the language, so we fire the + // event here because the InfoView should be wired up to receive it now. + this.didSetLanguageEmitter.fire(doc.languageId) + + this.notifyDidOpen(doc) + } + + notifyDidOpen (doc: TextDocument) { + // BUG: was `DidOpenTextDocumentNotification.type` instead of the string, but that failed + void this.client?.sendNotification('textDocument/didOpen', { + textDocument: { + uri: doc.uri.toString(), + languageId: doc.languageId, + version: 1, + text: doc.getText() + } + }) + } + + async isSameWorkspace (uri: Uri): Promise { + // if (this.folderUri) { + // if (this.folderUri.scheme !== uri.scheme) return false + // if (this.folderUri.scheme === 'file') { + // const realPath1 = await fs.promises.realpath(this.folderUri.fsPath) + // const realPath2 = await fs.promises.realpath(uri.fsPath) + // return isFileInFolder(realPath2, realPath1) + // } else { + // return uri.toString().startsWith(this.folderUri.toString()) + // } + // } else { + // return uri.scheme === 'untitled' + // } + return false + } + + getWorkspaceFolder (): string { + return this.folderUri?.toString() + } + + async start (): Promise { + return await this.restart() + } + + isStarted (): boolean { + return this.client !== undefined + } + + isRunning (): boolean { + if (this.client != null) { + return this.running + } + return false + } + + async stop (): Promise { + // assert(() => this.isStarted()) + if ((this.client != null) && this.running) { + this.noPrompt = true + try { + // some timing conditions can happen while running unit tests that cause + // this to throw an exception which then causes those tests to fail. + await this.client.stop() + } catch (e) { + console.log(`[LeanClient] Error stopping language client: ${e}`) + } + } + + this.noPrompt = false + this.progress = new Map() + this.client = undefined + this.running = false + } + + configChanged (e: ConfigurationChangeEvent): void { + // let newToolchainPath = this.storageManager.getLeanPath() + // if (!newToolchainPath) newToolchainPath = toolchainPath() + // if (this.toolchainPath !== newToolchainPath) { + // void this.restart() + // } + } + + async restartFile (doc: TextDocument): Promise { + if (!this.running) return // there was a problem starting lean server. + + // assert(() => this.isStarted()) + + if (!await this.isSameWorkspace(doc.uri)) { + // skip it, this file belongs to a different workspace... + return + } + const uri = doc.uri.toString() + console.log(`[LeanClient] Restarting File: ${uri}`) + // This causes a text document version number discontinuity. In + // (didChange (oldVersion) => restartFile => didChange (newVersion)) + // the client emits newVersion = oldVersion + 1, despite the fact that the + // didOpen packet emitted below initializes the version number to be 1. + // This is not a problem though, since both client and server are fine + // as long as the version numbers are monotonous. + void this.client?.sendNotification('textDocument/didClose', { + textDocument: { + uri + } + }) + void this.client?.sendNotification('textDocument/didOpen', { + textDocument: { + uri, + languageId: 'lean4', + version: 1, + text: doc.getText() + } + }) + this.restartedWorkerEmitter.fire(uri) + } + + // eslint-disable-next-line @typescript-eslint/explicit-module-boundary-types + async sendRequest (method: string, params: any): Promise { + return this.running && (this.client != null) + ? await this.client.sendRequest(method, params) + : await new Promise((_, reject) => { reject('Client is not running') }) + } + + // eslint-disable-next-line @typescript-eslint/explicit-module-boundary-types + sendNotification (method: string, params: any): Promise | undefined { + return this.running && (this.client != null) ? this.client.sendNotification(method, params) : undefined + } + + async getDiagnosticParams (uri: Uri, diagnostics: readonly Diagnostic[]): Promise { + const params: PublishDiagnosticsParams = { + uri: c2pConverter.asUri(uri), + diagnostics: await c2pConverter.asDiagnostics(diagnostics as Diagnostic[]) + } + return params + } + + getDiagnostics (): DiagnosticCollection | undefined { + return this.running ? this.client?.diagnostics : undefined + } + + get initializeResult (): InitializeResult | undefined { + return this.running ? this.client?.initializeResult : undefined + } + + private async checkToolchainVersion (folderUri: Uri): Promise { + // see if we have a well known toolchain label that corresponds + // to a known date like 'leanprover/lean4:nightly-2022-02-01' + // const toolchainVersion = await readLeanVersion(folderUri) + // if (toolchainVersion) { + // const match = /^leanprover\/lean4:nightly-(\d+)-(\d+)-(\d+)$/.exec(toolchainVersion) + // if (match != null) { + // return new Date(parseInt(match[1]), parseInt(match[2]) - 1, parseInt(match[3])) + // } + // if (toolchainVersion === 'leanprover/lean4:stable') { + // return new Date(2022, 2, 1) + // } + // } + return undefined + } + + // async checkLakeVersion (executable: string, version: string): Promise { + // // Check that the Lake version is high enough to support "lake serve" option. + // const versionOptions = version ? ['+' + version, '--version'] : ['--version'] + // const start = Date.now() + // const lakeVersion = await batchExecute(executable, versionOptions, this.folderUri?.fsPath, undefined) + // logger.log(`[LeanClient] Ran '${executable} ${versionOptions.join(' ')}' in ${Date.now() - start} ms`) + // const actual = this.extractVersion(lakeVersion) + // if (actual.compare('3.0.0') > 0) { + // return true + // } + // return false + // } + + // private extractVersion (v: string | undefined): SemVer { + // if (!v) return new SemVer('0.0.0') + // const prefix = 'Lake version' + // if (v.startsWith(prefix)) v = v.slice(prefix.length).trim() + // const pos = v.indexOf('(') + // if (pos > 0) v = v.slice(0, pos).trim() + // try { + // return new SemVer(v) + // } catch { + // return new SemVer('0.0.0') + // } + // } +} diff --git a/client/src/wasm.ts b/client/src/wasm.ts new file mode 100644 index 0000000..0a35104 --- /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(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/server/reverse-ffi/lib/RFFI.lean b/server/reverse-ffi/lib/RFFI.lean index 3ecfa1d..eb5202d 100644 --- a/server/reverse-ffi/lib/RFFI.lean +++ b/server/reverse-ffi/lib/RFFI.lean @@ -1,8 +1,30 @@ -import Lean +import Lean.Server.Watchdog -@[export my_length] -def myLength (s : String) : IO Unit := do - IO.println "hello" - IO.println Lean.origin - IO.println s +open Lean +open Server +open Watchdog +open Lsp +open IO +open JsonRpc + +#check JsonRpc.Request + +@[export game_send_message] +def sendMessage (s : String) : IO Unit := do + let expectedMethod := "initialize" + let j ← ofExcept (Json.parse s) + let m ← match fromJson? j with + | Except.ok (m : JsonRpc.Message) => pure m + | Except.error inner => throw $ userError s!"JSON '{j.compress}' did not have the format of a JSON-RPC message.\n{inner}" + let initRequest ← match m with + | Message.request id method params? => + if method = expectedMethod then + let j := toJson params? + match fromJson? j with + | Except.ok v => pure $ JsonRpc.Request.mk id expectedMethod (v : InitializeParams) + | Except.error inner => throw $ userError s!"Unexpected param '{j.compress}' for method '{expectedMethod}'\n{inner}" + else + throw $ userError s!"Expected method '{expectedMethod}', got method '{method}'" + | _ => throw $ userError s!"Expected JSON-RPC request, got: '{(toJson m).compress}'" + IO.println s!"{initRequest.param.editDelay}" return () diff --git a/server/reverse-ffi/main.c b/server/reverse-ffi/main.c index 6b6985f..6882e9a 100644 --- a/server/reverse-ffi/main.c +++ b/server/reverse-ffi/main.c @@ -1,7 +1,7 @@ #include #include -extern lean_object* my_length(lean_object*, lean_object*); +extern lean_object* game_send_message(lean_object*, lean_object*); // see https://leanprover.github.io/lean4/doc/dev/ffi.html#initialization extern void lean_initialize_runtime_module(); @@ -29,5 +29,5 @@ int main() { void send_message(char* msg){ lean_object * s = lean_mk_string(msg); - my_length(s, lean_io_mk_world()); + game_send_message(s, lean_io_mk_world()); }