Merge branch 'main' of github.com:leanprover-community/lean4game

server/leanserver/GameServer/Commands.lean

@@ -79,9 +79,12 @@ elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : comma
   -- | none => `(lemma $(mkIdent "XX") $sig $val) -- TODO: Make it into an `example`
   -- | some name => `(lemma $name $sig $val)
 
+  let scope ← getScope
+
   elabCommand thmStatement
   modifyCurLevel fun level => pure {level with
     goal := sig,
+    scope := scope,
     descrText := descr.getString,
     descrFormat := match statementName with
     | none => "example " ++ (toString <| reprint sig.raw) ++ " := by"
@@ -187,17 +190,28 @@ elab "TacticDoc" name:ident content:str : command =>
 instance : Quote TacticDocEntry `term :=
 ⟨λ entry => Syntax.mkCApp ``TacticDocEntry.mk #[quote entry.name, quote entry.content]⟩
 
+/-- Throw an error if tactic doc does not exist -/
+def checkTacticDoc (name : Name) : CommandElabM Unit := do
+  let some _ := (tacticDocExt.getState (← getEnv)).find? (·.name = name)
+    | throwError "Missing Tactic Documentation: {name}"
+
 /-- Declare tactics that are introduced by this level. -/
 elab "NewTactics" args:ident* : command => do
-  modifyCurLevel fun level => pure {level with newTactics := args.map (·.getId)}
+  let names := args.map (·.getId)
+  for name in names do checkTacticDoc name
+  modifyCurLevel fun level => pure {level with newTactics := names}
 
 /-- Declare tactics that are temporarily disabled in this level -/
 elab "DisabledTactics" args:ident* : command => do
-  modifyCurLevel fun level => pure {level with disabledTactics := args.map (·.getId)}
+  let names := args.map (·.getId)
+  for name in names do checkTacticDoc name
+  modifyCurLevel fun level => pure {level with disabledTactics := names}
 
 /-- Temporarily disable all tactics except the ones declared here -/
 elab "OnlyTactics" args:ident* : command => do
-  modifyCurLevel fun level => pure {level with onlyTactics := args.map (·.getId)}
+  let names := args.map (·.getId)
+  for name in names do checkTacticDoc name
+  modifyCurLevel fun level => pure {level with onlyTactics := names}
 
 /-! ## Lemmas -/
 

server/leanserver/GameServer/EnvExtensions.lean

@@ -161,9 +161,10 @@ deriving ToJson, FromJson, Repr
 def getCurLevelId [MonadError m] : m LevelId := do
   return { game := ← getCurGameId, world := ← getCurWorldId, level := ← getCurLevelIdx}
 
+/-- Instance to make GameLevel Repr work -/
+instance : Repr Elab.Command.Scope := ⟨fun s _ => repr s.currNamespace⟩
+
 /--
-
-
 Fields:
 - TODO
 - introduction: Theory block shown all the time.
@@ -195,6 +196,7 @@ structure GameLevel where
   lemmas: Array Availability := default
   hints: Array GoalHintEntry := default
   goal : TSyntax `Lean.Parser.Command.declSig := default
+  scope : Elab.Command.Scope := default
   descrText: String := default
   descrFormat : String := default
   deriving Inhabited, Repr

server/leanserver/GameServer/FileWorker.lean

@@ -77,13 +77,24 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (level : GameL
   | .atom info val =>
     -- ignore syntax elements that do not start with a letter
     -- and ignore "with" keyword
-    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ val != "with" then
+    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ val != "with" ∧ val != "at" then
       if ¬ ((level.tactics.map (·.name.toString))).contains val then
         addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"
       else if level.disabledTactics.contains val
         ∨ (¬ level.onlyTactics.isEmpty ∧ ¬ level.onlyTactics.contains val)then
         addErrorMessage info s!"The tactic '{val}' is disabled in this level!"
-  | .ident info rawVal val preresolved => return ()
+  | .ident info rawVal val preresolved =>
+      let ns ←
+        try resolveGlobalConst (mkIdent val)
+        catch | _ => pure [] -- catch "unknown constant" error
+      for n in ns do
+        let some (.thmInfo ..) := (← getEnv).find? n
+          | return () -- not a theroem -> ignore
+        if ¬ ((level.lemmas.map (·.name))).contains n then
+          addErrorMessage info s!"You have not unlocked the lemma '{n}' yet!"
+        else if level.disabledLemmas.contains n
+          ∨ (¬ level.onlyLemmas.isEmpty ∧ ¬ level.onlyLemmas.contains n)then
+          addErrorMessage info s!"The lemma '{n}' is disabled in this level!"
 where addErrorMessage (info : SourceInfo) (s : MessageData) :=
   modify fun st => { st with
     messages := st.messages.add {
@@ -139,10 +150,10 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
 
-          let cmdStx ← `(command|
-            set_option tactic.hygienic false in
-            theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
-          Elab.Command.elabCommandTopLevel cmdStx)
+          let cmdStx ← `(command| theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
+
+          Elab.Command.withScope (fun _ => level.scope) do -- use open namespaces and options as in the file
+            Elab.Command.elabCommandTopLevel cmdStx)
         cmdCtx cmdStateRef
     let postNew := (← tacticCacheNew.get).post
     snap.tacticCache.modify fun _ => { pre := postNew, post := {} }

server/leanserver/GameServer/Watchdog.lean

@@ -102,6 +102,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
   let i ← maybeTee "wdIn.txt" false i
   let o ← maybeTee "wdOut.txt" true o
   let e ← maybeTee "wdErr.txt" true e
+  let state := {env := ← createEnv, game := `TestGame}
   let initRequest ← i.readLspRequestAs "initialize" InitializeParams
   o.writeLspResponse {
     id     := initRequest.id
@@ -114,7 +115,6 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
       : InitializeResult
     }
   }
-  let state := {env := ← createEnv, game := `TestGame}
   let context : ServerContext := {
     hIn            := i
     hOut           := o