chore: hidden tactics do not need a doc entry #300

leanprover-community · Feb 25, 2025 · 28da6ea · 28da6ea
1 parent f878dd8
commit 28da6ea
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 17 deletions.
diff --git a/server/GameServer/Command/Doc.lean b/server/GameServer/Command/Doc.lean
@@ -94,8 +94,6 @@ elab "NewTactic" args:ident* : command => do
 /-- Declare tactics that are introduced by this level but do not show up in inventory. -/
 elab "NewHiddenTactic" args:ident* : command => do
   checkCommandNotDuplicated ((←getCurLevel).tactics.hidden) "NewHiddenTactic"
-  for name in ↑args do
-    checkInventoryDoc .Tactic name (template := "")
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId),
                                    hidden := level.tactics.hidden ++ args.map (·.getId)}}

diff --git a/server/GameServer/Command/MakeGame.lean b/server/GameServer/Command/MakeGame.lean
@@ -237,21 +237,24 @@ elab "MakeGame" : command => do
     -- Basic inventory item availability: all locked.
     let Availability₀ : Std.HashMap Name InventoryTile :=
       Std.HashMap.ofList $
-        ← allItems.toList.mapM fun item => do
-          -- Using a match statement because the error message of `Option.get!` is not helpful.
-          match (← getInventoryItem? item inventoryType) with
-          | none =>
+        ← allItems.toList.filterMapM fun item => do
+          match hiddenItems.contains item, (← getInventoryItem? item inventoryType) with
+          | true, _ =>
+            -- drop hidden items
+            return none
+          | false, none =>
             -- Note: we did have a panic here before because theorem statement and doc entry
             -- had mismatching namespaces
             logError m!"There is no inventory item ({inventoryType}) for: {item}."
             panic s!"Inventory item {item} not found!"
-          | some data =>
-            return (item, {
+          | false, some data =>
+            return some (item, {
               name := item
               displayName := data.displayName
               category := data.category
               altTitle := data.statement
-              hidden := hiddenItems.contains item })
+              -- TODO: we don't need `hidden` anymore
+              hidden := false })
 
 
 
@@ -264,7 +267,8 @@ elab "MakeGame" : command => do
       -- logInfo m!"Predecessors: {predecessors.toArray.map fun (a) => (a)}"
       for predWorldId in predecessors do
         for item in newItemsInWorld.getD predWorldId {} do
-          let data := (← getInventoryItem? item inventoryType).get!
+          let some data ← getInventoryItem? item inventoryType
+            | continue
           items := items.insert item {
             name := item
             displayName := data.displayName
@@ -284,7 +288,8 @@ elab "MakeGame" : command => do
 
         -- unlock items that are unlocked in this level
         for item in levelInfo.new do
-          let data := (← getInventoryItem? item inventoryType).get!
+          let some data ← getInventoryItem? item inventoryType
+            | continue
           items := items.insert item {
             name := item
             displayName := data.displayName
@@ -299,7 +304,8 @@ elab "MakeGame" : command => do
           match theoremStatements.get? (worldId, levelId) with
           | none => pure ()
           | some name =>
-            let data := (← getInventoryItem? name inventoryType).get!
+            let some data ← getInventoryItem? name inventoryType
+              | continue
             items := items.insert name {
               name := name
               displayName := data.displayName
@@ -331,10 +337,13 @@ elab "MakeGame" : command => do
     allItemsByType := allItemsByType.insert inventoryType allItems
 
   let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
-    (allItemsByType.getD type {}).toArray.mapM (fun name => do
-      let some item ← getInventoryItem? name type
-        | throwError "Expected item to exist: {name}"
-      return item.toTile)
+    (allItemsByType.getD type {}).toArray.filterMapM (fun name => do
+      match ← getInventoryItem? name type with
+      | none =>
+        if !(hiddenItems.contains name) then
+          logWarning s!"Expected item to exist: {name}"
+        return none
+      | some item => return some item.toTile)
   let inventory : InventoryOverview := {
     theorems := (← getTiles .Theorem).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
     tactics := (← getTiles .Tactic).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})

diff --git a/server/GameServer/SaveData.lean b/server/GameServer/SaveData.lean
@@ -52,7 +52,7 @@ def saveGameData (allItemsByType : Std.HashMap InventoryType (Std.HashSet Name))
   for inventoryType in [InventoryType.Theorem, .Tactic, .Definition] do
     for name in allItemsByType.getD inventoryType {} do
       let some item ← getInventoryItem? name inventoryType
-        | throwError "Expected item to exist: {name}"
+        | continue -- TODO: cleanup. Hidden items should also not appear in `allItemsByType`
       IO.FS.writeFile (path / docFileName inventoryType name) (toString (toJson item))
 
   IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))

diff --git a/server/TestGame/Levels/DemoWorld1/L01_HelloWorld.lean b/server/TestGame/Levels/DemoWorld1/L01_HelloWorld.lean
@@ -24,5 +24,6 @@ Conclusion "This last message appears if the level is solved."
 /- Use these commands to add items to the game's inventory. -/
 
 NewTactic rw rfl
+NewHiddenTactic simp
 -- NewTheorem Nat.add_comm Nat.add_assoc
 -- NewDefinition Nat Add Eq