From 43ddced24d641f136b1dece4535a90b07fcbc8bc Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 14 Dec 2023 20:57:04 +0100 Subject: [PATCH] use initialization options for inventory --- client/src/components/level.tsx | 5 ++- package-lock.json | 6 ++-- package.json | 2 +- server/GameServer/FileWorker.lean | 23 ++++++-------- server/GameServer/Game.lean | 52 +++++++++++++++++++++++++++++++ 5 files changed, 69 insertions(+), 19 deletions(-) diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 4aa3daa..7541752 100644 --- a/client/src/components/level.tsx +++ b/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 = 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 = { diff --git a/package-lock.json b/package-lock.json index c985568..7f459aa 100644 --- a/package-lock.json +++ b/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", - "integrity": "sha512-VwKtgF6CUQtC3616+/y4I4DURdaVNU7Bvs++tDbL39YDOSomjLyauLZzzyXRr8/CAFGsnaF13eiafENWMzZE5Q==", + "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#b91645a7b88814675ba9f99817436d0a2ce3a0ec", + "integrity": "sha512-s9qYeXuMNBGDPKC5IuFTjV/j8tQCRkZr+poYKEWljrM95rsz4JHIvjdEt891fE9JhPDLSN+iXNRXwIOCT6FlMg==", "dependencies": { "@emotion/react": "^11.11.1", "@emotion/styled": "^11.11.0", diff --git a/package.json b/package.json index d461744..8ac56a5 100644 --- a/package.json +++ b/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", diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index c4d0dff..95ae3e5 100644 --- a/server/GameServer/FileWorker.lean +++ b/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:= { - -- uri := doc.uri - -- gameDir := gameDir - -- levelModule := sorry - -- tactics := sorry - -- 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 some initializationOptions := initRequest.param.initializationOptions? + | throwServerError "no initialization options found" + let gameWorkerState : GameWorkerState:= { + inventory := initializationOptions.inventory + difficulty := initializationOptions.difficulty } - 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 diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean index bb7b0bc..177f3ef 100644 --- a/server/GameServer/Game.lean +++ b/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