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.*

README.md

@@ -2,15 +2,12 @@
 
 This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
 
-The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
-(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
-of Kevin Buzzard and Mohammad Pedramfar.
-The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
-
 ## Creating a Game
 
-Please follow the tutorial [Creating a Game](doc/create_game.md).
-In particular step 5 thereof explains [How to Run Games Locally](doc/running_locally.md).
+Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, the following steps might be of interest:
+
+* Step 5: [How to Run Games Locally](doc/running_locally.md)
+* Step 7: [How to Update an existing Game](doc/update_game.md)
 
 ### Publishing a Game
 
@@ -34,3 +31,10 @@ Contributions to `lean4game` are always welcome!
 ## Security
 
 Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap.
+
+## Credits
+
+The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
+(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
+of Kevin Buzzard and Mohammad Pedramfar.
+The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).

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

doc/create_game.md

@@ -4,7 +4,7 @@ This tutorial walks you through creating a new game for lean4. It covers from wr
 
 ## 1. Create the project
 
-1. Use the [NNG template](https://github.com/hhu-adam/NNG4) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
+1. Use the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
 2. Clone the game repo.
 3. Call `lake update && lake exe cache get && lake build` to build the Lean project.
 
@@ -243,6 +243,10 @@ Hint "now use `rw [{h}]` to use your assumption {h}."
 ```
 That way, the game will replace it with the actual name the assumption has in the player's proof state.
 
+## 7. Update your game
+
+In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](https://github.com/leanprover-community/lean4game/blob/main/doc/update_game.md).
+
 ## Further Notes
 
 Here are some random further things you should consider designing a new game:

doc/running_locally.md

@@ -4,13 +4,15 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
 
 There are several options to play a game locally:
 
-- VSCode Dev Container: needs `docker` installed on your machine
-- Codespaces: Needs active internet connection and computing time is limited.
-- Gitpod: does not work yet (I that true?)
-- Manual installation: Needs `npm` installed on your system
+1. VSCode Dev Container: needs `docker` installed on your machine
+2. Codespaces: Needs active internet connection and computing time is limited.
+3. Gitpod: does not work yet (Is that true?)
+4. Manual installation: Needs `npm` installed on your system
 
 The recommended option is "VSCode Dev containers" but you may choose any option above depending on your setup.
 
+The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) contains all the relevant files to make your local setup (dev container / gitpod / codespaces) work. You might need to update these files manually by copying them from there if you need any new improvements to the dev setup you're using in an existing game.
+
 ## VSCode Dev Containers
 
 1.  **Install Docker and Dev Containers** *(once)*:<br/>
@@ -27,9 +29,9 @@ The recommended option is "VSCode Dev containers" but you may choose any option
     Once you have the Dev Containers Extension installed, (re)open the project folder of your game in VSCode.
     A message appears asking you to "Reopen in Container".
 
-    * The first start will take a while, ca. 2-10 minutes. After the first
+    * The first start will take a while, ca. 2-15 minutes. After the first
       start this should be very quickly.
-    * Once built, you can open http://localhost:3000 in your browser. which should load the game
+    * Once built, you can open http://localhost:3000 in your browser. which should load the game.
 
 3.  **Editing Files** *(everytime)*:<br/>
     After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes.
@@ -42,12 +44,13 @@ The recommended option is "VSCode Dev containers" but you may choose any option
   you might have deleted stuff from docker via your shell. Try deleting the container and image
   explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
   container. (this will again take some time)
+* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
 
 ## Codespaces
 
 You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
 
-Note: You have to wait until npm started properly. In particular, this is after a message like `[client] webpack 5.81.0 compiled successfully in 38119 ms` appears in the terminal, which might take a good while.
+Note: You have to wait until npm started properly, which might take a good while.
 
 As with devcontainers, you need to run `lake build` after changing any lean files and then reload the browser.
 
@@ -73,15 +76,15 @@ Now install node:
 nvm install node
 ```
 
-Clone the game (e.g. `NNG4` here):
+Clone the game (e.g. `GameSkeleton` here):
 ```bash
-git clone https://github.com/hhu-adam/NNG4.git
-# or: git clone git@github.com:hhu-adam/NNG4.git
+git clone https://github.com/hhu-adam/GameSkeleton.git
+# or: git clone git@github.com:hhu-adam/GameSkeleton.git
 ```
 
 Download dependencies and build the game:
 ```bash
-cd NNG4
+cd GameSkeleton
 lake update
 lake exe cache get   # if your game depends on mathlib
 lake build
@@ -93,7 +96,7 @@ cd ..
 git clone https://github.com/leanprover-community/lean4game.git
 # or: git clone git@github.com:leanprover-community/lean4game.git
 ```
-The folders `NNG4` and `lean4game` must be in the same directory!
+The folders `GameSkeleton` and `lean4game` must be in the same directory!
 
 In `lean4game`, install dependencies:
 ```bash
@@ -106,15 +109,15 @@ Run the game:
 npm start
 ```
 
-This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/NNG4. Replace `NNG4` with the folder name of your local game.
+This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/GameSkeleton. Replace `GameSkeleton` with the folder name of your local game.
 
 ## Modifying the GameServer
 
-When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by setting `export NODE_ENV=development` inside your local game before building it:
+When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by setting `export LEAN4GAME=local` inside your local game before building it:
 
 ```bash
 cd NNG4
-export NODE_ENV=development
+export LEAN4GAME=local
 lake update
 lake build
 ```

doc/update_game.md

@@ -0,0 +1,37 @@
+# How to update your Game
+
+## New Lean version
+
+You can update the game to any Lean version by simply editing the `lean-toolchain` in your game repo to contain the
+new lean version `leanprover/lean4:v4.X.0`.
+
+Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https://github.com/leanprover-community/lean4game/tags).
+
+Then, depending on the setup you use, do one of the following:
+
+* Dev Container: Rebuild the VSCode Devcontainer.
+* Local Setup: run `lake update` (followed by `lake exe cache get` if you depend on mathlib.)
+* Gitpod/Codespaces: Create a fresh one
+
+This will update `lean4game` and `mathlib` in your project to the new lean version.
+
+## Newest developing setup
+
+There are a few files in your game repository which are used for the developing setup
+(dev container/codespaces/gitpod). If you need to update your're developing setup, for example because it doesn't work
+anymore, you will need to copy the relevant files from the [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) template into your game repo.
+
+The relevant files are:
+
+```
+lakefile.lean
+.devcontainer/**
+.docker/**
+.gitpod
+.vscode/**
+```
+
+simply copy them from the `GameSkeleton` into your game.
+
+(Note: You should not need to modify any of these files, with the exception of the `lakefile.lean`,
+where you need to add any dependencies of your game.)

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)
-      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
+  def mkHeaderTask (m : DocumentMeta) (hOut : FS.Stream) (paths : List System.FilePath)
+      (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
-    let ctx ← read
+  partial def mainLoop1 (msg : JsonRpc.Message): GameWorkerM Bool := do
     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