error: Tried to spawn a new thread, but

.gitignore

@@ -2,5 +2,7 @@ node_modules
 client/dist
 server/build
 server/lakefile.olean
+server32bit
 **/lake-packages/
 **/.DS_Store
+client/public/server.*

client/public/worker.js

@@ -0,0 +1,94 @@
+
+var stderrBuffer = ""
+var messageBuffer = []
+var initialized = false;
+var flushing = false;
+
+var headerMode = true;
+var header="";
+var re = /Content-Length: (\d+)\r\n/i;
+var contentLength = 0;
+var content = []
+var utf8decoder = new TextDecoder();
+
+
+function flushMessageBuffer(){
+  if (initialized && !flushing) {
+    while(messageBuffer.length > 0) {
+      flushing = true;
+      var msg = messageBuffer.shift();
+      console.log(`Send message: ${msg}`);
+      Module.ccall('send_message', 'void', ['string'], [msg]);
+      console.log(`Message done: ${msg}`);
+    }
+    flushing = false;
+  }
+}
+
+var Module = {
+  "arguments": ["--worker"],
+  "preRun": [function() {
+    function stdin() {
+      return null;
+    }
+
+    function stdout(asciiCode) {
+      if (headerMode) {
+        header += String.fromCharCode(asciiCode)
+        if (header.endsWith('\r\n\r\n')) {
+          const found = header.match(re)
+          if (found == null) { console.error(`Invalid header: ${header}`) }
+          contentLength = parseInt(found[1])
+          content = []
+          headerMode = false
+        }
+      } else {
+        content.push(asciiCode)
+        if (content.length == contentLength) {
+          const message = utf8decoder.decode(new Uint8Array(content))
+          console.log(`Server: ${message}`)
+          postMessage(message);
+          headerMode = true
+          header = ''
+        }
+      }
+    }
+
+    function stderr(asciiCode) {
+      stderrBuffer += String.fromCharCode(asciiCode)
+    }
+
+    FS.init(stdin, stdout, stderr);
+  }],
+  "noInitialRun": true,
+  "onRuntimeInitialized": () => {
+    Module.ccall('main', 'void', [], []);
+    initialized = true;
+    if (stderrBuffer !== "") {
+      console.log(stderrBuffer);
+      stderrBuffer = ""
+    }
+    flushMessageBuffer();
+  }
+};
+
+importScripts("server.js")
+
+
+
+onmessage = (ev) => {
+  console.log(`Client: ${ev.data}`)
+  messageBuffer.push(ev.data);
+  flushMessageBuffer();
+}
+
+setInterval(() => {
+  if (stderrBuffer !== "") {
+    console.log(stderrBuffer);
+    stderrBuffer = ""
+  }
+}, 1000)
+
+setTimeout(() =>{
+
+},2000)

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

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<Uri, LeanFileProgressProcessingInfo[]>
+
+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<DidChangeTextDocumentParams>()
+  didChange = this.didChangeEmitter.event
+
+  private readonly diagnosticsEmitter = new EventEmitter<PublishDiagnosticsParams>()
+  diagnostics = this.diagnosticsEmitter.event
+
+  private readonly didSetLanguageEmitter = new EventEmitter<string>()
+  didSetLanguage = this.didSetLanguageEmitter.event
+
+  private readonly didCloseEmitter = new EventEmitter<DidCloseTextDocumentParams>()
+  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<string>()
+  restartedWorker = this.restartedWorkerEmitter.event
+
+  private readonly serverFailedEmitter = new EventEmitter<string>()
+  serverFailed = this.serverFailedEmitter.event
+
+  /** Files which are open. */
+  private readonly isOpen: Map<string, TextDocument> = 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<void> {
+  //   // 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<void> {
+    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<boolean> {
+    // 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<void> {
+    return await this.restart()
+  }
+
+  isStarted (): boolean {
+    return this.client !== undefined
+  }
+
+  isRunning (): boolean {
+    if (this.client != null) {
+      return this.running
+    }
+    return false
+  }
+
+  async stop (): Promise<void> {
+    // 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<void> {
+    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<any> {
+    return this.running && (this.client != null)
+      ? await this.client.sendRequest(method, params)
+      : await new Promise<any>((_, reject) => { reject('Client is not running') })
+  }
+
+  // eslint-disable-next-line @typescript-eslint/explicit-module-boundary-types
+  sendNotification (method: string, params: any): Promise<void> | undefined {
+    return this.running && (this.client != null) ? this.client.sendNotification(method, params) : undefined
+  }
+
+  async getDiagnosticParams (uri: Uri, diagnostics: readonly Diagnostic[]): Promise<PublishDiagnosticsParams> {
+    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<Date | undefined> {
+    // 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<boolean> {
+  //   // 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')
+  //   }
+  // }
+}

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<void> {
+      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<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';
+    }
+}

index.html

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

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

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/.gitignore

@@ -1,3 +1,3 @@
-build
+.lake
 adam
-nng
+lakefile32.olean

server/GameServer.lean

@@ -0,0 +1,13 @@
+import Lean.Server.Watchdog
+import GameServer.Commands
+import GameServer.Game
+
+Game "TestGame"
+Title "Hello Test"
+
+World "Test"
+Level 1
+
+Statement : 1 = 1 := sorry
+
+MakeGame

server/GameServer/FileWorker.lean

@@ -395,26 +395,9 @@ section Initialization
     fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
     fileMap  := default
 
-  def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
+  def mkHeaderTask (m : DocumentMeta) (hOut : FS.Stream) (paths : List System.FilePath)
-      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
+      (env : Environment) (opts : Options) (hasWidgets : Bool) :
       IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
-    -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
-    let out ← IO.Process.output
-      { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
-    if out.exitCode != 0 then
-      throwServerError s!"Error while running Lake: {out.stderr}"
-
-    -- Make the paths relative to the current directory
-    let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
-    let currentDir ← IO.currentDir
-    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p
-
-    -- Set the search path
-    Lean.searchPathRef.set paths
-
-    let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
-    -- return (env, paths)
-
     -- use empty header
     let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
       {m.mkInputContext with
@@ -456,11 +439,32 @@ section Initialization
       publishDiagnostics m headerSnap.diagnostics.toArray hOut
       return (headerSnap, srcSearchPath)
 
+  def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
+      (levelParams : Game.DidOpenLevelParams) :
+      IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
+    -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
+    let out ← IO.Process.output
+      { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+    if out.exitCode != 0 then
+      throwServerError s!"Error while running Lake: {out.stderr}"
+
+    -- Make the paths relative to the current directory
+    let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
+    let currentDir ← IO.currentDir
+    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p
+
+    -- Set the search path
+    Lean.searchPathRef.set paths
+
+    let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
+    -- return (env, paths)
+    mkHeaderTask m hOut paths env opts hasWidgets
+
   def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
        (levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
     let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      levelParams initParams
+      levelParams
     let cancelTk ← CancelToken.new
     let ctx :=
       { hIn  := i
@@ -515,10 +519,8 @@ section MessageHandling
 end MessageHandling
 
 section MainLoop
-  partial def mainLoop : GameWorkerM Unit := do
+  partial def mainLoop1 (msg : JsonRpc.Message): GameWorkerM Bool := do
-    let ctx ← read
     let mut st ← StateT.lift get
-    let msg ← ctx.hIn.readLspMessage
     let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
         : IO PendingRequestMap := do
       if (← hasFinished task) then
@@ -541,11 +543,11 @@ section MainLoop
     match msg with
     | Message.request id method (some params) =>
       handleRequest id method (toJson params)
-      mainLoop
+      return false
     | Message.notification "exit" none =>
       let doc := st.doc
       doc.cancelTk.set
-      return ()
+      return true
     | Message.notification "$/game/setInventory" params =>
       let p := (← parseParams Game.SetInventoryParams (toJson params))
       let s ← get
@@ -553,11 +555,19 @@ section MainLoop
       set {s with levelParams := {s.levelParams with
         inventory := p.inventory,
         difficulty := p.difficulty}}
-      mainLoop
+      return false
     | Message.notification method (some params) =>
       handleNotification method (toJson params)
-      mainLoop
+      return false
     | _ => throwServerError "Got invalid JSON-RPC message"
+
+
+partial def mainLoop : GameWorkerM Unit := do
+  let ctx ← read
+  let msg ← ctx.hIn.readLspMessage
+  if not (← mainLoop1 msg) then
+    mainLoop
+
 end MainLoop
 
 def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do

server/GameServer/WasmServer.lean

@@ -0,0 +1,257 @@
+import Lean.Server.Watchdog
+import GameServer.FileWorker
+import GameServer.EnvExtensions
+import GameServer.Game
+
+namespace WasmServer.Watchdog
+open Lean
+open Server
+open Watchdog
+open IO
+open Lsp
+open JsonRpc
+open System.Uri
+
+open MyServer.FileWorker
+
+structure WasmFileState :=
+  fileWorkerState : FileWorker.WorkerState
+  gameWorkerState : GameWorkerState
+  headerTask : Task (Except Error (Snapshots.Snapshot × SearchPath))
+
+structure WasmServerState :=
+  initParams? : Option InitializeParams
+  gameServerState : GameServerState
+  fileState : HashMap String WasmFileState := {}
+
+def wasmSearchPath : SearchPath  := ["/lib", "/gamelib"]
+
+@[export game_make_state]
+unsafe def makeState : IO WasmServerState := do
+  let e ← IO.getStderr
+  try
+    Lean.enableInitializersExecution
+    searchPathRef.set wasmSearchPath
+    let env ← importModules #[
+      { module := `GameServer : Import }
+    ] {} 0
+    let state : GameServerState := {
+      env,
+      game := `TestGame,
+      gameDir := "test",
+      inventory := #[]
+      difficulty := 0
+    }
+    return ⟨none, state, {}⟩
+  catch err =>
+    e.putStrLn s!"Import error: {err}"
+    throw err
+
+def readMessage (s : String) : IO JsonRpc.Message := do
+  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}"
+  return m
+
+def readLspRequestAs (s : String) (expectedMethod : String) (α : Type) [FromJson α] : IO (Request α) := do
+  let m ← readMessage s
+  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 : α)
+      | 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}'"
+
+def initializeServer (id : RequestID) : IO Unit := do
+  let o ← IO.getStdout
+  o.writeLspResponse {
+    id     := id
+    result := {
+      capabilities := mkLeanServerCapabilities
+      serverInfo?  := some {
+        name     := "Lean 4 Game Server"
+        version? := "0.1.1"
+      }
+      : InitializeResult
+    }
+  }
+  return ()
+
+def mkServerContext (state : WasmServerState) : IO ServerContext := do
+  let i ← IO.getStdin
+  let o ← IO.getStdout
+  let e ← IO.getStderr
+  let srcSearchPath ← searchPathRef.get
+  let references ← IO.mkRef (← loadReferences)
+  let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
+  let workerPath := "no-worker-path"
+  let some initParams := state.initParams?
+    | throwServerError "no yet initialized"
+  return {
+    hIn            := i
+    hOut           := o
+    hLog           := e
+    args           := []
+    fileWorkersRef := fileWorkersRef
+    initParams
+    workerPath
+    srcSearchPath
+    references
+  }
+
+def runGameServerM (state : WasmServerState) (x : GameServerM α) : IO (α × WasmServerState) := do
+  let (res, gameServerState) ← ReaderT.run
+      (StateT.run x state.gameServerState)
+      (← mkServerContext state)
+  return (res, {state with gameServerState})
+
+def mkWorkerContext (state : WasmServerState) (headerTask : Task (Except Error (Snapshots.Snapshot × SearchPath))) :
+    IO FileWorker.WorkerContext := do
+  let i ← IO.getStdin
+  let o ← IO.getStdout
+  let e ← IO.getStderr
+  let some initParams := state.initParams?
+    | throwServerError "no yet initialized"
+  let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
+  return {
+    hIn  := i
+    hOut := o
+    hLog := e
+    headerTask := headerTask
+    initParams := initParams
+    clientHasWidgets
+  }
+
+def runGameWorkerM (state : WasmServerState) (fileState : WasmFileState) (x : GameWorkerM α) :
+    IO (α × WasmFileState) := do
+  let s := fileState.fileWorkerState
+  let ctx ← mkWorkerContext state fileState.headerTask
+  let ((res, gameWorkerState), s) ← StateRefT'.run (s := s) <| ReaderT.run (r := ctx) <|
+      StateT.run (s := fileState.gameWorkerState) <| x
+  let fileState := {fileState with gameWorkerState := gameWorkerState, fileWorkerState := s}
+  return (res, fileState)
+
+def parseParams {paramType : Type} [FromJson paramType] (params : Json) : IO paramType :=
+  match fromJson? params with
+  | Except.ok parsed => pure parsed
+  | Except.error inner => throwServerError s!"Got param with wrong structure: {params.compress}\n{inner}"
+
+def requestWorkerUri (method : String) (params : Json) : IO (Option DocumentUri) := do
+  if method == "$/lean/rpc/connect" then
+    let ps : Lsp.RpcConnectParams ← parseParams params
+    pure <| fileSource ps
+  else match (← routeLspRequest method params) with
+    | Except.error e =>
+      throwServerError e.message
+    | Except.ok uri => pure uri
+
+open FileWorker in
+def handleDidOpen (params : DidOpenTextDocumentParams) (state : WasmServerState) : IO WasmServerState := do
+  let some initParams := state.initParams?
+    | throwServerError "no yet initialized"
+  let (_, state) ← runGameServerM state do
+    let some lvl ← GameServer.getLevelByFileName? initParams
+        ((System.Uri.fileUriToPath? params.textDocument.uri).getD params.textDocument.uri |>.toString)
+      | throwServerError s!"Level not found: {params.textDocument.uri} | {initParams.rootUri?}"
+
+    let env ← importModules #[
+      { module := lvl.module : Import }
+    ] {} 0
+
+    (← getStderr).putStr "Import for level completed"
+
+    let doc := params.textDocument
+    let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
+    let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
+
+    let (headerStx, headerTask) ← mkHeaderTask meta (← getStdout) wasmSearchPath env {} clientHasWidgets
+    let cancelTk ← CancelToken.new
+
+    let levelParams := {
+      uri := meta.uri
+      gameDir := state.gameServerState.gameDir
+      levelModule := lvl.module
+      tactics := lvl.tactics.tiles
+      lemmas := lvl.lemmas.tiles
+      definitions := lvl.definitions.tiles
+      inventory := state.gameServerState.inventory
+      difficulty := state.gameServerState.difficulty
+      statementName := lvl.statementName
+      : Game.DidOpenLevelParams
+    }
+
+    let ctx ← mkWorkerContext state headerTask
+    let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
+      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk levelParams ctx (startAfterMs := 0)
+      | Except.error e   => throw (e : ElabTaskError))
+    let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
+
+
+    let s : WasmFileState := {
+      fileWorkerState := {
+        doc             := doc
+        initHeaderStx   := headerStx
+        pendingRequests := RBMap.empty
+        rpcSessions     := RBMap.empty
+      }
+      gameWorkerState := { levelParams }
+      headerTask
+    }
+    let fileState := state.fileState.insert params.textDocument.uri s
+    return {state with fileState}
+  return state
+
+@[export game_send_message]
+unsafe def sendMessage (s : String) (state : WasmServerState) : IO WasmServerState := do
+  let e ← IO.getStderr
+  try
+    let m ← readMessage s
+    match m with
+    | Message.request id "initialize" (some params) =>
+      let p : InitializeParams ← parseParams (toJson params)
+      initializeServer id
+      let p := {p with rootUri? := some (toString state.gameServerState.game)}
+      return {state with initParams? := some p}
+    | _ =>
+      let (isGameEv, state) ← runGameServerM state (Game.handleServerEvent (.clientMsg m))
+      if isGameEv then
+        return state
+      else
+        match m with
+        | Message.notification method (some params) =>
+            let handle := (fun α [FromJson α] (handler : α → WasmServerState → IO WasmServerState)
+              => parseParams (toJson params) >>= (handler · state))
+            match method with --TODO
+            | "textDocument/didOpen"            => handle DidOpenTextDocumentParams handleDidOpen
+            -- | "textDocument/didChange"          => handle DidChangeTextDocumentParams handleDidChange
+            -- | "textDocument/didClose"           => handle DidCloseTextDocumentParams handleDidClose
+            -- | "workspace/didChangeWatchedFiles" => handle DidChangeWatchedFilesParams handleDidChangeWatchedFiles
+            -- | "$/cancelRequest"                 => handle CancelParams handleCancelRequest
+            -- | "$/lean/rpc/connect"              => handle RpcConnectParams (forwardNotification method)
+            -- | "$/lean/rpc/release"              => handle RpcReleaseParams (forwardNotification method)
+            -- | "$/lean/rpc/keepAlive"            => handle RpcKeepAliveParams (forwardNotification method)
+            | _ => return state
+        | Message.request id method (some params) =>
+          let some uri ← requestWorkerUri method (toJson params)
+            | throwServerError s!"Could not find Uri for request: {method}"
+          let some fileState := state.fileState.find? uri
+            | throwServerError s!"File not open: {uri}"
+          let (_, fileState) ← runGameWorkerM state fileState do
+            MyServer.FileWorker.mainLoop1 m
+          let fileState := state.fileState.insert uri fileState
+          return {state with fileState}
+        | Message.responseError _ _ e .. =>
+          throwServerError s!"Unhandled response error: {e}"
+        | _ => throwServerError "Got invalid JSON-RPC message"
+        -- match m with
+        -- | _ =>
+        --   e.putStrLn s!"Expected JSON-RPC request, got: '{(toJson m).compress}'"
+        --   return state
+  catch err =>
+    e.putStrLn s!"Server error: {err}"
+    return state

server/Main.lean

@@ -1,5 +1,6 @@
 import GameServer.FileWorker
 import GameServer.Watchdog
+import GameServer.WasmServer
 import GameServer.Commands
 
 -- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`

server/lakefile.lean

@@ -3,6 +3,7 @@ open Lake DSL
 
 package GameServer
 
+@[default_target]
 lean_lib GameServer
 
 @[default_target]

server/lakefile32.lean

@@ -0,0 +1,15 @@
+import Lake
+open Lake DSL
+
+package GameServer {
+  buildDir := ".lake/build32"
+}
+
+@[default_target]
+lean_lib GameServer
+
+@[default_target]
+lean_exe gameserver {
+  root := `Main
+  supportInterpreter := true
+}

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0
+leanprover/lean4:v4.3.0-rc2

server/main.c

@@ -0,0 +1,58 @@
+#include <stdio.h>
+#include <lean/lean.h>
+
+extern lean_object* game_send_message(lean_object*, lean_object*, lean_object*);
+extern lean_object* game_make_state(lean_object*);
+
+// see https://leanprover.github.io/lean4/doc/dev/ffi.html#initialization
+extern void lean_initialize_runtime_module();
+extern void lean_initialize();
+extern void lean_io_mark_end_initialization();
+extern lean_object * initialize_GameServer_WasmServer(uint8_t builtin, lean_object *);
+
+lean_object * state;
+lean_object * io_world;
+
+
+void main() {
+  lean_initialize_runtime_module();
+  lean_initialize();
+  lean_object * res;
+  // use same default as for Lean executables
+  uint8_t builtin = 1;
+  io_world = lean_io_mk_world();
+  res = initialize_GameServer_WasmServer(builtin, io_world);
+  if (lean_io_result_is_ok(res)) {
+      lean_dec(res);
+  } else {
+      lean_io_result_show_error(res);
+      lean_dec(res);
+      return;  // do not access Lean declarations if initialization failed
+  }
+  lean_init_task_manager();
+  lean_io_mark_end_initialization();
+
+  res = game_make_state(io_world);
+  if (lean_io_result_is_ok(res)) {
+    state = lean_io_result_get_value(res);
+    lean_inc(state);
+    lean_dec(res);
+  } else {
+    lean_io_result_show_error(res);
+    lean_dec(res);
+    return;  // do not access Lean declarations if initialization failed
+  }
+}
+
+void send_message(char* msg){
+  lean_object * s = lean_mk_string(msg);
+  lean_object * res = game_send_message(s, state, io_world);
+  if (lean_io_result_is_ok(res)) {
+    state = lean_io_result_get_value(res);
+    lean_inc(state);
+    lean_dec(res);
+  } else {
+    lean_io_result_show_error(res);
+    lean_dec(res);
+  }
+}

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

wasm.sh

@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cd server
+
+mkdir -p .lake/toolchains
+if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst  ]
+then
+    wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_wasm32.tar.zst
+    tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst -C .lake/toolchains
+fi
+if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst  ]
+then
+    wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_x86.tar.zst
+    tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst -C .lake/toolchains
+fi
+
+# Linking will fail, but that's ok. We only need the c files.
+.lake/toolchains/lean-4.3.0-rc2-linux_x86/bin/lake build -f=lakefile32.lean
+
+
+lake build
+
+
+OUT_DIR=../client/public
+LEAN_SYSROOT=.lake/toolchains/lean-4.3.0-rc2-linux_wasm32
+LEAN_LIBDIR=$LEAN_SYSROOT/lib/lean
+
+emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR .lake/build/ir/GameServer/*.c -lInit -lLean -lleancpp -lleanrt \
+  -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 \
+  -sPTHREAD_POOL_SIZE_STRICT=2 \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Init"@/lib/Init \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Init.olean"@/lib/Init.olean \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Init.ilean"@/lib/Init.ilean \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean"@/lib/Lean \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.olean"@/lib/Lean.olean \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.ilean"@/lib/Lean.ilean \
+  --preload-file "./.lake/build32/lib"@/gamelib