use initialization options for inventory

client/src/components/level.tsx

@@ -549,6 +549,9 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
   const uriStr = `file:///${worldId}/${levelId}`
   const uri = monaco.Uri.parse(uriStr)
 
+  const inventory: Array<String> = useSelector(selectInventory(gameId))
+  const difficulty: number = useSelector(selectDifficulty(gameId))
+
   useEffect(() => {
     const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri)
     if (onDidChangeContent) {
@@ -615,7 +618,7 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
     }
 
     // Following `vscode-lean4/webview/index.ts`
-    const client = new LeanClient(connectionProvider, showRestartMessage)
+    const client = new LeanClient(connectionProvider, showRestartMessage, {inventory, difficulty})
     const infoProvider = new InfoProvider(client)
     // const div: HTMLElement = infoviewRef.current!
     const imports = {

package-lock.json

@@ -31,7 +31,7 @@
         "debounce": "^1.2.1",
         "express": "^4.18.2",
         "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-        "lean4web": "github:hhu-adam/lean4web#03fe27835115d6b00c02e3f61cefd4a1ba9e3ae0",
+        "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
         "octokit": "^2.0.14",
         "path-browserify": "^1.0.1",
         "react": "^18.2.0",
@@ -10081,8 +10081,8 @@
     },
     "node_modules/lean4web": {
       "version": "0.1.0",
-      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#03fe27835115d6b00c02e3f61cefd4a1ba9e3ae0",
+      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
-      "integrity": "sha512-VwKtgF6CUQtC3616+/y4I4DURdaVNU7Bvs++tDbL39YDOSomjLyauLZzzyXRr8/CAFGsnaF13eiafENWMzZE5Q==",
+      "integrity": "sha512-s9qYeXuMNBGDPKC5IuFTjV/j8tQCRkZr+poYKEWljrM95rsz4JHIvjdEt891fE9JhPDLSN+iXNRXwIOCT6FlMg==",
       "dependencies": {
         "@emotion/react": "^11.11.1",
         "@emotion/styled": "^11.11.0",

package.json

@@ -28,7 +28,7 @@
     "debounce": "^1.2.1",
     "express": "^4.18.2",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-    "lean4web": "github:hhu-adam/lean4web#03fe27835115d6b00c02e3f61cefd4a1ba9e3ae0",
+    "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
     "octokit": "^2.0.14",
     "path-browserify": "^1.0.1",
     "react": "^18.2.0",

server/GameServer/FileWorker.lean

@@ -213,7 +213,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           modify (fun s => { s with messages := msgLog })
           parseResultRef.set (tacticStx, cmdParserState)
 
-          -- TODO: Check for forbidden tactics
+          -- Check for forbidden tactics
           findForbiddenTactics inputCtx gameWorkerState level tacticStx
 
           -- Insert invisible `skip` command to make sure we always display the initial goal
@@ -590,7 +590,7 @@ end MainLoop
 def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
-  let initRequest ← i.readLspRequestAs "initialize" InitializeParams
+  let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
   o.writeLspResponse {
     id     := initRequest.id
     result := {
@@ -616,20 +616,15 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
   let _ ← IO.setStderr e
   try
     let game ← loadGameData gameDir
-    let s : GameWorkerState:= {
+    let some initializationOptions := initRequest.param.initializationOptions?
-      -- uri := doc.uri
+      | throwServerError "no initialization options found"
-      -- gameDir := gameDir
+    let gameWorkerState : GameWorkerState:= {
-      -- levelModule := sorry
+      inventory := initializationOptions.inventory
-      -- tactics := sorry
+      difficulty := initializationOptions.difficulty
-      -- lemmas := sorry
-      -- definitions := sorry
-      inventory := #[] -- TODO: Ensure that this is set in time!
-      difficulty := 0 -- TODO: Ensure that this is set in time!
-      -- statementName := sorry
     }
-    let (ctx, st) ← initializeWorker meta i o e initRequest.param opts gameDir game s
+    let (ctx, st) ← initializeWorker meta i o e initRequest.param.toLeanInternal opts gameDir game gameWorkerState
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
-      StateT.run (s := s) <| (mainLoop)
+      StateT.run (s := gameWorkerState) <| (mainLoop)
     return (0 : UInt32)
   catch e =>
     IO.eprintln e

server/GameServer/Game.lean

@@ -25,6 +25,58 @@ open Lsp
 open JsonRpc
 open IO
 
+/- Game-specific version of `InitializeParams` that allows for extra options: -/
+
+structure InitializationOptions extends Lean.Lsp.InitializationOptions :=
+  difficulty : Nat
+  inventory : Array String
+  deriving ToJson, FromJson
+
+structure InitializeParams where
+  processId? : Option Int := none
+  clientInfo? : Option ClientInfo := none
+  /- We don't support the deprecated rootPath
+  (rootPath? : Option String) -/
+  rootUri? : Option String := none
+  initializationOptions? : Option InitializationOptions := none
+  capabilities : ClientCapabilities
+  /-- If omitted, we default to off. -/
+  trace : Trace := Trace.off
+  workspaceFolders? : Option (Array WorkspaceFolder) := none
+  deriving ToJson
+
+instance : FromJson InitializeParams where
+  fromJson? j := do
+    let processId? := j.getObjValAs? Int "processId"
+    let clientInfo? := j.getObjValAs? ClientInfo "clientInfo"
+    let rootUri? := j.getObjValAs? String "rootUri"
+    let initializationOptions? := j.getObjValAs? InitializationOptions "initializationOptions"
+    let capabilities ← j.getObjValAs? ClientCapabilities "capabilities"
+    let trace := (j.getObjValAs? Trace "trace").toOption.getD Trace.off
+    let workspaceFolders? := j.getObjValAs? (Array WorkspaceFolder) "workspaceFolders"
+    return ⟨
+      processId?.toOption,
+      clientInfo?.toOption,
+      rootUri?.toOption,
+      initializationOptions?.toOption,
+      capabilities,
+      trace,
+      workspaceFolders?.toOption⟩
+
+def InitializeParams.toLeanInternal (p : InitializeParams) : Lean.Lsp.InitializeParams :=
+{
+  processId? := p.processId?
+  clientInfo? := p.clientInfo?
+  rootUri? := p.rootUri?
+  initializationOptions? := p.initializationOptions?.map fun o => {
+    editDelay? := o.editDelay?
+    hasWidgets? := o.hasWidgets?
+  }
+  capabilities := p.capabilities
+  trace := p.trace
+  workspaceFolders? := p.workspaceFolders?
+}
+
 structure SetInventoryParams where
   inventory : Array String
   difficulty : Nat