throw error in regular difficulty if tactic not unlocked

client/src/components/level.tsx

@@ -284,7 +284,7 @@ function PlayableLevel({impressum, setImpressum}) {
   // if the user inventory changes, notify the server
   useEffect(() => {
     let leanClient = connection.getLeanClient(gameId)
-    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, checkEnabled: difficulty > 0})
+    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty})
   }, [inventory])
 
   useEffect(() => {

server/GameServer/FileWorker.lean

@@ -61,13 +61,13 @@ section Elab
 /-- Find all tactics in syntax object that are forbidden according to a
 set `allowed` of allowed tactics. -/
 partial def findForbiddenTactics (inputCtx : Parser.InputContext)
-    (levelParams : Game.DidOpenLevelParams) (stx : Syntax) :
+    (levelParams : Game.DidOpenLevelParams) (stx : Syntax) (asError : Bool) :
     Elab.Command.CommandElabM Unit := do
   match stx with
   | .missing => return ()
   | .node info kind args =>
     for arg in args do
-      findForbiddenTactics inputCtx levelParams arg
+      findForbiddenTactics inputCtx levelParams arg asError
   | .atom info val =>
     -- ignore syntax elements that do not start with a letter
     -- and ignore "with" keyword
@@ -108,7 +108,7 @@ where addWarningMessage (info : SourceInfo) (s : MessageData) :=
   modify fun st => { st with
     messages := st.messages.add {
       fileName := inputCtx.fileName
-      severity := MessageSeverity.warning
+      severity := if asError then MessageSeverity.error else MessageSeverity.warning
       pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
       data     := s
     }
@@ -170,8 +170,9 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           parseResultRef.set (tacticStx, cmdParserState)
 
           -- Check for forbidden tactics
-          if levelParams.checkEnabled then
+          if levelParams.difficulty > 0 then
             findForbiddenTactics inputCtx levelParams tacticStx
+              (asError := levelParams.difficulty > 1)
 
           -- Insert invisible `skip` command to make sure we always display the initial goal
           let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
@@ -533,7 +534,7 @@ section MainLoop
 
       set {s with levelParams := {s.levelParams with
         inventory := p.inventory,
-        checkEnabled := p.checkEnabled}}
+        difficulty := p.difficulty}}
       mainLoop
     | Message.notification method (some params) =>
       handleNotification method (toJson params)

server/GameServer/Game.lean

@@ -7,7 +7,7 @@ structure GameServerState :=
 (game : Name)
 (gameDir : String)
 (inventory : Array String)
-(checkEnabled : Bool)
+(difficulty : Nat)
 
 abbrev GameServerM := StateT GameServerState Server.Watchdog.ServerM
 
@@ -79,8 +79,13 @@ structure DidOpenLevelParams where
   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
+  Check for tactics/theorems that are not unlocked.
+  0: no check
+  1: give warnings
+  2: give errors
+  -/
+  difficulty : Nat
   deriving ToJson, FromJson
 
 structure LoadDocParams where
@@ -90,7 +95,7 @@ deriving ToJson, FromJson
 
 structure SetInventoryParams where
   inventory : Array String
-  checkEnabled : Bool
+  difficulty : Nat
 deriving ToJson, FromJson
 
 def handleDidOpenLevel (params : Json) : GameServerM Unit := do
@@ -117,7 +122,7 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
       lemmas := lvl.lemmas.tiles
       definitions := lvl.definitions.tiles
       inventory := s.inventory
-      checkEnabled := s.checkEnabled
+      difficulty := s.difficulty
       : DidOpenLevelParams
     }
   }
@@ -205,7 +210,7 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
     | Message.notification "$/game/setInventory" params =>
       let p := (← parseParams SetInventoryParams (toJson params))
       let s ← get
-      set {s with inventory := p.inventory, checkEnabled := p.checkEnabled}
+      set {s with inventory := p.inventory, difficulty := p.difficulty}
       let st ← read
       let workers ← st.fileWorkersRef.get
       for (_, fw) in workers do

server/GameServer/Watchdog.lean

@@ -114,7 +114,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
     game := gameName,
     gameDir := gameDir,
     inventory := #[]
-    checkEnabled := false
+    difficulty := 0
     }
   let initRequest ← i.readLspRequestAs "initialize" InitializeParams
   -- We misuse the `rootUri` field to the gameName