fixes for v4.6.0-rc1

.github/workflows/build.yml

@@ -1,8 +1,6 @@
 name: Build
 run-name: Build the project
-on:
+on: [push]
-  workflow_dispatch:
-  push:
 jobs:
   build:
     runs-on: ubuntu-latest

client/src/components/hints.tsx

@@ -5,33 +5,15 @@ import { DeletedChatContext, ProofContext } from "./infoview/context";
 import { lastStepHasErrors } from "./infoview/goals";
 import { Button } from "./button";
 
-/** Plug-in the variable names in a hint. We do this client-side to prepare
- * for i18n in the future. i.e. one should be able translate the `rawText`
- * and have the variables substituted just before displaying.
- */
-function getHintText(hint: GameHint): string {
-  if (hint.rawText) {
-    // Replace the variable names used in the hint with the ones used by the player
-    // variable names are marked like `«{g}»` inside the text.
-    return hint.rawText.replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
-      // `hint.varNames` contains tuples `[oldName, newName]`
-      (hint.varNames.find(x => x[0] == v))[1]))
-  } else {
-    // hints created in the frontend do not have a `rawText`
-    // TODO: `hint.text` could be removed in theory.
-    return hint.text
-  }
-}
-
 export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
   return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
-    <Markdown>{getHintText(hint)}</Markdown>
+    <Markdown>{hint.text}</Markdown>
   </div>
 }
 
 export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
   return <div className={`message warning step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
-    <Markdown>{getHintText(hint)}</Markdown>
+    <Markdown>{hint.text}</Markdown>
   </div>
 }
 
@@ -49,7 +31,7 @@ export function Hints({hints, showHidden, step, selected, toggleSelection, lastL
 
 export function DeletedHint({hint} : {hint: GameHint}) {
   return <div className="message information deleted-hint">
-    <Markdown>{getHintText(hint)}</Markdown>
+    <Markdown>{hint.text}</Markdown>
   </div>
 }
 

client/src/components/infoview/goals.tsx

@@ -268,7 +268,7 @@ interface GoalsProps {
 
 export function Goals({ goals, filter }: GoalsProps) {
     if (goals.goals.length === 0) {
-        return <></>
+        return <>No goals</>
     } else {
         return <>
           {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}

client/src/components/infoview/main.tsx

@@ -232,11 +232,7 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
     ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
   } else {
     ret = <div className="infoview vscode-light">
-      {proof.completedWithWarnings &&
+      {proof.completed && <div className="level-completed">Level completed! 🎉</div>}
-        <div className="level-completed">
-          {proof.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"}
-        </div>
-      }
       <Infos />
       <Hints hints={proof.steps[curPos?.line]?.goals[0]?.hints}
         showHidden={showHelp.has(curPos?.line)} step={curPos?.line}

client/src/components/infoview/rpc_api.ts

@@ -49,8 +49,6 @@ export interface InteractiveTermGoal extends InteractiveGoalCore {
 export interface GameHint {
   text: string;
   hidden: boolean;
-  rawText: string;
-  varNames: string[][]; // in Lean: `Array (Name × Name)`
 }
 
 export interface InteractiveGoalWithHints {

client/src/css/infoview.css

@@ -41,13 +41,6 @@
 .level-completed {
   font-size: 1.8rem;
   font-weight: 500;
-  padding-left: .5em;
-  padding-right: .5em;
-  padding-top: .2em;
-  padding-bottom: .2em;
-  border-radius: .5em;
-  background-color: #eee;
-
 }
 
 .typewriter {

client/src/css/level.css

@@ -370,6 +370,6 @@ td code  {
 }
 
 /* DEBUG */
-/* .proof .step {
+.proof .step {
   border: 2px solid rgb(0, 123, 255);
-} */
+}

doc/troubleshoot.md

@@ -2,15 +2,6 @@
 
 Here are some issues experienced by users.
 
-- You can reset the lake projects involved (i.e. the `server/` folder here as well as your [game's folder](https://github.com/hhu-adam/GameSkeleton)) with the following commands:
-  ```
-  cd [THE PROJECT]
-  rm -rf .lake/
-  lake update -R
-  lake build
-  ```
-  If you experience problems related to Lean or lake, you should first try to reset it this way.
-
 # VSCode Dev-Container
 * If you don't get the pop-up, you might have disabled them, and you can reenable it by
   running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.

package-lock.json

@@ -8753,9 +8753,9 @@
       }
     },
     "node_modules/ip": {
-      "version": "1.1.9",
+      "version": "1.1.8",
-      "resolved": "https://registry.npmjs.org/ip/-/ip-1.1.9.tgz",
+      "resolved": "https://registry.npmjs.org/ip/-/ip-1.1.8.tgz",
-      "integrity": "sha512-cyRxvOEpNHNtchU3Ln9KC/auJgup87llfQpQ+t5ghoC/UhL16SWzbueiCsdTnWmqAWl7LadfuwhlqmtOaqMHdQ=="
+      "integrity": "sha512-PuExPYUiu6qMBQb4l06ecm6T6ujzhmh+MeJcW9wa89PoAz5pvd4zPgN5WJV104mb6S2T1AwNIAaB70JNrLQWhg=="
     },
     "node_modules/ip-anonymize": {
       "version": "0.1.0",
@@ -14341,14 +14341,6 @@
         "node": ">=6"
       }
     },
-    "node_modules/stacktrace-parser/node_modules/type-fest": {
-      "version": "0.7.1",
-      "resolved": "https://registry.npmjs.org/type-fest/-/type-fest-0.7.1.tgz",
-      "integrity": "sha512-Ne2YiiGN8bmrmJJEuTWTLJR32nh/JdL1+PSicowtNb0WFpn59GK8/lfD61bVtzguz7b3PBt74nxpv/Pw5po5Rg==",
-      "engines": {
-        "node": ">=8"
-      }
-    },
     "node_modules/statuses": {
       "version": "2.0.1",
       "resolved": "https://registry.npmjs.org/statuses/-/statuses-2.0.1.tgz",
@@ -14910,12 +14902,9 @@
       }
     },
     "node_modules/type-fest": {
-      "version": "4.10.3",
+      "version": "0.7.1",
-      "resolved": "https://registry.npmjs.org/type-fest/-/type-fest-4.10.3.tgz",
+      "resolved": "https://registry.npmjs.org/type-fest/-/type-fest-0.7.1.tgz",
-      "integrity": "sha512-JLXyjizi072smKGGcZiAJDCNweT8J+AuRxmPZ1aG7TERg4ijx9REl8CNhbr36RV4qXqL1gO1FF9HL8OkVmmrsA==",
+      "integrity": "sha512-Ne2YiiGN8bmrmJJEuTWTLJR32nh/JdL1+PSicowtNb0WFpn59GK8/lfD61bVtzguz7b3PBt74nxpv/Pw5po5Rg==",
-      "dev": true,
-      "optional": true,
-      "peer": true,
       "engines": {
         "node": ">=8"
       }

server/GameServer/Commands.lean

@@ -2,8 +2,6 @@ import GameServer.Helpers
 import GameServer.Inventory
 import GameServer.Options
 import GameServer.SaveData
-import GameServer.Hints
-import I18n
 
 open Lean Meta Elab Command
 
@@ -34,17 +32,16 @@ elab "Level" level:num : command => do
 
 /-- Define the title of the current game/world/level. -/
 elab "Title" t:str : command => do
-  let title ← t.getString.translate
   match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with title := title}
+  | .Level => modifyCurLevel fun level => pure {level with title := t.getString}
-  | .World => modifyCurWorld  fun world => pure {world with title := title}
+  | .World => modifyCurWorld  fun world => pure {world with title := t.getString}
   | .Game => modifyCurGame  fun game => pure {game with
       title := t.getString
-      tile := {game.tile with title := title}}
+      tile := {game.tile with title := t.getString}}
 
 /-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
-  let intro ← t.getString.translate
+  let intro := t.getString
   match ← getCurLayer with
   | .Level => modifyCurLevel fun level => pure {level with introduction := intro}
   | .World => modifyCurWorld  fun world => pure {world with introduction := intro}
@@ -52,7 +49,7 @@ elab "Introduction" t:str : command => do
 
 /-- Define the info of the current game. Used for e.g. credits -/
 elab "Info" t:str : command => do
-  let info ← t.getString.translate
+  let info:= t.getString
   match ← getCurLayer with
   | .Level =>
     logError "Can't use `Info` in a level!"
@@ -84,7 +81,7 @@ elab "Image" t:str : command => do
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
 elab "Conclusion" t:str : command => do
-  let conclusion ← t.getString.translate
+  let conclusion := t.getString
   match ← getCurLayer with
   | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion}
   | .World => modifyCurWorld  fun world => pure {world with conclusion := conclusion}
@@ -97,13 +94,13 @@ elab "Prerequisites" t:str* : command => do
 
 /-- Short caption for the game (1 sentence) -/
 elab "CaptionShort" t:str : command => do
-  let caption ← t.getString.translate
+  let caption := t.getString
   modifyCurGame fun game => pure {game with
     tile := {game.tile with short := caption}}
 
 /-- More detailed description what the game is about (2-4 sentences). -/
 elab "CaptionLong" t:str : command => do
-  let caption ← t.getString.translate
+  let caption := t.getString
   modifyCurGame fun game => pure {game with
     tile := {game.tile with long := caption}}
 
@@ -144,7 +141,6 @@ TacticDoc rw "`rw` stands for rewrite, etc. "
  -/
 elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do
   let doc ← parseDocCommentLegacy doc content
-  let doc ← doc.translate
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Tactic
     name := name.getId
@@ -169,7 +165,6 @@ The theorem/definition to have the same fully qualified name as in mathlib.
 elab doc:docComment ? "TheoremDoc" name:ident "as" displayName:str "in" category:str content:str ? :
     command => do
   let doc ← parseDocCommentLegacy doc content
-  let doc ← doc.translate
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Lemma
     name := name.getId
@@ -199,7 +194,6 @@ The theorem/definition to have the same fully qualified name as in mathlib.
  -/
 elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:str ? : command => do
   let doc ← parseDocCommentLegacy doc template
-  let doc ← doc.translate
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Definition
     name := name.getId,
@@ -346,9 +340,6 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
   let lvlIdx ← getCurLevelIdx
 
   let docContent ← parseDocComment doc
-  let docContent ← match docContent with
-  | none => pure none
-  | some d => d.translate
 
   -- Save the messages before evaluation of the proof.
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
@@ -405,41 +396,12 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
         .nest hidden $
         .compose (.ofGoal text) (.ofGoal goal) := msg.data then
       let hint ← liftTermElabM $ withMCtx ctx.mctx $ withLCtx ctx.lctx #[] $ withEnv ctx.env do
-
-        let goalDecl ← goal.getDecl
-        let fvars := goalDecl.lctx.decls.toArray.filterMap id |> Array.map (·.fvarId)
-
-        -- NOTE: This code about `hintFVarsNames` is duplicated from `RpcHandlers`
-        -- where the variable bijection is constructed, and they
-        -- need to be matching.
-        -- NOTE: This is a bit a hack of somebody who does not know how meta-programming works.
-        -- All we want here is a list of `userNames` for the `FVarId`s in `hintFVars`...
-        -- and we wrap them in `«{}»` here since I don't know how to do it later.
-        let mut hintFVarsNames : Array Expr := #[]
-        for fvar in fvars do
-          let name₁ ← fvar.getUserName
-          hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩
-
-        let text ← instantiateMVars (mkMVar text)
-
-        -- Evaluate the text in the `Hint`'s context to get the old variable names.
-        let rawText := (← GameServer.evalHintMessage text) hintFVarsNames
-        let ctx₂ := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
-        let rawText : String ← (MessageData.withContext ctx₂ rawText).toString
-
         return {
           goal := ← abstractCtx goal
-          text := text
+          text := ← instantiateMVars (mkMVar text)
-          rawText := rawText
           strict := strict == 1
           hidden := hidden == 1
         }
-
-      -- Note: The current setup for hints is a bit convoluted, but for now we need to
-      -- send the text once through i18n to register it in the env extension.
-      -- This could probably be rewritten once i18n works fully.
-      let _ ← hint.rawText.translate
-
       hints := hints.push hint
     else
       nonHintMsgs := nonHintMsgs.push msg
@@ -478,8 +440,6 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
 
 /-! # Hints -/
 
-open GameServer in
-
 /-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
 see hints. The tactic does not affect the goal state.
 -/

server/GameServer/EnvExtensions.lean

@@ -1,13 +1,7 @@
 import GameServer.AbstractCtx
 import GameServer.Graph
-import GameServer.Hints
 
-open GameServer
 
--- TODO: Is there a better place?
-/-- Keywords that the server should not consider as tactics. -/
-def GameServer.ALLOWED_KEYWORDS : List String :=
-  ["with", "fun", "at", "only", "by", "generalizing"]
 
 /-- The default game name if `Game "MyGame"` is not used. -/
 def defaultGameName: String := "MyGame"
@@ -24,6 +18,22 @@ defined in this file.
 
 open Lean
 
+/-! ## Hints -/
+
+/-- A hint to help the user with a specific goal state -/
+structure GoalHintEntry where
+  goal : AbstractCtxResult
+  /-- Text of the hint as an expression of type `Array Expr → MessageData` -/
+  text : Expr
+  /-- If true, then hint should be hidden and only be shown on player's request -/
+  hidden : Bool := false
+  /-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
+  strict : Bool := false
+
+instance : Repr GoalHintEntry := {
+  reprPrec := fun a n => reprPrec a.text n
+}
+
 /-! ## Inventory (documentation)
 
 The inventory contains documentation that the user can access.

server/GameServer/FileWorker.lean

@@ -122,7 +122,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState :
     -- Atoms might be tactic names or other keywords.
     -- Note: We whitelisted known keywords because we cannot
     -- distinguish keywords from tactic names.
-    let allowed := GameServer.ALLOWED_KEYWORDS
+    let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"]
     -- Ignore syntax elements that do not start with a letter or are listed above.
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       -- Treat `simp?` and `simp!` like `simp`
@@ -169,20 +169,15 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState :
       match theoremsAndDefs.find? (·.name == n) with
       | none =>
         -- Theorem will never be introduced in this game
-        addMessageByDifficulty info s!"The theorem/definition '{n}' is not available in this game!"
+        addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
       | some thm =>
         -- Theorem is introduced at some point in the game.
         if thm.disabled then
           -- Theorem is disabled in this level.
           addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
         else if thm.locked then
-          match workerState.inventory.find? (· == n.toString) with
+          -- Theorem is still locked.
-          | none =>
+          addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
-            -- Theorem is still locked.
-            addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
-          | some _ =>
-            -- Theorem is in the inventory, allow it.
-            pure ()
 
 where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
   -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
@@ -391,60 +386,60 @@ def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.Ini
 
   hOut.writeLspNotification { method := "$/game/publishProofState", param }
 
-/-- Checks whether game level has been completed and sends a notification to the client -/
+  /-- Checks whether game level has been completed and sends a notification to the client -/
-def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
+  def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
-  -- check if there is any error or warning
+    -- check if there is any error or warning
-  for snap in snaps do
+    for snap in snaps do
-    if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning
+      if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning
-    then return
+      then return
-  let param := { uri := m.uri : GameCompletedParams}
+    let param := { uri := m.uri : GameCompletedParams}
-  hOut.writeLspNotification { method := "$/game/completed", param }
+    hOut.writeLspNotification { method := "$/game/completed", param }
 
-/-- copied from `Lean.Server.FileWorker.nextCmdSnap`. -/
+  /-- copied from `Lean.Server.FileWorker.nextCmdSnap`. -/
--- @[inherit_doc Lean.Server.FileWorker.nextCmdSnap] -- cannot inherit from private
+  -- @[inherit_doc Lean.Server.FileWorker.nextCmdSnap] -- cannot inherit from private
-private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
+  private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-    (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) :
+      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) :
-    AsyncElabM (Option Snapshot) := do
+      AsyncElabM (Option Snapshot) := do
-  cancelTk.check
+    cancelTk.check
-  let s ← get
+    let s ← get
-  let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
+    let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
-  if lastSnap.isAtEnd then
+    if lastSnap.isAtEnd then
-    publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
+      publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
-    publishProgressDone m ctx.hOut
+      publishProgressDone m ctx.hOut
-    publishIleanInfoFinal m ctx.hOut s.snaps
+      publishIleanInfoFinal m ctx.hOut s.snaps
-    return none
+      return none
-  publishProgressAtPos m lastSnap.endPos ctx.hOut
+    publishProgressAtPos m lastSnap.endPos ctx.hOut
 
-  -- (modified part)
+    -- (modified part)
-  -- Make sure that there is at least one snap after the head snap, so that
+    -- Make sure that there is at least one snap after the head snap, so that
-  -- we can see the current goal even on an empty document
+    -- we can see the current goal even on an empty document
-  let couldBeEndSnap := s.snaps.size > 1
+    let couldBeEndSnap := s.snaps.size > 1
-  let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
+    let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
-    gameWorkerState initParams
+      gameWorkerState initParams
 
-  set { s with snaps := s.snaps.push snap }
+    set { s with snaps := s.snaps.push snap }
-  cancelTk.check
+    cancelTk.check
-  publishProofState m snap initParams ctx.hOut
+    publishProofState m snap initParams ctx.hOut
-  publishDiagnostics m snap.diagnostics.toArray ctx.hOut
+    publishDiagnostics m snap.diagnostics.toArray ctx.hOut
-  publishIleanInfoUpdate m ctx.hOut #[snap]
+    publishIleanInfoUpdate m ctx.hOut #[snap]
-  return some snap
+    return some snap
 
--- Copied from `Lean.Server.FileWorker.unfoldCmdSnaps` using our own `nextCmdSnap`.
+  -- Copied from `Lean.Server.FileWorker.unfoldCmdSnaps` using our own `nextCmdSnap`.
-@[inherit_doc Lean.Server.FileWorker.unfoldCmdSnaps]
+  @[inherit_doc Lean.Server.FileWorker.unfoldCmdSnaps]
-def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
+  def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
-    (startAfterMs : UInt32) (gameWorkerState : WorkerState)
+      (startAfterMs : UInt32) (gameWorkerState : WorkerState)
-    : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
+      : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
-  let ctx ← read
+    let ctx ← read
-  let some headerSnap := snaps[0]? | panic! "empty snapshots"
+    let some headerSnap := snaps[0]? | panic! "empty snapshots"
-  if headerSnap.msgLog.hasErrors then
+    if headerSnap.msgLog.hasErrors then
-    publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
+      publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
-    publishIleanInfoFinal m ctx.hOut #[headerSnap]
+      publishIleanInfoFinal m ctx.hOut #[headerSnap]
-    return AsyncList.ofList [headerSnap]
+      return AsyncList.ofList [headerSnap]
-  else
+    else
-    publishIleanInfoUpdate m ctx.hOut snaps
+      publishIleanInfoUpdate m ctx.hOut snaps
-    return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
+      return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
-      IO.sleep startAfterMs
+        IO.sleep startAfterMs
-      AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
+        AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
 
 end Elab
 

server/GameServer/Helpers.lean

@@ -4,6 +4,8 @@ import Lean
 
 open Lean Meta Elab Command
 
+syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
+
 /-! ## Doc Comment Parsing -/
 
 /-- Read a doc comment and get its content. Return `""` if no doc comment available. -/
@@ -83,6 +85,23 @@ def getStatementString (name : Name) : CommandElabM String := do
 syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
 -- TODO
 
+
+/-- Remove any spaces at the beginning of a new line -/
+partial def removeIndentation (s : String) : String :=
+  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
+    let c := s.get i
+    let i := s.next i
+    if s.atEnd i then
+      acc.push c
+    else if removeSpaces && c == ' ' then
+      loop i acc (removeSpaces := true)
+    else if c == '\n' then
+      loop i (acc.push c) (removeSpaces := true)
+    else
+      loop i (acc.push c)
+  loop ⟨0⟩ ""
+
+
 /-! ## Loops in Graph-like construct
 
 TODO: Why are we not using graphs here but our own construct `HashMap Name (HashSet Name)`?

server/GameServer/Hints.lean

@@ -1,54 +0,0 @@
-import GameServer.AbstractCtx
-
-/-!
-This file contains anything related to the `Hint` tactic used to add hints to a game level.
--/
-
-open Lean Meta Elab
-
-namespace GameServer
-
-syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
-
-/-- A hint to help the user with a specific goal state -/
-structure GoalHintEntry where
-  goal : AbstractCtxResult
-  /-- Text of the hint as an expression of type `Array Expr → MessageData` -/
-  text : Expr
-  rawText : String
-  /-- If true, then hint should be hidden and only be shown on player's request -/
-  hidden : Bool := false
-  /-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
-  strict : Bool := false
-
-instance : Repr GoalHintEntry := {
-  reprPrec := fun a n => reprPrec a.text n
-}
-
-/-- For a hint `(hint : GoalHintEntry)` one uses `(← evalHintMessage hint.text) x`
- where `(x : Array Expr)` contains the names of all the variables that should be inserted
- in the text.
-
- TODO: explain better. -/
-unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
-  evalExpr (Array Expr → MessageData)
-    (.forallE default (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr))
-      (mkConst ``MessageData) .default)
-
-@[implemented_by evalHintMessageUnsafe]
-def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pure (fun _ => "")
-
-/-- Remove any spaces at the beginning of a new line -/
-partial def removeIndentation (s : String) : String :=
-  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
-    let c := s.get i
-    let i := s.next i
-    if s.atEnd i then
-      acc.push c
-    else if removeSpaces && c == ' ' then
-      loop i acc (removeSpaces := true)
-    else if c == '\n' then
-      loop i (acc.push c) (removeSpaces := true)
-    else
-      loop i (acc.push c)
-  loop ⟨0⟩ ""

server/GameServer/Inventory.lean

@@ -121,7 +121,7 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co
   | .atom _info val =>
     -- ignore syntax elements that do not start with a letter
     -- and ignore some standard keywords
-    let allowed := GameServer.ALLOWED_KEYWORDS
+    let allowed := ["with", "fun", "at", "only", "by"]
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
       return {acc with tactics := acc.tactics.insert val}

server/GameServer/RpcHandlers.lean

@@ -1,7 +1,6 @@
 import GameServer.EnvExtensions
 import GameServer.InteractiveGoal
 import Std.Data.Array.Init.Basic
-import GameServer.Hints
 
 open Lean
 open Server
@@ -104,6 +103,14 @@ def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (in
   then return some bij
   else return none
 
+unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
+  evalExpr (Array Expr → MessageData)
+    (.forallE default (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr))
+      (mkConst ``MessageData) .default)
+
+@[implemented_by evalHintMessageUnsafe]
+def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pure (fun _ => "")
+
 open Meta in
 /-- Find all hints whose trigger matches the current goal -/
 def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
@@ -114,42 +121,14 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
       openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
         if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
         then
-
+          let lctx := (← goal.getDecl).lctx
-          -- NOTE: This code for `hintFVarsNames` is also duplicated in the
+          if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
-          -- "Statement" command, where `hint.rawText` is created. They need to be matching.
-          -- NOTE: This is a bit a hack of somebody who does not know how meta-programming works.
-          -- All we want here is a list of `userNames` for the `FVarId`s in `hintFVars`...
-          -- and we wrap them in `«{}»` here since I don't know how to do it later.
-          let mut hintFVarsNames : Array Expr := #[]
-          for fvar in hintFVars do
-            let name₁ ← fvar.fvarId!.getUserName
-            hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩
-
-          let lctx := (← goal.getDecl).lctx -- the player's local context
-          if let some bij ← matchDecls hintFVars lctx.getFVars
-            (strict := hint.strict) (initBij := fvarBij)
           then
             let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
-            -- Evaluate the text in the player's context to get the new variable names.
             let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
             let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := lctx, opts := {}}
             let text ← (MessageData.withContext ctx text).toString
-
+            return some { text := text, hidden := hint.hidden }
-            -- Here we map the goal's variable names to the player's variable names.
-            let mut varNames : Array <| Name × Name := #[]
-            for (fvar₁, fvar₂) in bij.forward.toArray do
-              -- get the `userName` of the fvar in the opened local context of the hint.
-              let name₁ ← fvar₁.getUserName
-              -- get the `userName` in the player's local context.
-              let name₂ := (lctx.get! fvar₂).userName
-              varNames := varNames.push (name₁, name₂)
-
-            return some {
-              text := text,
-              hidden := hint.hidden,
-              rawText := hint.rawText,
-              varNames := varNames }
-
           else return none
         else
           return none

server/GameServer/SaveData.lean

@@ -1,8 +1,8 @@
 import GameServer.EnvExtensions
-import I18n
 
 open Lean Meta Elab Command
 
+
 /-! ## Copy images -/
 
 open IO.FS System FilePath in
@@ -59,9 +59,6 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
 
   IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
 
-  -- write PO file for translation
-  I18n.createPOTemplate
-
 open GameData
 
 def loadData (f : System.FilePath) (α : Type) [FromJson α] : IO α := do

server/GameServer/Structures.lean

@@ -54,17 +54,8 @@ deriving RpcEncodable
 
 /-- A hint in the game at the corresponding goal. -/
 structure GameHint where
-  /-- The text with the variable names already inserted.
-
-  Note: This is in theory superfluous and will be completely replaced by `rawText`. We just left
-  it in for debugging for now. -/
   text : String
-  /-- Flag whether the hint should be hidden initially. -/
   hidden : Bool
-  /-- The text with the variables not inserted yet. -/
-  rawText : String
-  /-- The assignment of variable names in the `rawText` to the ones the player used. -/
-  varNames : Array <| Name × Name
 deriving FromJson, ToJson
 
 /-- Bundled `InteractiveGoal` together with an array of hints that apply at this stage. -/

server/lake-manifest.json

@@ -4,19 +4,10 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
+   "rev": "276953b13323ca151939eafaaec9129bf7970306",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "v4.6.0-rc1",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hhu-adam/lean-i18n.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "c5b84feffb28dbd5b1ac74b3bf63271296fabfa5",
-   "name": "i18n",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",

server/lakefile.lean

@@ -7,7 +7,8 @@ package GameServer
 def leanVersion : String := s!"v{Lean.versionString}"
 
 require std from git "https://github.com/leanprover/std4.git" @ leanVersion
-require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion
+
+-- require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
 
 lean_lib GameServer
 

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.0
+leanprover/lean4:v4.6.0-rc1

tsconfig.json

@@ -11,9 +11,6 @@
     "downlevelIteration": true,
     "experimentalDecorators": true,
     "allowSyntheticDefaultImports": true,
-    "lib": [
-      "ES2021.String"
-    ]
   },
   "exclude": ["server", "relay"]
 }