lock tactics based on local storage

client/src/components/level.tsx

@@ -30,19 +30,20 @@ import { faBars, faHome, faCircleInfo, faArrowRight, faArrowLeft, faShield, faRo
 import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles';
 
 import { GameIdContext } from '../app';
-import { ConnectionContext, useLeanClient } from '../connection';
+import { ConnectionContext, connection, useLeanClient } from '../connection';
 import { useAppDispatch, useAppSelector } from '../hooks';
 import { Button } from './button'
 import Markdown from './markdown';
 import {Inventory, Documentation} from './inventory';
 import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api';
-import { changedSelection, codeEdited, selectCode, selectSelections, progressSlice, selectCompleted, helpEdited, selectHelp, selectDifficulty } from '../state/progress';
+import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited, selectHelp, selectDifficulty, selectInventory } from '../state/progress';
 import { DualEditor } from './infoview/main'
 import { DeletedHint, DeletedHints, Hints } from './hints';
 import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './infoview/context';
 import { hasInteractiveErrors } from './infoview/command_line';
 import { GameHint } from './infoview/rpc_api';
 import { Impressum } from './privacy_policy';
+import { store } from '../state/store';
 
 function Level() {
 
@@ -73,8 +74,6 @@ function PlayableLevel({worldId, levelId}) {
   // a new proof has been entered. e.g. to consult messages coming from dead ends
   const [deletedChat, setDeletedChat] = useState<Array<GameHint>>([])
 
-  const store = useStore()
-
   // A set of row numbers where help is displayed
   const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
 
@@ -91,6 +90,8 @@ function PlayableLevel({worldId, levelId}) {
 
   const [impressum, setImpressum] = React.useState(false)
 
+  const difficulty = useSelector(selectDifficulty(gameId))
+
   function closeImpressum() {
     setImpressum(false)
   }
@@ -99,6 +100,13 @@ function PlayableLevel({worldId, levelId}) {
     setImpressum(!impressum)
   }
 
+  const inventory: Array<String> = useSelector(selectInventory(gameId))
+
+  React.useEffect(() => {
+    let leanClient = connection.getLeanClient(gameId)
+    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, checkEnabled: difficulty > 0})
+  }, [inventory])
+
   useEffect(() => {
     // // Scroll to top when loading a new level
     // // TODO: Thats the wrong behaviour probably

client/src/state/progress.ts

@@ -24,11 +24,19 @@ interface WorldProgressState {
 
 export interface GameProgressState {
   inventory: string[],
-  // Difficulty: the default is 2.
   difficulty: number,
   data: WorldProgressState
 }
 
+/**
+ * Currently we have three difficulties:
+ *
+ *   | lock tactics | lock levels |
+ * --|--------------|-------------|
+ * 0 |      no      |      no     |
+ * 1 |     yes      |      no     |
+ * 2 |     yes      |     yes     |
+ */
 const DEFAULT_DIFFICULTY = 2
 
 /** The progress made on all lean4-games */

server/GameServer/FileWorker.lean

@@ -74,11 +74,19 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
     let allowed := ["with", "fun", "at", "only"]
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      match levelParams.tactics.find? (fun t => t.name.toString == val) with
-      | none => addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
+      match levelParams.tactics.find? (·.name.toString == val) with
+      | none =>
+        -- Note: This case means that the tactic will never be introduced in the game.
+        match levelParams.inventory.find? (· == val) with
+        | none =>
+          addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
+        | some _ => pure () -- tactic is in the inventory, allow it.
       | some tac =>
         if tac.locked then
-          addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
+          match levelParams.inventory.find? (· == val) with
+          | none =>
+            addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
+          | some _ => pure () -- tactic is in the inventory, allow it.
         else if tac.disabled then
           addWarningMessage info s!"The tactic '{val}' is disabled in this level!"
   | .ident info rawVal val preresolved =>
@@ -108,8 +116,8 @@ where addWarningMessage (info : SourceInfo) (s : MessageData) :=
 
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
-    (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams)
-    (checkForbiddenTactics := true) : IO Snapshot := do
+    (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams)
+    (initParams : Lsp.InitializeParams) : IO Snapshot := do
   -- Recognize end snap
   if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
     let endSnap : Snapshot := {
@@ -162,7 +170,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           parseResultRef.set (tacticStx, cmdParserState)
 
           -- Check for forbidden tactics
-          if checkForbiddenTactics then
+          if levelParams.checkEnabled then
             findForbiddenTactics inputCtx levelParams tacticStx
 
           -- Insert invisible `skip` command to make sure we always display the initial goal
@@ -302,14 +310,21 @@ where
 
 end Elab
 
+structure GameWorkerState :=
+(levelParams : Game.DidOpenLevelParams)
+
+abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
+
 section Updates
 
 /-- Given the new document, updates editable doc state. -/
-  def updateDocument (newMeta : DocumentMeta) (levelParams : Game.DidOpenLevelParams) : WorkerM Unit := do
+  def updateDocument (newMeta : DocumentMeta) : GameWorkerM Unit := do
+    let s ← get
+    let levelParams := s.levelParams
     let ctx ← read
-    let oldDoc := (←get).doc
+    let oldDoc := (← StateT.lift get).doc
     oldDoc.cancelTk.set
-    let initHeaderStx := (← get).initHeaderStx
+    let initHeaderStx := (← StateT.lift get).initHeaderStx
     let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext
     let cancelTk ← CancelToken.new
     let headSnapTask := oldDoc.cmdSnaps.waitHead?
@@ -349,7 +364,8 @@ section Updates
       -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
       unfoldSnaps newMeta validSnaps.toArray cancelTk levelParams ctx
         (startAfterMs := ctx.initParams.editDelay.toUInt32)
-    modify fun st => { st with doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk } }
+    StateT.lift <| modify fun st => { st with
+      doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
 
 end Updates
 
@@ -361,7 +377,8 @@ section Initialization
     fileMap  := default
 
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-    (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams): IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
+      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
+      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"] }
@@ -449,10 +466,10 @@ end Initialization
 
 section NotificationHandling
 
-  def handleDidChange (levelParams : Game.DidOpenLevelParams) (p : DidChangeTextDocumentParams) : WorkerM Unit := do
+  def handleDidChange (p : DidChangeTextDocumentParams) : GameWorkerM Unit := do
     let docId := p.textDocument
     let changes := p.contentChanges
-    let oldDoc := (←get).doc
+    let oldDoc := (← StateT.lift get).doc
     let some newVersion ← pure docId.version?
       | throwServerError "Expected version number"
     if newVersion ≤ oldDoc.meta.version then
@@ -460,28 +477,28 @@ section NotificationHandling
       IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
     else if ¬ changes.isEmpty then
       let newDocText := foldDocumentChanges changes oldDoc.meta.text
-      updateDocument ⟨docId.uri, newVersion, newDocText⟩ levelParams
+      updateDocument ⟨docId.uri, newVersion, newDocText⟩
 
 end NotificationHandling
 
 section MessageHandling
 
-  def handleNotification (method : String) (params : Json) (levelParams : Game.DidOpenLevelParams) : WorkerM Unit := do
-    let handle := fun paramType [FromJson paramType] (handler : paramType → WorkerM Unit) =>
-      parseParams paramType params >>= handler
+  def handleNotification (method : String) (params : Json) : GameWorkerM Unit := do
+    let handle := fun paramType [FromJson paramType] (handler : paramType → GameWorkerM Unit) =>
+      (StateT.lift <| parseParams paramType params) >>= handler
     match method with
-    | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange levelParams)
-    | "$/cancelRequest"        => handle CancelParams handleCancelRequest
-    | "$/lean/rpc/release"     => handle RpcReleaseParams handleRpcRelease
-    | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams handleRpcKeepAlive
+    | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
+    | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
+    | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
+    | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
     | _                        => throwServerError s!"Got unsupported notification method: {method}"
 
 end MessageHandling
 
 section MainLoop
-  partial def mainLoop (levelParams : Game.DidOpenLevelParams) : WorkerM Unit := do
+  partial def mainLoop : GameWorkerM Unit := do
     let ctx ← read
-    let mut st ← get
+    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
@@ -504,16 +521,25 @@ section MainLoop
     set st
     match msg with
     | Message.request id method (some params) =>
+      -- TODO: What's this error message?
       if method == "Game.getInteractiveGoals" then throwServerError "HELLO"
       handleRequest id method (toJson params)
-      mainLoop levelParams
+      mainLoop
     | Message.notification "exit" none =>
       let doc := st.doc
       doc.cancelTk.set
       return ()
+    | Message.notification "$/game/setInventory" params =>
+      let p := (← parseParams Game.SetInventoryParams (toJson params))
+      let s ← get
+
+      set {s with levelParams := {s.levelParams with
+        inventory := p.inventory,
+        checkEnabled := p.checkEnabled}}
+      mainLoop
     | Message.notification method (some params) =>
-      handleNotification method (toJson params) levelParams
-      mainLoop levelParams
+      handleNotification method (toJson params)
+      mainLoop
     | _ => throwServerError "Got invalid JSON-RPC message"
 end MainLoop
 
@@ -535,11 +561,15 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let _ ← IO.setStderr e
   try
     let (ctx, st) ← initializeWorker meta i o e initParams.param opts levelParams
-    let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) (mainLoop levelParams)
+    let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
+      StateT.run (s := {levelParams := levelParams}) <| (mainLoop)
     return (0 : UInt32)
   catch e =>
     IO.eprintln e
-    publishDiagnostics meta #[{ range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, severity? := DiagnosticSeverity.error, message := e.toString }] o
+    publishDiagnostics meta #[{
+      range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩,
+      severity? := DiagnosticSeverity.error,
+      message := e.toString }] o
     return (1 : UInt32)
 
 def workerMain (opts : Options) : IO UInt32 := do

server/GameServer/Game.lean

@@ -6,6 +6,8 @@ structure GameServerState :=
 (env : Lean.Environment)
 (game : Name)
 (gameDir : String)
+(inventory : Array String)
+(checkEnabled : Bool)
 
 abbrev GameServerM := StateT GameServerState Server.Watchdog.ServerM
 
@@ -70,6 +72,9 @@ structure DidOpenLevelParams where
   tactics : Array InventoryTile
   lemmas : Array InventoryTile
   definitions : Array InventoryTile
+  inventory : Array String
+  /-- if true the server gives warnings for used tactics/lemmas that are not unlocked. -/
+  checkEnabled : Bool
   deriving ToJson, FromJson
 
 structure LoadDocParams where
@@ -77,6 +82,11 @@ structure LoadDocParams where
   type : InventoryType
 deriving ToJson, FromJson
 
+structure SetInventoryParams where
+  inventory : Array String
+  checkEnabled : Bool
+deriving ToJson, FromJson
+
 def handleDidOpenLevel (params : Json) : GameServerM Unit := do
   let p ← parseParams _ params
   let m := p.textDocument
@@ -90,15 +100,18 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
       c.hLog.putStr s!"Level not found: {m.uri} {c.initParams.rootUri?}"
       c.hLog.flush
   -- Send an extra notification to the file worker to inform it about the level data
+  let s ← get
   fw.stdin.writeLspNotification {
     method := "$/game/didOpenLevel"
     param  := {
       uri := m.uri
-      gameDir := (← get).gameDir
+      gameDir := s.gameDir
       levelModule := lvl.module
       tactics := lvl.tactics.tiles
       lemmas := lvl.lemmas.tiles
       definitions := lvl.definitions.tiles
+      inventory := s.inventory
+      checkEnabled := s.checkEnabled
       : DidOpenLevelParams
     }
   }
@@ -160,6 +173,16 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       -- let doc : InventoryItem := { doc with
       --   name := doc.name.toString }
       c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
+      return true
+    | Message.notification "$/game/setInventory" params =>
+      let p := (← parseParams SetInventoryParams (toJson params))
+      let s ← get
+      set {s with inventory := p.inventory, checkEnabled := p.checkEnabled}
+      let st ← read
+      let workers ← st.fileWorkersRef.get
+      for (_, fw) in workers do
+        fw.stdin.writeLspMessage msg
+
       return true
     | Message.request id "loadInventoryOverview" _ =>
       let s ← get

server/GameServer/Watchdog.lean

@@ -109,7 +109,13 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
   let i ← maybeTee "wdIn.txt" false i
   let o ← maybeTee "wdOut.txt" true o
   let e ← maybeTee "wdErr.txt" true e
-  let state := {env := ← createEnv gameDir module, game := gameName, gameDir := gameDir}
+  let state := {
+    env := ← createEnv gameDir module,
+    game := gameName,
+    gameDir := gameDir,
+    inventory := #[]
+    checkEnabled := false
+    }
   let initRequest ← i.readLspRequestAs "initialize" InitializeParams
   -- We misuse the `rootUri` field to the gameName
   let rootUri? := gameName