From 854ac6ee55bd7beed4eecd01e6ca8ab0251eb71b Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Fri, 2 Dec 2022 09:57:34 +0100 Subject: [PATCH] display messages (displaying all of them immediately for now) --- client/src/components/TacticState.tsx | 5 +++- server/leanserver/GameServer/FileWorker.lean | 13 +------- server/leanserver/GameServer/RpcHandlers.lean | 30 ++++++++++++++++--- 3 files changed, 31 insertions(+), 17 deletions(-) diff --git a/client/src/components/TacticState.tsx b/client/src/components/TacticState.tsx index b739d03..7a926ca 100644 --- a/client/src/components/TacticState.tsx +++ b/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 = /:1:(?[^:]*): (?.*)/; @@ -30,6 +32,7 @@ function Goal({ goal }) { } Prove: {goal.goal} + {goal.messages.map((message) => {message})} ) } diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean index 05cdf3e..6984412 100644 --- a/server/leanserver/GameServer/FileWorker.lean +++ b/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 - -- TODO: make world and game configurable - let some level ← getLevel? {game := `TestGame, world := `TestWorld, level := levelId} - | throwServerError "Level not found" + let level ← GameServer.getLevelByFileName inputCtx.fileName -- 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 diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean index fc21cb2..e953f36 100644 --- a/server/leanserver/GameServer/RpcHandlers.lean +++ b/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