First big junk of communication refactor

server/GameServer/FileWorker.lean

@@ -3,6 +3,7 @@ import Lean.Server.FileWorker
 import GameServer.Game
 import GameServer.ImportModules
 import GameServer.SaveData
+import GameServer.EnvExtensions
 
 namespace MyModule
 
@@ -60,8 +61,8 @@ open Snapshots
 open JsonRpc
 
 /--
-Game-specific state to be packed on top of the `Lean.Server.FileWorker.WorkerState`
-used by the lean server.
+Game-specific state to be packed on top of the `Server.FileWorker.WorkerState`
+used by the Lean server.
 -/
 structure WorkerState :=
   /--
@@ -84,7 +85,7 @@ structure WorkerState :=
 deriving ToJson, FromJson
 
 /--
-Pack the `GameServer.FileWorker.WorkerState` on top of the normal worker monad
+Pack the our custom `WorkerState` on top of the normal worker monad
 `Server.FileWorker.WorkerM`.
 -/
 abbrev WorkerM := StateT WorkerState Server.FileWorker.WorkerM
@@ -102,16 +103,6 @@ def addMessage (info : SourceInfo) (inputCtx : Parser.InputContext)
       pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
       data     := s }}
 
-/-- Deprecated! -/
-def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
-    Elab.Command.CommandElabM Unit := do
-  modify fun st => { st with
-    messages := st.messages.add {
-      fileName := inputCtx.fileName
-      severity := MessageSeverity.error
-      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
-      data     := s }}
-
 -- TODO: use HashSet for allowed tactics?
 /--
 Find all tactics in syntax object that are forbidden according to a
@@ -322,6 +313,79 @@ where
     uri : String
   deriving ToJson, FromJson
 
+structure GameDiagnostics where
+  diagnostics : List Diagnostic
+deriving ToJson, FromJson
+
+structure GameParams where
+  uri : String
+  diagnostics : GameDiagnostics
+deriving ToJson, FromJson
+
+/-- WIP: publish diagnostics, all intermediate goals and if the game is completed. -/
+def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.InitializeParams) (hOut : FS.Stream) :
+    IO Unit := do
+  -- let text := m.text
+
+  -- -- `snap` is the one snapshot containing the entire proof.
+  -- let mut goals : Array <| InteractiveGoalsWithHints := #[]
+  -- for pos in text.positions do
+  --   let source := text.getLineBefore pos
+  --   -- iterate over all newlines in the proof and get the goals and hints at each position
+  --   if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? text pos then
+  --     pure ()
+  --     let goalAtPos : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
+  --       fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
+  --         -- TODO: What does this function body do?
+  --         -- let ciAfter := { ci with mctx := ti.mctxAfter }
+  --         let ci := if useAfter then
+  --             { ci with mctx := tacticInfo.mctxAfter }
+  --           else
+  --             { ci with mctx := tacticInfo.mctxBefore }
+  --         -- compute the interactive goals
+  --         let goalMvars : List MVarId ← ci.runMetaM {} do
+  --           return if useAfter then tacticInfo.goalsAfter else tacticInfo.goalsBefore
+
+  --         let interactiveGoals : List InteractiveGoalWithHints ← ci.runMetaM {} do
+  --           goalMvars.mapM fun goal => do
+  --             let hints ← findHints goal m initParams
+  --             let interactiveGoal ← goalToInteractive goal
+  --             return ⟨interactiveGoal, hints⟩
+  --         -- TODO: This code is way old, can it be deleted?
+  --         -- compute the goal diff
+  --         -- let goals ← ciAfter.runMetaM {} (do
+  --         --     try
+  --         --       Widget.diffInteractiveGoals useAfter ti goals
+  --         --     catch _ =>
+  --         --       -- fail silently, since this is just a bonus feature
+  --         --       return goals
+  --         -- )
+  --         return interactiveGoals
+  --     let goalAtPos : Array InteractiveGoalWithHints := ⟨goalAtPos.foldl (· ++ ·) []⟩
+  --     goals := goals.push ⟨goalAtPos, source⟩
+  --   else
+  --     -- No goals present
+  --     goals := goals.push default
+
+  -- -- Question: Is there a difference between the diags of this snap and the last snap?
+  -- -- Should we get the diags from there?
+  -- let diag : Array Widget.InteractiveDiagnostic := snap.interactiveDiags.toArray
+
+  -- -- Level is completed if there are no errrors or warnings
+  -- let completed : Bool := ¬ diag.any (fun d =>
+  --   d.severity? == some .error ∨ d.severity? == some .warning)
+
+  -- let param : ProofState := {
+  --   steps := goals,
+  --   diagnostics := diag,
+  --   completed := completed }
+
+  -- TODO
+  let param := { uri := m.uri : GameCompletedParams}
+
+
+  hOut.writeLspNotification { method := "$/game/publishProofState", param }
+
   /-- 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
     -- check if there is any error or warning
@@ -331,65 +395,51 @@ where
     let param := { uri := m.uri : GameCompletedParams}
     hOut.writeLspNotification { method := "$/game/completed", param }
 
-  /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
-  private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams)
-      : AsyncElabM (Option Snapshot) := do
+  /-- copied from `Lean.Server.FileWorker.nextCmdSnap`. -/
+  -- @[inherit_doc Lean.Server.FileWorker.nextCmdSnap] -- cannot inherit from private
+  private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
+      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) :
+      AsyncElabM (Option Snapshot) := do
     cancelTk.check
     let s ← get
     let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
     if lastSnap.isAtEnd then
-      publishGameCompleted m ctx.hOut s.snaps
       publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
       publishProgressDone m ctx.hOut
-      -- This will overwrite existing ilean info for the file, in case something
-      -- went wrong during the incremental updates.
       publishIleanInfoFinal m ctx.hOut s.snaps
       return none
     publishProgressAtPos m lastSnap.endPos ctx.hOut
+
+    -- (modified part)
     -- 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
     let couldBeEndSnap := s.snaps.size > 1
     let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
       gameWorkerState initParams
+
     set { s with snaps := s.snaps.push snap }
-    -- TODO(MH): check for interrupt with increased precision
     cancelTk.check
-    /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
-      while preferring newer versions over old ones. The former is necessary because we do
-      not explicitly clear older diagnostics, while the latter is necessary because we do
-      not guarantee that diagnostics are emitted in order. Specifically, it may happen that
-      we interrupted this elaboration task right at this point and a newer elaboration task
-      emits diagnostics, after which we emit old diagnostics because we did not yet detect
-      the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
-      because we cannot guarantee that no further diagnostics are emitted after clearing
-      them. -/
-    -- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
-    -- because empty diagnostics clear existing error/information squiggles. Therefore we always
-    -- want to publish in case there was previously a message at this position.
+    publishProofState m snap initParams ctx.hOut
     publishDiagnostics m snap.diagnostics.toArray ctx.hOut
     publishIleanInfoUpdate m ctx.hOut #[snap]
     return some snap
 
-  /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
-  def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
+  -- Copied from `Lean.Server.FileWorker.unfoldCmdSnaps` using our own `nextCmdSnap`.
+  @[inherit_doc Lean.Server.FileWorker.unfoldCmdSnaps]
+  def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
       (startAfterMs : UInt32) (gameWorkerState : WorkerState)
       : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
     let ctx ← read
     let some headerSnap := snaps[0]? | panic! "empty snapshots"
     if headerSnap.msgLog.hasErrors then
-      -- Treat header processing errors as fatal so users aren't swamped with
-      -- followup errors
       publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
       publishIleanInfoFinal m ctx.hOut #[headerSnap]
       return AsyncList.ofList [headerSnap]
     else
-      -- This will overwrite existing ilean info for the file since this has a
-      -- higher version number.
       publishIleanInfoUpdate m ctx.hOut snaps
       return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
         IO.sleep startAfterMs
-        AsyncList.unfoldAsync (nextSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
+        AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
 
 end Elab
 
@@ -439,7 +489,7 @@ def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
         validSnaps := validSnaps.dropLast
     -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
     -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
-    unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx
+    unfoldCmdSnaps newMeta validSnaps.toArray cancelTk s ctx
       (startAfterMs := ctx.initParams.editDelay.toUInt32)
   StateT.lift <| modify fun st => { st with
     doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
@@ -513,49 +563,52 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     publishDiagnostics m headerSnap.diagnostics.toArray hOut
     return (headerSnap, srcSearchPath)
 
+/-- Copied from `Lean.Server.FileWorker.initializeWorker`. Added `gameDir` and
+`gameWorkerState` arguments and use custom `unfoldCmdSnaps`. -/
+-- @[inherit_doc Lean.Server.FileWorker.initializeWorker]
 def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
     (gameDir : String) (gameWorkerState : WorkerState) : IO (WorkerContext × Server.FileWorker.WorkerState) := do
   let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
-
   let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-    gameDir gameWorkerState.levelInfo.module
+    (gameDir := gameDir) (module := gameWorkerState.levelInfo.module)
   let cancelTk ← CancelToken.new
-  let ctx :=
-    { hIn  := i
-      hOut := o
-      hLog := e
-      headerTask
-      initParams
-      clientHasWidgets
-    }
+  let ctx := {
+    hIn  := i
+    hOut := o
+    hLog := e
+    headerTask
+    initParams
+    clientHasWidgets
+  }
   let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-    | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
+    | Except.ok (s, _) => unfoldCmdSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
     | Except.error e   => throw (e : ElabTaskError))
   let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
-  return (ctx,
-  { doc             := doc
-    initHeaderStx   := headerStx
+  return (ctx, {
+    doc                := doc
+    initHeaderStx      := headerStx
     currHeaderStx      := headerStx
     importCachingTask? := none
-    pendingRequests := RBMap.empty
-    rpcSessions     := RBMap.empty
+    pendingRequests    := RBMap.empty
+    rpcSessions        := RBMap.empty
   })
 
 end Initialization
 
 section NotificationHandling
 
+/-- Copied from `Lean.Server.FileWorker.handleDidChange` but with our custom `WorkerM` and
+`updateDocument` -/
+-- @[inherit_doc Lean.Server.FileWorker.handleDidChange]
 def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do
   let docId := p.textDocument
   let changes := p.contentChanges
-  let oldDoc := (← StateT.lift get).doc
-  let some newVersion ← pure docId.version?
-    | throwServerError "Expected version number"
-  if newVersion ≤ oldDoc.meta.version then
-    -- TODO(WN): This happens on restart sometimes.
-    IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
-  else if ¬ changes.isEmpty then
+  let oldDoc := (← StateT.lift get).doc -- needed a lift to our custom `WorkerM`
+  let newVersion := docId.version?.getD 0
+  if ¬ changes.isEmpty then
     let newDocText := foldDocumentChanges changes oldDoc.meta.text
+    -- modification: set the `DependencyBuildMode` from
+    -- `oldDoc.meta.dependencyBuildMode` to `.always`
     updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
 
 end NotificationHandling
@@ -591,39 +644,34 @@ end MessageHandling
 section MainLoop
 
 /--
-Erase finished tasks if there are no errors.
--/
-private def filterFinishedTasks (acc : PendingRequestMap) (id : RequestID)
-    (task : Task (Except IO.Error Unit)) : IO PendingRequestMap := do
-  if (← hasFinished task) then
-    /- Handler tasks are constructed so that the only possible errors here
-    are failures of writing a response into the stream. -/
-    if let Except.error e := task.get then
-      throwServerError s!"Failed responding to request {id}: {e}"
-    pure <| acc.erase id
-  else pure acc
-
-/--
-The main-loop.
+The main-loop. Copied from `Lean.Server.FileWorker.mainLoop`. Use custom `WorkerM` as well
+as custom `handleNotification`.
 -/
+--@[inherit_doc Lean.Server.FileWorker.mainLoop]
 partial def mainLoop : WorkerM Unit := do
   let ctx ← read
   let mut st ← StateT.lift get
   let msg ← ctx.hIn.readLspMessage
-  let pendingRequests ← st.pendingRequests.foldM (fun acc id task =>
-    filterFinishedTasks acc id task) st.pendingRequests
+  -- Erase finished tasks if there are no errors.
+  let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
+      : IO PendingRequestMap := do
+    if (← hasFinished task) then
+      if let Except.error e := task.get then
+        throwServerError s!"Failed responding to request {id}: {e}"
+      pure <| acc.erase id
+    else pure acc
+  let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
   st := { st with pendingRequests }
-  -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired.
   for (id, seshRef) in st.rpcSessions do
     let sesh ← seshRef.get
     if (← sesh.hasExpired) then
       st := { st with rpcSessions := st.rpcSessions.erase id }
 
   set st
-
   -- Process the RPC-message and restart main-loop.
   match msg with
   | Message.request id "shutdown" none =>
+    --added. TODO: why do we need that? Or has it just removed in Lean since when we started?
     ctx.hOut.writeLspResponse ⟨id, Json.null⟩
     mainLoop
   | Message.request id method (some params) =>
@@ -633,6 +681,7 @@ partial def mainLoop : WorkerM Unit := do
   | Message.notification "exit" none =>
     let doc := st.doc
     doc.cancelTk.set
+    doc.cmdSnaps.cancel
     return ()
   | Message.notification method (some params) =>
     -- Custom notification handler
@@ -643,10 +692,15 @@ partial def mainLoop : WorkerM Unit := do
 
 end MainLoop
 
-
+/-- Modified from `Lean.Server.FileWorker.initAndRunWorker`.
+Added `gameDir` argument, -/
+-- @[inherit_doc Lean.Server.FileWorker.initAndRunWorker]
 def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
+
+
+  -- BIG MODIFICATION
   let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
   o.writeLspResponse {
     id     := initRequest.id
@@ -662,16 +716,16 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
   discard $ i.readLspNotificationAs "initialized" InitializedParams
   let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
 
+
   let doc := param.textDocument
-  /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
-    "\n", which should be enough to handle both LF and CRLF correctly.
-    This is because LSP always refers to characters by (line, column),
-    so if we get the line number correct it shouldn't matter that there
-    is a CR there. -/
+  -- modification: using `.always`
   let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
+
+
+    -- BIG MODIFICATION
     let game ← loadGameData gameDir
     -- TODO: We misuse the `rootUri` field to the gameName
     let rootUri? : Option String := some (toString game.name)
@@ -691,6 +745,8 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
     -- Run the main loop
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
       StateT.run (s := gameWorkerState) <| (mainLoop)
+
+
     return (0 : UInt32)
   catch e =>
     IO.eprintln e
@@ -703,8 +759,12 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
 /--
 The main function. Simply wrapping `initAndRunWorker`.
 
+Copied from `Lean.Server.FileWorker.workerMain`. We add `args` as an argument to pass on
+the `gameDir`.
+
 TODO: The first arg `args[0]` is always expected to be `--server`. We could drop this completely.
 -/
+-- @[inherit_doc Lean.Server.FileWorker.workerMain]
 def workerMain (opts : Options) (args : List String): IO UInt32 := do
   let i ← IO.getStdin
   let o ← IO.getStdout
@@ -712,9 +772,6 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do
   try
     let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
     let exitCode ← initAndRunWorker i o e opts gameDir
-    -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit,
-    -- but we definitely don't want to do that in the case of the worker processes,
-    -- which can produce non-terminating tasks evaluating user code.
     o.flush
     e.flush
     IO.Process.exit exitCode.toUInt8

server/GameServer/InteractiveGoal.lean

@@ -1,62 +1,19 @@
-import Lean.Widget.InteractiveGoal
+import GameServer.Structures
 
 /-!
 This file is a modified copy of `Lean.Widget.InteractiveGoal`.
 
-We add the structure `GameHint` and extend two existing structures:
-
-* `isAssumption?` in `InteractiveHypothesisBundle`: stores if a hypothesis is of type `Prop`.
-* `hint` in `InteractiveGoal`: stores the game hints associated with the goal.
-
-The rest of this file is simply copied to use these new modified stuctures.
+Note that the structures have been moved to `Structures.lean`, but most of the
+functions here must be duplicated from `Lean.Widget.InteractiveGoal` in order
+to use the duplicated structures.
 -/
 
 namespace GameServer
 
 open Lean Lean.Widget Lean.Server
 
-/-- A hint in the game at the corresponding goal. -/
-structure GameHint where
-  text : String
-  hidden : Bool
-deriving FromJson, ToJson
-
-/-- Extend the interactive hypothesis bundle with an option to distinguish
-"assumptions" from "objects". "Assumptions" ate hyptheses of type `Prop`. -/
--- @[inherit_doc Lean.Widget.InteractiveHypothesisBundle]
-structure InteractiveHypothesisBundle extends Lean.Widget.InteractiveHypothesisBundle where
-  /-- The hypothesis's type is of type `Prop` -/
-  isAssumption? : Option Bool := none
-deriving RpcEncodable
-
--- duplicated but with custom `InteractiveHypothesisBundle`
-@[inherit_doc Lean.Widget.InteractiveGoalCore]
-structure InteractiveGoalCore where
-  hyps : Array InteractiveHypothesisBundle
-  type : CodeWithInfos
-  ctx : WithRpcRef Elab.ContextInfo
-
--- duplicated but with custom `InteractiveGoalCore` and extended by `hints`
-@[inherit_doc Lean.Widget.InteractiveGoal]
-structure InteractiveGoal extends InteractiveGoalCore where
-  userName? : Option String
-  goalPrefix : String
-  mvarId : MVarId
-  isInserted? : Option Bool := none
-  isRemoved? : Option Bool := none
-  /-- Extended the `InteractiveGoal` by an array of hints at that goal. -/
-  hints : Array GameHint := #[]
-deriving RpcEncodable
-
 -- duplicated with custom `InteractiveGoalCore`
-@[inherit_doc Lean.Widget.InteractiveTermGoal]
-structure InteractiveTermGoal extends InteractiveGoalCore where
-  range : Lsp.Range
-  term : WithRpcRef Elab.TermInfo
-deriving RpcEncodable
-
--- duplicated with custom `InteractiveGoalCore`
-@[inherit_doc Lean.Widget.InteractiveGoalCore.pretty]
+-- @[inherit_doc Lean.Widget.InteractiveGoalCore.pretty]
 def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String)
     (goalPrefix : String) : Format := Id.run do
   let indent := 2 -- Use option
@@ -140,10 +97,9 @@ def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α)
 
 open Meta in
 
--- Copied from `Lean.Widget.goalToInteractive` but added
--- argument `hint` which is simply passed along.
+-- Duplicated from `Lean.Widget.goalToInteractive` with custom structures
 @[inherit_doc Lean.Widget.goalToInteractive]
-def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM InteractiveGoal := do
+def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
   let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
   let showLetValues := pp.showLetValues.get (← getOptions)
@@ -165,9 +121,6 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
       else
         match localDecl with
         | LocalDecl.cdecl _index fvarId varName type _ _ =>
-          -- We rely on the fact that `withGoalCtx` runs `LocalContext.sanitizeNames`,
-          -- so the `userName`s of local hypotheses are already pretty-printed
-          -- and it suffices to simply `toString` them.
           let varName := toString varName
           let type ← instantiateMVars type
           if prevType? == none || prevType? == some type then
@@ -197,8 +150,6 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
       userName?
       goalPrefix := getGoalPrefix mvarDecl
       mvarId
-      -- Added:
-      hints
     }
 
 end GameServer

server/GameServer/RpcHandlers.lean

@@ -7,7 +7,6 @@ open Widget
 open RequestM
 open Meta
 
-
 /-! ## GameGoal -/
 
 namespace GameServer
@@ -113,10 +112,10 @@ def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pu
 
 open Meta in
 /-- Find all hints whose trigger matches the current goal -/
-def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
+def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
   goal.withContext do
-    let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
-      | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
+    let some level ← getLevelByFileName? initParams m.mkInputContext.fileName
+      | throwError "Level not found: {m.mkInputContext.fileName}"
     let hints ← level.hints.filterMapM fun hint => do
       openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
         if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
@@ -134,8 +133,212 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams :
           return none
     return hints
 
+/-- Get the line that ends in `pos`. Note that `pos` is expected to be the
+position of a `\n` but this is not enforced. -/
+def _root_.Lean.FileMap.getLineBefore (fmap : FileMap) (pos : String.Pos) : String := Id.run do
+  match fmap.positions.findIdx? (· == pos) with
+  | none =>
+    panic s!"Position {pos} is not a newline character in " ++
+      s!"the following string: '{fmap.source}'!"
+  | some 0 =>
+    -- the first entry of `positions` is always `0`
+    return ""
+  | some (i + 1) =>
+    let line : Substring := ⟨fmap.source, fmap.positions.get! i, pos⟩
+    return line.toString
+
+/-- Returns the `List` without the last element. -/
+def _root_.List.dropBack {α : Type _} : List α → List α
+| [] => []
+| _ :: [] => []
+| x :: xs => x :: xs.dropBack
+
+/-- Trim empty lines from the file and add a single newline. -/
+def _root_.Lean.FileMap.trim (fmap : FileMap) : FileMap :=
+  let str := match fmap.source.trim with
+  | "" => ""
+  | s => s ++ "\n"
+  FileMap.ofString str
+
+/-- Returns the `Array` without the last element. -/
+def _root_.Array.dropBack {α : Type _} (a : Array α) : Array α := ⟨a.data.dropBack⟩
+
+/-- Add custom diagnostics about whether the level is completed. -/
+def addCompletionDiagnostics (diag : Array InteractiveDiagnostic) (goals : Array InteractiveGoalWithHints)
+    (pos : Lsp.Position) (prevGoalCount : Nat) : RequestM <| Array InteractiveDiagnostic := do
+  let mut out : Array InteractiveDiagnostic := diag
+
+  if goals.size == 0 then
+    if diag.any (·.severity? == some .error) then
+      pure ()
+    else if diag.any (·.severity? == some .warning) then
+      out := out.push {
+        message := .text "level completed with warnings. 🎭"
+        range := {
+          start := pos
+          «end» := pos
+          }
+        severity? := Lsp.DiagnosticSeverity.information }
+    else
+      out := out.push {
+        message := .text "level completed! 🎉"
+        range := {
+          start := pos
+          «end» := pos
+          }
+        severity? := Lsp.DiagnosticSeverity.information }
+  else if goals.size < prevGoalCount then
+    out := out.push {
+      message := .text "intermediate goal solved! 🎉"
+      range := {
+        start := pos
+        «end» := pos
+        }
+      severity? := Lsp.DiagnosticSeverity.information
+    }
+
+
+  return out
+          -- diagsAtPos := if goalsAtPos.size < intermediateGoalCount then
+          --   diagsAtPos.push {
+          --     message := .text "intermediate goal solved 🎉"
+          --     range := {
+          --       start := lspPosAt
+          --       «end» := lspPosAt
+          --       }
+          --     severity? := Lsp.DiagnosticSeverity.information
+          --   }
+          --   else diagsAtPos
+
+/-- Request that returns the goals at the end of each line of the tactic proof
+plus the diagnostics (i.e. warnings/errors) for the proof.
+ -/
+def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option ProofState)) := do
+  let doc ← readDoc
+  let rc ← readThe RequestContext
+  let text := doc.meta.text.trim
+
+  -- BUG: trimming here is a problem, since the snap might already be evaluated before
+  -- the trimming and then the positions don't match anymore :((
+
+  withWaitFindSnap
+    doc
+    -- TODO (Alex): I couldn't find a good condition to find the correct snap. So we are looking
+    -- for the first snap with goals here.
+    -- NOTE (Jon): The entire proof is in one snap, so hoped that Position `0` is good enough.
+    (fun snap => ¬ (snap.infoTree.goalsAt? doc.meta.text 0).isEmpty)
+    (notFoundX := return none)
+    fun snap => do
+      -- `snap` is the one snapshot containing the entire proof.
+      let mut steps : Array <| InteractiveGoalsWithHints := #[]
+
+      -- Question: Is there a difference between the diags of this snap and the last snap?
+      -- Should we get the diags from there?
+      -- Answer: The last snap only copied the diags from the end of this snap
+      let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray
+
+      let mut intermediateGoalCount := 0
+
+      -- Drop the last position as we ensured that there is always a newline at the end
+      for pos in text.positions.dropBack do
+        -- iterate over all newlines in the proof and get the goals and hints at each position
+        -- TODO: we drop the last position because we always have a newline. Would be better
+        -- to trim newlines instead before submitting!
+        let source := text.getLineBefore pos
+
+        if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text pos then
+          pure ()
+          let goalAtPos : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
+            fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
+              -- TODO: What does this function body do?
+              -- let ciAfter := { ci with mctx := ti.mctxAfter }
+              let ci := if useAfter then
+                  { ci with mctx := tacticInfo.mctxAfter }
+                else
+                  { ci with mctx := tacticInfo.mctxBefore }
+              -- compute the interactive goals
+              let goalMvars : List MVarId ← ci.runMetaM {} do
+                return if useAfter then tacticInfo.goalsAfter else tacticInfo.goalsBefore
+
+              let interactiveGoals : List InteractiveGoalWithHints ← ci.runMetaM {} do
+                goalMvars.mapM fun goal => do
+                  let hints ← findHints goal doc.meta rc.initParams
+                  let interactiveGoal ← goalToInteractive goal
+                  return ⟨interactiveGoal, hints⟩
+              -- TODO: This code is way old, can it be deleted?
+              -- compute the goal diff
+              -- let goals ← ciAfter.runMetaM {} (do
+              --     try
+              --       Widget.diffInteractiveGoals useAfter ti goals
+              --     catch _ =>
+              --       -- fail silently, since this is just a bonus feature
+              --       return goals
+              -- )
+              return interactiveGoals
+          let goalsAtPos : Array InteractiveGoalWithHints := ⟨goalAtPos.foldl (· ++ ·) []⟩
+
+          -- diags are labeled in Lsp-positions, which differ from the lean-internal
+          -- positions by `1`.
+          let lspPosAt := text.utf8PosToLspPos pos
+
+          let mut diagsAtPos : Array InteractiveDiagnostic :=
+            -- `+1` for getting the errors after the line.
+            diag.filter (·.range.start.line + 1 == lspPosAt.line)
+
+          diagsAtPos ← addCompletionDiagnostics diagsAtPos goalsAtPos lspPosAt intermediateGoalCount
+
+          intermediateGoalCount := goalsAtPos.size
+
+          steps := steps.push ⟨goalsAtPos, source, diagsAtPos, lspPosAt.line, lspPosAt.character⟩
+        else
+          -- No goals present
+          steps := steps.push default
+
+
+
+      --       //   if (goals.length && goalCount > goals.length) {
+      -- //     messages.unshift({
+      -- //       range: {
+      -- //         start: {
+      -- //           line: i-1,
+      -- //           character: 0,
+      -- //         },
+      -- //         end: {
+      -- //           line: i-1,
+      -- //           character: 0,
+      -- //         }},
+      -- //       severity: DiagnosticSeverity.Information,
+      -- //       message: {
+      -- //       text: 'intermediate goal solved 🎉'
+      -- //       }
+      -- //     })
+      -- //   }
+
+      -- Level is completed if there are no errrors or warnings
+
+      let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error)
+      let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning)
+
+      -- Filter out the "unsolved goals" message
+      diag := diag.filter (fun d => match d.message with
+        | .append ⟨(.text x) :: _⟩ => x != "unsolved goals"
+        | _ => true)
+
+      let lastPos := text.utf8PosToLspPos text.positions.back
+      let remainingDiags : Array InteractiveDiagnostic :=
+        diag.filter (fun d => d.range.start.line >= lastPos.line)
+
+      return some {
+        steps := steps,
+        diagnostics := remainingDiags,
+        completed := completed,
+        completedWithWarnings := completedWithWarnings,
+        lastPos := lastPos.line
+        }
+
 open RequestM in
-def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do
+
+def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option <| InteractiveGoals)) := do
   let doc ← readDoc
   let rc ← readThe RequestContext
   let text := doc.meta.text
@@ -145,7 +348,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
   withWaitFindSnap doc (fun s => ¬ (s.infoTree.goalsAt? doc.meta.text hoverPos).isEmpty)
     (notFoundX := return none) fun snap => do
       if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
-        let goals : List InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+        let goals : List <| Array InteractiveGoal ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
           let ciAfter := { ci with mctx := ti.mctxAfter }
           let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
           -- compute the interactive goals
@@ -153,8 +356,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
             return List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
           let goals ← ci.runMetaM {} do
              goals.mapM fun goal => do
-              let hints ← findHints goal doc rc.initParams
-              return ← goalToInteractive goal hints
+              -- let hints ← findHints goal doc.meta rc.initParams
+              return ← goalToInteractive goal
           -- compute the goal diff
           -- let goals ← ciAfter.runMetaM {} (do
           --     try
@@ -163,8 +366,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
           --       -- fail silently, since this is just a bonus feature
           --       return goals
           -- )
-          return {goals}
-        return some <| goals.foldl (· ++ ·) ⟨#[]⟩
+          return goals
+        return some <| ⟨goals.foldl (· ++ ·) #[]⟩
       else
         return none
 
@@ -172,7 +375,16 @@ builtin_initialize
   registerBuiltinRpcProcedure
     `Game.getInteractiveGoals
     Lsp.PlainGoalParams
-    (Option InteractiveGoals)
+    (Option <| InteractiveGoals
+    )
     getInteractiveGoals
 
+builtin_initialize
+  registerBuiltinRpcProcedure
+    `Game.getProofState
+    Lsp.PlainGoalParams
+    (Option ProofState)
+    getProofState
+
+
 end GameServer

server/GameServer/Structures.lean

@@ -0,0 +1,93 @@
+import Lean.Widget.InteractiveGoal
+import Lean.Widget.InteractiveDiagnostic
+import Lean.Data.Lsp.Diagnostics
+
+/-!
+This file contains the custom data structures use by the server.
+
+Some of them overwrite built-in structures from Lean.
+
+In particular, the structures from `Lean.Widget.InteractiveGoal` are duplicated with
+the following extension:
+
+* `isAssumption?` in `InteractiveHypothesisBundle`: stores if a hypothesis is of type `Prop`.
+
+NOTE: Changes here need to be reflected in  the corresponding `interface` in `rcp_api.ts`
+on the client-side.
+-/
+
+open Lean Server Widget
+
+namespace GameServer
+
+/-- Extend the interactive hypothesis bundle with an option to distinguish
+"assumptions" from "objects". "Assumptions" are hypotheses of type `Prop`. -/
+-- @[inherit_doc Lean.Widget.InteractiveHypothesisBundle]
+structure InteractiveHypothesisBundle extends Lean.Widget.InteractiveHypothesisBundle where
+  /-- The hypothesis's type is of type `Prop` -/
+  isAssumption? : Option Bool := none
+deriving RpcEncodable
+
+-- duplicated but with custom `InteractiveHypothesisBundle`
+@[inherit_doc Lean.Widget.InteractiveGoalCore]
+structure InteractiveGoalCore where
+  hyps : Array InteractiveHypothesisBundle
+  type : CodeWithInfos
+  ctx : WithRpcRef Elab.ContextInfo
+
+-- duplicated but with custom `InteractiveGoalCore`
+@[inherit_doc Lean.Widget.InteractiveGoal]
+structure InteractiveGoal extends InteractiveGoalCore where
+  userName? : Option String
+  goalPrefix : String
+  mvarId : MVarId
+  isInserted? : Option Bool := none
+  isRemoved? : Option Bool := none
+deriving RpcEncodable
+
+-- duplicated with custom `InteractiveGoalCore`
+@[inherit_doc Lean.Widget.InteractiveTermGoal]
+structure InteractiveTermGoal extends InteractiveGoalCore where
+  range : Lsp.Range
+  term : WithRpcRef Elab.TermInfo
+deriving RpcEncodable
+
+/-- A hint in the game at the corresponding goal. -/
+structure GameHint where
+  text : String
+  hidden : Bool
+deriving FromJson, ToJson
+
+/-- Bundled `InteractiveGoal` together with an array of hints that apply at this stage. -/
+structure InteractiveGoalWithHints where
+  goal : InteractiveGoal
+  /-- Extended the `InteractiveGoal` by an array of hints at that goal. -/
+  hints : Array GameHint
+deriving RpcEncodable
+
+structure InteractiveGoalsWithHints where
+  goals : Array InteractiveGoalWithHints
+  /-- The content of the line evaluated. -/
+  command : String
+  diags : Array InteractiveDiagnostic := default
+  line : Option Nat -- only for debugging
+  column : Option Nat -- only for debugging
+
+deriving RpcEncodable
+
+instance : Inhabited InteractiveGoalsWithHints := ⟨default, default, default, none, none⟩
+
+/-- Collected goals throughout the proof. Used for communication with the game client. -/
+structure ProofState where
+  /-- goals after each line. includes the hints. -/
+  steps : Array <| InteractiveGoalsWithHints
+  /-- diagnostics contains all errors and warnings.
+
+  TODO: I think they contain information about which line they belong to. Verify this.
+  -/
+  diagnostics : Array InteractiveDiagnostic := default
+  /-- Whether the level is considered solved. -/
+  completed : Bool
+  completedWithWarnings : Bool
+  lastPos : Nat -- only for debugging
+deriving RpcEncodable

server/lake-manifest.json

@@ -9,6 +9,24 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.5.0",
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "rev": "a6b484980b41aab874fb3113ec5245bd91b625d8",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.4.0",
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",
  "lakeDir": ".lake"}

server/lakefile.lean

@@ -8,6 +8,8 @@ def leanVersion : String := s!"v{Lean.versionString}"
 
 require std from git "https://github.com/leanprover/std4.git" @ leanVersion
 
+require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
+
 lean_lib GameServer
 
 @[default_target]