lean4game.verbose option

server/GameServer/Commands.lean

@@ -10,6 +10,13 @@ register_option lean4game.showDependencyReasons : Bool := {
   descr := "show reasons for calculated world dependencies."
 }
 
+/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
+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"` -/
@@ -108,6 +115,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 " ++
         m!"docstring) instead. If you want to write a different description, add " ++
         m!"`{type}Doc {name}` somewhere above this statement.")
@@ -220,6 +228,7 @@ elab "NewTactic" args:ident* : command => do
 
 /-- Declare tactics that are introduced by this level. -/
 elab "NewHiddenTactic" args:ident* : command => do
+  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)}}
@@ -509,6 +518,7 @@ 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."
@@ -558,6 +568,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}"
   modifyLevel (←getCurLevelId) fun level => do
     return {level with template := s!"{template}"}