display messages (displaying all of them immediately for now)

client/src/components/TacticState.tsx

@@ -3,10 +3,12 @@ import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
+import ReactMarkdown from 'react-markdown';
+import { MathJax } from "better-react-mathjax";
 
 import List from '@mui/material/List';
 import ListItem from '@mui/material/ListItem';
-import { Paper, Box, Typography } from '@mui/material';
+import { Paper, Box, Typography, Alert } from '@mui/material';
 
 const errorRegex = /<stdin>:1:(?<col>[^:]*): (?<msg>.*)/;
 
@@ -30,6 +32,7 @@ function Goal({ goal }) {
         </List></Box>}
       <Typography>Prove:</Typography>
       <Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
+      {goal.messages.map((message) => <Alert severity="info" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert>)}
     </Box>)
 }
 

server/leanserver/GameServer/FileWorker.lean

@@ -59,14 +59,6 @@ open JsonRpc
 
 section Elab
 
--- TODO: Find a better way to pass on the file name?
-def levelIdFromFileName (fileName : String) : IO Nat := do
-  if fileName.startsWith "/level" then
-    if let some id := (fileName.drop "/level".length).toNat? then
-      return id
-  throwServerError s!"Could not find level ID in file name: {fileName}"
-  return 1
-
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) (couldBeEndSnap : Bool) : IO Snapshot := do
   let cmdState := snap.cmdState
@@ -100,10 +92,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get scope.opts) <| liftM (m := BaseIO) do
       Elab.Command.catchExceptions
         (getResetInfoTrees *> do
-          let levelId ← levelIdFromFileName inputCtx.fileName
+          let level ← GameServer.getLevelByFileName inputCtx.fileName
-          -- TODO: make world and game configurable
-          let some level ← getLevel? {game := `TestGame, world := `TestWorld, level := levelId}
-            | throwServerError "Level not found"
           -- Insert invisible `skip` command to make sure we always display the initial goal
           let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
           -- Insert final `done` command to display unsolved goal error in the end

server/leanserver/GameServer/RpcHandlers.lean

@@ -1,4 +1,5 @@
 import Lean
+import GameServer.EnvExtensions
 
 open Lean
 open Server
@@ -18,10 +19,11 @@ structure GameGoal where
   objects : List GameLocalDecl
   assumptions : List GameLocalDecl
   goal : String
+  messages : Array String
 deriving FromJson, ToJson
 
 
-def Lean.MVarId.toGameGoal (goal : MVarId) : MetaM GameGoal := do
+def Lean.MVarId.toGameGoal (goal : MVarId) (messages : Array String) : MetaM GameGoal := do
 match (← getMCtx).findDecl? goal with
 | none          => throwError "unknown goal"
 | some mvarDecl => do
@@ -44,7 +46,7 @@ match (← getMCtx).findDecl? goal with
       return { userName := decl.userName, type := toString (← Meta.ppExpr decl.type) }
     let assumptions ← assumptions.mapM fun decl => do
       return { userName := decl.userName, type := toString (← Meta.ppExpr decl.type) }
-    return {objects := objects, assumptions := assumptions, goal := toString (← Meta.ppExpr mvarDecl.type) }
+    return {objects := objects, assumptions := assumptions, goal := toString (← Meta.ppExpr mvarDecl.type), messages }
 
 
 namespace GameServer
@@ -56,11 +58,30 @@ structure PlainGoal where
   goals : Array GameGoal
   deriving FromJson, ToJson
 
+-- TODO: Find a better way to pass on the file name?
+def levelIdFromFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String) : m Nat := do
+  if fileName.startsWith "/level" then
+    if let some id := (fileName.drop "/level".length).toNat? then
+      return id
+  throwError s!"Could not find level ID in file name: {fileName}"
+  return 1
+
+def getLevelByFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String) : m GameLevel := do
+  let levelId ← levelIdFromFileName fileName
+  -- TODO: make world and game configurable
+  let some level ← getLevel? {game := `TestGame, world := `TestWorld, level := levelId}
+    | throwError "Level not found"
+  return level
+
+def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array String) := do
+  let level ← getLevelByFileName doc.meta.mkInputContext.fileName
+  return level.messages.map GoalMessageEntry.message
+
 def getGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option PlainGoal)) := do
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
-  -- TODO: Couldn't find a good condition to find the correct snap. So we are looking
+  -- TODO: I couldn't find a good condition to find the correct snap. So we are looking
   -- for the first snap with goals here:
   withWaitFindSnap doc (fun s => ¬ (s.infoTree.goalsAt? doc.meta.text hoverPos).isEmpty)
     (notFoundX := return none) fun snap => do
@@ -69,7 +90,8 @@ def getGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option PlainGoal
           let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
           let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
           let goals ← ci.runMetaM {} $ goals.mapM fun goal => do
-            return ← goal.toGameGoal
+            let messages ← findMessages goal doc
+            return ← goal.toGameGoal messages
           return goals
         return some { goals := goals.foldl (· ++ ·) ∅ }
       else