turn missing doc error into warning

server/GameServer/Commands.lean

@@ -79,10 +79,10 @@ in the first level and get enabled during the game.
 /-! ## Doc entries -/
 
 /-- Throw an error if inventory doc does not exist -/
-def checkInventoryDoc (type : InventoryType) (name : Name) : CommandElabM Unit := do
+def checkInventoryDoc (type : InventoryType) (name : Syntax) : CommandElabM Unit := do
   let some _ := (inventoryDocExt.getState (← getEnv)).find?
-      (fun x => x.name == name && x.type == type)
+      (fun x => x.name == name.getId && x.type == type)
-    | throwError "Missing {type} Documentation: {name} (add `{type}Doc {name}` in your game's docs section)"
+    | logWarningAt name m!"Missing {type} Documentation: {name} (add `{type}Doc {name}` in your game's docs section)"
 
 /-- Documentation entry of a tactic. Example:
 
@@ -144,60 +144,60 @@ elab "DefinitionDoc" name:ident "as" displayName:str content:str : command =>
 
 /-- Declare tactics that are introduced by this level. -/
 elab "NewTactic" args:ident* : command => do
-  let names := args.map (·.getId)
+  for name in ↑args do checkInventoryDoc .Tactic name
-  for name in names do checkInventoryDoc .Tactic name
+  modifyCurLevel fun level => pure {level with
-  modifyCurLevel fun level => pure {level with tactics := {level.tactics with new := names}}
+    tactics := {level.tactics with new := args.map (·.getId)}}
 
 /-- Declare lemmas that are introduced by this level. -/
 elab "NewLemma" args:ident* : command => do
-  let names := args.map (·.getId)
+  for name in ↑args do checkInventoryDoc .Lemma name
-  for name in names do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with
-  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with new := names}}
+    lemmas := {level.lemmas with new := args.map (·.getId)}}
 
 /-- Declare definitions that are introduced by this level. -/
 elab "NewDefinition" args:ident* : command => do
-  let names := args.map (·.getId)
+  for name in ↑args do checkInventoryDoc .Definition name
-  for name in names do checkInventoryDoc .Definition name
+  modifyCurLevel fun level => pure {level with
-  modifyCurLevel fun level => pure {level with definitions := {level.definitions with new := names}}
+    definitions := {level.definitions with new := args.map (·.getId)}}
 
 /-- Declare tactics that are temporarily disabled in this level.
 This is ignored if `OnlyTactic` is set. -/
 elab "DisabledTactic" args:ident* : command => do
-  let names := args.map (·.getId)
+  for name in ↑args do checkInventoryDoc .Tactic name
-  -- for name in names do checkInventoryDoc .Tactic name
+  modifyCurLevel fun level => pure {level with
-  modifyCurLevel fun level => pure {level with tactics := {level.tactics with disabled := names}}
+    tactics := {level.tactics with disabled := args.map (·.getId)}}
 
 /-- Declare lemmas that are temporarily disabled in this level.
 This is ignored if `OnlyLemma` is set. -/
 elab "DisabledLemma" args:ident* : command => do
-  let names := args.map (·.getId)
+  for name in ↑args  do checkInventoryDoc .Lemma name
-  -- for name in names do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with
-  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with disabled := names}}
+    lemmas := {level.lemmas with disabled := args.map (·.getId)}}
 
 /-- Declare definitions that are temporarily disabled in this level -/
 elab "DisabledDefinition" args:ident* : command => do
-  let names := args.map (·.getId)
+  for name in ↑args do checkInventoryDoc .Definition name
-  -- for name in names do checkInventoryDoc .Definition name
+  modifyCurLevel fun level => pure {level with
-  modifyCurLevel fun level => pure {level with definitions := {level.definitions with disabled := names}}
+    definitions := {level.definitions with disabled := args.map (·.getId)}}
 
 /-- Temporarily disable all tactics except the ones declared here -/
 elab "OnlyTactic" args:ident* : command => do
-  let names := args.map (·.getId)
+  for name in ↑args do checkInventoryDoc .Tactic name
-  for name in names do checkInventoryDoc .Tactic name
+  modifyCurLevel fun level => pure {level with
-  modifyCurLevel fun level => pure {level with tactics := {level.tactics with only := names}}
+    tactics := {level.tactics with only := args.map (·.getId)}}
 
 /-- Temporarily disable all lemmas except the ones declared here -/
 elab "OnlyLemma" args:ident* : command => do
-  let names := args.map (·.getId)
+  for name in ↑args do checkInventoryDoc .Lemma name
-  for name in names do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with
-  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with only := names}}
+    lemmas := {level.lemmas with only := args.map (·.getId)}}
 
 /-- Temporarily disable all definitions except the ones declared here.
 This is ignored if `OnlyDefinition` is set. -/
 elab "OnlyDefinition" args:ident* : command => do
-  let names := args.map (·.getId)
+  for name in ↑args do checkInventoryDoc .Definition name
-  for name in names do checkInventoryDoc .Definition name
+  modifyCurLevel fun level => pure {level with
-  modifyCurLevel fun level => pure {level with definitions := {level.definitions with only := names}}
+    definitions := {level.definitions with only := args.map (·.getId)}}
 
 /-- Define which tab of Lemmas is opened by default. Usage: `LemmaTab "Nat"`.
 If omitted, the current tab will remain open. -/
@@ -235,7 +235,7 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
 
   -- Check that statement has a docs entry.
   match statementName with
-  | some name => checkInventoryDoc .Lemma name.getId
+  | some name => checkInventoryDoc .Lemma name
   | none => pure ()
 
   -- The default name of the statement is `[Game].[World].level[no.]`, e.g. `NNG.Addition.level1`

server/test/test_statement.lean

@@ -5,10 +5,21 @@ Game "Test"
 World "TestW"
 Level 1
 
+/- Missing doc -/
+
+-- Shows warning on `foo.bar`:
+Statement foo.bar "some text" : 5 ≤ 7 := by
+  simp
+
+NewLemma foo.baz
+DisabledTactic tauto
+
+/- Other tests -/
+
 LemmaDoc add_zero as "add_zero" in "Nat" "(nothing)"
 
-@[simp] Statement add_zero "test" (n : Nat) : n + n = n := by
+Statement add_zero "test" (n : Nat) : n + 0 = n := by
-  sorry
+  rfl
 
 Statement (n : Nat) : 0 + n = n := by
   Template
@@ -23,5 +34,5 @@ NewLemma add_zero
 
 #print add_zero
 
-theorem xy (n : Nat) : n + n = n := by
+theorem xy (n : Nat) : n + 0 = n := by
   simp