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/Commands.lean b/server/leanserver/GameServer/Commands.lean index db9628b..c991344 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -116,16 +116,10 @@ def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term /-- Declare a message. This version doesn't prevent the unused linter variable from running. -/ local elab "Message'" decls:mydecl* ":" goal:term "=>" msg:str : command => do let g ← liftMacroM $ mkGoalSyntax goal (decls.map (λ decl => (getIdent decl, getType decl))).toList - let g ← liftTermElabM do (return ← instantiateMVars (← elabTerm g none)) - let (ctx_size, normalized_goal) ← liftTermElabM do - let msg_mvar ← mkFreshExprMVar g MetavarKind.syntheticOpaque - msg_mvar.mvarId!.withContext do - let (_, msg_mvar) ← msg_mvar.mvarId!.introNP decls.size - return ((← msg_mvar.getDecl).lctx.size, (← normalizedRevertExpr msg_mvar)) + let g ← liftTermElabM do (return ← elabTermAndSynthesize g none) modifyCurLevel fun level => pure {level with messages := level.messages.push { - ctx_size := ctx_size, - normalized_goal := normalized_goal, - intro_nb := decls.size, + goal := g, + intros := decls.size, message := msg.getString }} /-- Declare a message in reaction to a given tactic state in the current level. -/ diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 5ba1b6e..67c452c 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -11,9 +11,8 @@ open Lean /-! ## Messages -/ structure GoalMessageEntry where - ctx_size : Nat - normalized_goal : Expr - intro_nb : Nat + goal : Expr + intros : Nat message : String deriving Repr diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean index 05cdf3e..b8f1d73 100644 --- a/server/leanserver/GameServer/FileWorker.lean +++ b/server/leanserver/GameServer/FileWorker.lean @@ -9,11 +9,10 @@ open Lean open Elab open Parser -private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message := +private def mkErrorMessage (c : InputContext) (pos : String.Pos) (errorMsg : String) : Message := let pos := c.fileMap.toPosition pos { fileName := c.fileName, pos := pos, data := errorMsg } -open Parser in private def mkEOI (pos : String.Pos) : Syntax := let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring pos) "" mkNode `Lean.Parser.Module.eoi #[atom] @@ -28,23 +27,27 @@ partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext) if inputCtx.input.atEnd pos ∧ couldBeEndSnap then stx := mkEOI pos return (stx, { pos, recovering }, messages, 0) - let c := mkParserContext inputCtx pmctx - let s := { cache := initCacheForInput c.input, pos := pos : ParserState } - let s := whitespace c s + + let tokens := getTokenTable pmctx.env + + let s := whitespace.run inputCtx pmctx tokens { cache := initCacheForInput inputCtx.input, pos } let endOfWhitespace := s.pos - let s := (Tactic.sepByIndentSemicolon tacticParser).fn c s + + let p := (Tactic.sepByIndentSemicolon tacticParser).fn + let s := p.run inputCtx pmctx tokens { cache := initCacheForInput inputCtx.input, pos } + pos := s.pos match s.errorMsg with | none => stx := s.stxStack.back recovering := false | some errorMsg => - messages := messages.add <| mkErrorMessage c s.pos (toString errorMsg) + messages := messages.add <| mkErrorMessage inputCtx s.pos (toString errorMsg) recovering := true stx := s.stxStack.back - if ¬ c.input.atEnd s.pos then - messages := messages.add <| mkErrorMessage c s.pos "end of input" - return (stx, { pos := c.input.endPos, recovering }, messages, endOfWhitespace) + if ¬ inputCtx.input.atEnd s.pos then + messages := messages.add <| mkErrorMessage inputCtx s.pos "end of input" + return (stx, { pos := inputCtx.input.endPos, recovering }, messages, endOfWhitespace) end MyModule @@ -59,14 +62,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 +95,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 @@ -340,10 +332,11 @@ section Initialization | Except.error e => throw (e : ElabTaskError)) let doc : EditableDocument := ⟨meta, AsyncList.delayed snaps, cancelTk⟩ return (ctx, - { doc := doc - pendingRequests := RBMap.empty - rpcSessions := RBMap.empty - }) + { doc := doc + initHeaderStx := Syntax.missing + pendingRequests := RBMap.empty + rpcSessions := RBMap.empty + }) end Initialization diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean index fc21cb2..6fb41d8 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,38 @@ 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 + +open Meta in +/-- Find all messages whose trigger matches the current goal -/ +def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array String) := do + let level ← getLevelByFileName doc.meta.mkInputContext.fileName + let messages ← level.messages.filterMapM fun message => do + let (declMvars, binderInfo, messageGoal) ← forallMetaBoundedTelescope message.goal message.intros + if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions + then return some message.message + else return none + return messages + +/-- Get goals and messages at a given position -/ 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 +98,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 diff --git a/server/leanserver/GameServer/Utils.lean b/server/leanserver/GameServer/Utils.lean index 271275d..4ad81bc 100644 --- a/server/leanserver/GameServer/Utils.lean +++ b/server/leanserver/GameServer/Utils.lean @@ -2,29 +2,13 @@ import Lean open Lean -def Lean.Expr.getFVars (e : Expr) : Array FVarId := - (Lean.collectFVars {} e).fvarIds - - -/-- Returns the type of the goal after reverting all free variables in the order -where they appear in the goal type. -/ -partial def normalizedRevertExpr (goal : MVarId) : MetaM Expr := do - goal.withContext do - let (_, new) ← goal.revert (← goal.getType).getFVars true - let e ← new.getType - if e.hasFVar then - return ← normalizedRevertExpr new - else - return (← new.getType) - - def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := { msgs := log.msgs.filter (·.severity matches .error) } /-- A version of `println!` that actually does its job by flushing stdout. -/ def output {α : Type} [ToString α] (s : α) : IO Unit := do println! s - IO.FS.Stream.flush (← IO.getStdout) + IO.FS.Stream.flush (← IO.getStdout) def Lean.LocalDecl.toJson (decl : LocalDecl) : MetaM Json := return Lean.ToJson.toJson [toString decl.userName, toString (← Meta.ppExpr decl.type)] diff --git a/server/leanserver/GameServer/Watchdog.lean b/server/leanserver/GameServer/Watchdog.lean index 0cc2aa1..bc0e09d 100644 --- a/server/leanserver/GameServer/Watchdog.lean +++ b/server/leanserver/GameServer/Watchdog.lean @@ -18,12 +18,10 @@ open System.Uri for (_, fw) in workers do if let WorkerState.running := fw.state then workerTasks := workerTasks.push <| fw.commTask.map (ServerEvent.workerEvent fw) - if let some ge ← fw.groupedEditsRef.get then - workerTasks := workerTasks.push <| ge.signalTask.map (ServerEvent.workerEvent fw) let ev ← IO.waitAny (clientTask :: workerTasks.toList) - if ← Game.handleServerEvent ev then + if ← Game.handleServerEvent ev then -- handle Game requests mainLoop (←runClientTask) else match ev with @@ -35,60 +33,28 @@ open System.Uri | Message.request id method (some params) => handleRequest id method (toJson params) mainLoop (←runClientTask) - | Message.notification "textDocument/didChange" (some params) => - let p ← parseParams DidChangeTextDocumentParams (toJson params) - let fw ← findFileWorker! p.textDocument.uri - let now ← monoMsNow - /- We wait `editDelay`ms since last edit before applying the changes. -/ - let applyTime := now + st.editDelay - let queuedMsgs? ← fw.groupedEditsRef.modifyGet fun - | some ge => (some ge.queuedMsgs, some { ge with - applyTime := applyTime - params.textDocument := p.textDocument - params.contentChanges := ge.params.contentChanges ++ p.contentChanges - -- drain now-outdated messages and respond with `contentModified` below - queuedMsgs := #[] }) - | none => (none, some { - applyTime := applyTime - params := p - /- This is overwritten just below. -/ - signalTask := Task.pure WorkerEvent.processGroupedEdits - queuedMsgs := #[] }) - match queuedMsgs? with - | some queuedMsgs => - for msg in queuedMsgs do - match msg with - | JsonRpc.Message.request id _ _ => - fw.erasePendingRequest id - (← read).hOut.writeLspResponseError { - id := id - code := ErrorCode.contentModified - message := "File changed." - } - | _ => pure () -- notifications do not need to be cancelled - | _ => - let t ← fw.runEditsSignalTask - fw.groupedEditsRef.modify (Option.map fun ge => { ge with signalTask := t } ) + | Message.response .. => + -- TODO: handle client responses mainLoop (←runClientTask) + | Message.responseError _ _ e .. => + throwServerError s!"Unhandled response error: {e}" | Message.notification method (some params) => handleNotification method (toJson params) mainLoop (←runClientTask) - | Message.response "register_ilean_watcher" _ => - mainLoop (←runClientTask) | _ => throwServerError "Got invalid JSON-RPC message" | ServerEvent.clientError e => throw e | ServerEvent.workerEvent fw ev => match ev with - | WorkerEvent.processGroupedEdits => - handleEdits fw - mainLoop clientTask | WorkerEvent.ioError e => - throwServerError s!"IO error while processing events for {fw.doc.meta.uri}: {e}" + throwServerError s!"IO error while processing events for {fw.doc.uri}: {e}" | WorkerEvent.crashed _ => - handleCrash fw.doc.meta.uri #[] + handleCrash fw.doc.uri #[] mainLoop clientTask | WorkerEvent.terminated => throwServerError "Internal server error: got termination event for worker that should have been removed" + | .importsChanged => + startFileWorker fw.doc + mainLoop clientTask def initAndRunWatchdogAux : GameServerM Unit := do let st ← read @@ -156,7 +122,6 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do args := args fileWorkersRef := fileWorkersRef initParams := initRequest.param - editDelay := initRequest.param.initializationOptions? |>.bind InitializationOptions.editDelay? |>.getD 200 workerPath srcSearchPath references diff --git a/server/leanserver/Main.lean b/server/leanserver/Main.lean index 114c168..95c0a6e 100644 --- a/server/leanserver/Main.lean +++ b/server/leanserver/Main.lean @@ -2,8 +2,11 @@ import GameServer.Watchdog import GameServer.FileWorker -def main : List String → IO UInt32 := fun args => do +unsafe def main : List String → IO UInt32 := fun args => do let e ← IO.getStderr + + Lean.enableInitializersExecution + if args[0]? == some "--server" then MyServer.Watchdog.watchdogMain [] else if args[0]? == some "--worker" then diff --git a/server/leanserver/lean-toolchain b/server/leanserver/lean-toolchain index 5dcde6d..5ca06ea 100644 --- a/server/leanserver/lean-toolchain +++ b/server/leanserver/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-10-29 +leanprover/lean4:nightly-2022-12-03 diff --git a/server/testgame/gameserver b/server/testgame/gameserver new file mode 100755 index 0000000..21de520 Binary files /dev/null and b/server/testgame/gameserver differ diff --git a/server/testgame/lake-manifest.json b/server/testgame/lake-manifest.json new file mode 100644 index 0000000..06dba30 --- /dev/null +++ b/server/testgame/lake-manifest.json @@ -0,0 +1,64 @@ +{"version": 4, + "packagesDir": "./lake-packages", + "packages": + [{"git": + {"url": "https://github.com/xubaiw/CMark.lean", + "subDir?": null, + "rev": "2cc7cdeef67184f84db6731450e4c2b258c28fe8", + "name": "CMark", + "inputRev?": "main"}}, + {"git": + {"url": "https://github.com/leanprover/lake", + "subDir?": null, + "rev": "235383015cdcb0082777b0347b84dba01843c79c", + "name": "lake", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/leanprover/doc-gen4", + "subDir?": null, + "rev": "7009910876145a9a1220359f968ba7045dd05290", + "name": "doc-gen4", + "inputRev?": "main"}}, + {"git": + {"url": "https://github.com/mhuisi/lean4-cli", + "subDir?": null, + "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e", + "name": "Cli", + "inputRev?": "nightly"}}, + {"git": + {"url": "https://github.com/leanprover-community/mathlib4.git", + "subDir?": null, + "rev": "9b15aa6f091a623f992d6fff76167864794ce350", + "name": "mathlib", + "inputRev?": "9b15aa6f091a623f992d6fff76167864794ce350"}}, + {"git": + {"url": "https://github.com/gebner/quote4", + "subDir?": null, + "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf", + "name": "Qq", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/JLimperg/aesop", + "subDir?": null, + "rev": "70c59fcfc63de90786d59222c32468dab87964c5", + "name": "aesop", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/hargonix/LeanInk", + "subDir?": null, + "rev": "9f3101452135964ac9107ec8e9910bfd14022bbc", + "name": "leanInk", + "inputRev?": "doc-gen"}}, + {"path": {"name": "GameServer", "dir": "./../leanserver"}}, + {"git": + {"url": "https://github.com/xubaiw/Unicode.lean", + "subDir?": null, + "rev": "6dd6ae3a3839c8350a91876b090eda85cf538d1d", + "name": "Unicode", + "inputRev?": "main"}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "42bb39d34ec7dcb07580458efa4a7936bd5192b7", + "name": "std", + "inputRev?": "main"}}]} diff --git a/server/testgame/lakefile.lean b/server/testgame/lakefile.lean index 9be3d46..1de4e98 100644 --- a/server/testgame/lakefile.lean +++ b/server/testgame/lakefile.lean @@ -4,7 +4,7 @@ open Lake DSL require GameServer from ".."/"leanserver" require mathlib from git - "https://github.com/leanprover-community/mathlib4.git"@"b1cf06cb126ee163a7dc895c1aee17946ff20900" + "https://github.com/leanprover-community/mathlib4.git"@"9b15aa6f091a623f992d6fff76167864794ce350" package TestGame diff --git a/server/testgame/lean-toolchain b/server/testgame/lean-toolchain index 5dcde6d..5ca06ea 100644 --- a/server/testgame/lean-toolchain +++ b/server/testgame/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-10-29 +leanprover/lean4:nightly-2022-12-03