From 13233710e9b279c5f022ea0b3e3e8315fa05c266 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 15 May 2023 15:09:27 +0200
Subject: [PATCH] modified inventory doc requirement

---
 server/GameServer/Commands.lean      | 38 +++++++++++++++++++++++-----
 server/GameServer/EnvExtensions.lean |  2 +-
 server/GameServer/Game.lean          |  2 +-
 server/index.mjs                     |  4 +--
 4 files changed, 35 insertions(+), 11 deletions(-)

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index d909dc6..9a1da1f 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -78,11 +78,33 @@ 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 : Syntax) : CommandElabM Unit := do
+/-- Throw a warning if inventory doc does not exist. If `(default := _)` is provided,
+it will create a new inverntory entry with the specified default description. -/
+def checkInventoryDoc (type : InventoryType) (name : Syntax)
+    (default : Option (String) := none) : CommandElabM Unit := do
   let some _ := (inventoryDocExt.getState (← getEnv)).find?
       (fun x => x.name == name.getId && x.type == type)
-    | logWarningAt name m!"Missing {type} Documentation: {name} (add `{type}Doc {name}` in your game's docs section)"
+    | match default with
+      | some _ =>
+        logInfoAt name (m!"Missing {type} Documentation: {name}, used provided default (e.g. " ++
+        m!"statement description) instead. If you want to write your own description, add " ++
+        m!"`{type}Doc {name}` somewhere above this statement.")
+      | none =>
+        logWarningAt name (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
+        m!"somewhere above this statement.")
+
+      let default₀ := match default with
+      | some d => d
+      | none => "missing"
+
+      -- Create a default inventory entry
+      let n := name.getId
+      modifyEnv (inventoryDocExt.addEntry · {
+        name := n
+        type := type
+        displayName :=  s!"{n}" -- TODO: for lemmas, only take the last part of the name
+        category := if type == .Lemma then s!"{n.getPrefix}" else ""
+        content := default₀ })
 
 /-- Documentation entry of a tactic. Example:
 
@@ -230,12 +252,16 @@ syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
 elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
 
+  let descr := match descr with
+    | none => none
+    | some s => s.getString
+
   -- Save the messages before evaluation of the proof.
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
 
   -- Check that statement has a docs entry.
   match statementName with
-  | some name => checkInventoryDoc .Lemma name
+  | some name => checkInventoryDoc .Lemma name (default := descr)
   | none => pure ()
 
   -- The default name of the statement is `[Game].[World].level[no.]`, e.g. `NNG.Addition.level1`
@@ -317,9 +343,7 @@ Only the existing statement will be available in later levels:
     module := env.header.mainModule
     goal := sig,
     scope := scope,
-    descrText := match descr with
-    | none => ""
-    | some s => s.getString
+    descrText := descr
     statementName := match statementName with
     | none => default
     | some name => name.getId
diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index 8c1f9b1..55bf9aa 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -183,7 +183,7 @@ structure GameLevel where
   goal : TSyntax `Lean.Parser.Command.declSig := default
   scope : Elab.Command.Scope := default
   /-- The mathematical statement in mathematician-readable form. (markdown) -/
-  descrText: String := default
+  descrText: Option String := none
   descrFormat : String := default
   /-- The `category` of lemmas to be open by default -/
   lemmaTab: Option String := none
diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean
index 7ec447c..230f818 100644
--- a/server/GameServer/Game.lean
+++ b/server/GameServer/Game.lean
@@ -45,7 +45,7 @@ structure LevelInfo where
   definitions : Array ComputedInventoryItem
   introduction : String
   conclusion : String
-  descrText : String := ""
+  descrText : Option String := none
   descrFormat : String := ""
   lemmaTab : Option String
   statementName : Option String
diff --git a/server/index.mjs b/server/index.mjs
index 2c4ad39..35164b1 100644
--- a/server/index.mjs
+++ b/server/index.mjs
@@ -18,13 +18,13 @@ import { importTrigger, importStatus } from './import.mjs'
 const games = {
     "g/hhu-adam/robo": {
         name: "Adam",
-        module: "Adam",
+        module: "Game",
         dir: "../../../../Robo",
         queueLength: 5
     },
     "g/hhu-adam/nng4": {
         name: "NNG",
-        module: "NNG",
+        module: "Game",
         dir: "../../../../NNG4",
         queueLength: 5
     }