Turn some logInfo into trace[debug] to toggle the off for building

server/GameServer/AbstractCtx.lean

@@ -1,4 +1,5 @@
 import Lean
+import GameServer.Utils
 
 section AbstractCtx
 open Lean

server/GameServer/Commands.lean

@@ -10,13 +10,14 @@ register_option lean4game.showDependencyReasons : Bool := {
   descr := "show reasons for calculated world dependencies."
 }
 
-/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
+/-- Let `MakeGame` print the reasons why the worlds depend on each other.
+
+Note: currently unused in favour of setting `set_option trace.debug true`. -/
 register_option lean4game.verbose : Bool := {
   defValue := false
   descr := "display more info messages to help developing the game."
 }
 
-
 /-! # Game metadata -/
 
 /-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/
@@ -182,7 +183,6 @@ def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.g
         name := name
         category := if type == .Lemma then s!"{n.getPrefix}" else ""
         content := s })
-      if lean4game.verbose.get (← getOptions) then
       logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
         m!"docstring) instead. If you want to write a different description, add " ++
         m!"`{type}Doc {name}` somewhere above this statement.")
@@ -589,12 +589,11 @@ elab (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do
   Tactic.evalTactic t
 
   -- Show an info whether the branch proofs all remaining goals.
-  if lean4game.verbose.get (← getOptions) then
   let gs ← Tactic.getUnsolvedGoals
   if gs.isEmpty then
-      logInfo "This branch finishes the proof."
+    trace[debug] "This branch finishes the proof."
   else
-      logInfo "This branch leaves open goals."
+    trace[debug] "This branch leaves open goals."
 
   let msgs ← Core.getMessageLog
   b.restore
@@ -639,8 +638,7 @@ elab "Template" tacs:tacticSeq : tactic => do
   Tactic.evalTactic tacs
   let newTacs : TSyntax `Lean.Parser.Tactic.tacticSeq := ⟨replaceHoles tacs.raw⟩
   let template ← PrettyPrinter.ppCategory `Lean.Parser.Tactic.tacticSeq newTacs
-  if lean4game.verbose.get (← getOptions) then
+  trace[debug] s!"Template:\n{template}"
-    logInfo s!"Template:\n{template}"
   modifyLevel (←getCurLevelId) fun level => do
     return {level with template := s!"{template}"}
 
@@ -1071,7 +1069,6 @@ elab "MakeGame" : command => do
         modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
           return level.setComputedInventory inventoryType itemsArray
 
-
 /-! # Debugging tools -/
 
 -- /-- Print current game for debugging purposes. -/

server/test/test_statement.lean

@@ -22,7 +22,7 @@ Statement foo.bar2 : 3 ≤ 7 := by
   simp
 
 
-NewLemma foo.baz
+NewLemma foo.bar
 DisabledTactic tauto