From cc4321ff3f7cbf43747114cd56197a1b2bb0c457 Mon Sep 17 00:00:00 2001
From: joneugster <eugster.jon@gmail.com>
Date: Tue, 17 Oct 2023 16:01:39 +0200
Subject: [PATCH] Turn some logInfo into trace[debug] to toggle the off for
 building

---
 server/GameServer/AbstractCtx.lean |  1 +
 server/GameServer/Commands.lean    | 23 ++++++++++-------------
 server/test/test_statement.lean    |  2 +-
 3 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/server/GameServer/AbstractCtx.lean b/server/GameServer/AbstractCtx.lean
index 831c607..ab20709 100644
--- a/server/GameServer/AbstractCtx.lean
+++ b/server/GameServer/AbstractCtx.lean
@@ -1,4 +1,5 @@
 import Lean
+import GameServer.Utils
 
 section AbstractCtx
 open Lean
diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index ea4ffd0..7d4165e 100644
--- a/server/GameServer/Commands.lean
+++ b/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,8 +183,7 @@ 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 " ++
+      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."
-    else
-      logInfo "This branch leaves open goals."
+  let gs ← Tactic.getUnsolvedGoals
+  if gs.isEmpty then
+    trace[debug] "This branch finishes the proof."
+  else
+    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
-    logInfo s!"Template:\n{template}"
+  trace[debug] 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. -/
diff --git a/server/test/test_statement.lean b/server/test/test_statement.lean
index eb2f79c..c89ca84 100644
--- a/server/test/test_statement.lean
+++ b/server/test/test_statement.lean
@@ -22,7 +22,7 @@ Statement foo.bar2 : 3 ≤ 7 := by
   simp
 
 
-NewLemma foo.baz
+NewLemma foo.bar
 DisabledTactic tauto