|
|
|
@ -3,6 +3,7 @@ import Lean.Server.FileWorker
|
|
|
|
import GameServer.Game
|
|
|
|
import GameServer.Game
|
|
|
|
import GameServer.ImportModules
|
|
|
|
import GameServer.ImportModules
|
|
|
|
import GameServer.SaveData
|
|
|
|
import GameServer.SaveData
|
|
|
|
|
|
|
|
import GameServer.EnvExtensions
|
|
|
|
|
|
|
|
|
|
|
|
namespace MyModule
|
|
|
|
namespace MyModule
|
|
|
|
|
|
|
|
|
|
|
|
@ -60,8 +61,8 @@ open Snapshots
|
|
|
|
open JsonRpc
|
|
|
|
open JsonRpc
|
|
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
/--
|
|
|
|
Game-specific state to be packed on top of the `Lean.Server.FileWorker.WorkerState`
|
|
|
|
Game-specific state to be packed on top of the `Server.FileWorker.WorkerState`
|
|
|
|
used by the lean server.
|
|
|
|
used by the Lean server.
|
|
|
|
-/
|
|
|
|
-/
|
|
|
|
structure WorkerState :=
|
|
|
|
structure WorkerState :=
|
|
|
|
/--
|
|
|
|
/--
|
|
|
|
@ -84,7 +85,7 @@ structure WorkerState :=
|
|
|
|
deriving ToJson, FromJson
|
|
|
|
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`.
|
|
|
|
`Server.FileWorker.WorkerM`.
|
|
|
|
-/
|
|
|
|
-/
|
|
|
|
abbrev WorkerM := StateT WorkerState 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)
|
|
|
|
pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
|
|
|
|
data := s }}
|
|
|
|
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?
|
|
|
|
-- TODO: use HashSet for allowed tactics?
|
|
|
|
/--
|
|
|
|
/--
|
|
|
|
Find all tactics in syntax object that are forbidden according to a
|
|
|
|
Find all tactics in syntax object that are forbidden according to a
|
|
|
|
@ -178,15 +169,20 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState :
|
|
|
|
match theoremsAndDefs.find? (·.name == n) with
|
|
|
|
match theoremsAndDefs.find? (·.name == n) with
|
|
|
|
| none =>
|
|
|
|
| none =>
|
|
|
|
-- Theorem will never be introduced in this game
|
|
|
|
-- Theorem will never be introduced in this game
|
|
|
|
addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
|
|
|
|
addMessageByDifficulty info s!"The theorem/definition '{n}' is not available in this game!"
|
|
|
|
| some thm =>
|
|
|
|
| some thm =>
|
|
|
|
-- Theorem is introduced at some point in the game.
|
|
|
|
-- Theorem is introduced at some point in the game.
|
|
|
|
if thm.disabled then
|
|
|
|
if thm.disabled then
|
|
|
|
-- Theorem is disabled in this level.
|
|
|
|
-- Theorem is disabled in this level.
|
|
|
|
addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
|
|
|
|
addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
|
|
|
|
else if thm.locked then
|
|
|
|
else if thm.locked then
|
|
|
|
-- Theorem is still locked.
|
|
|
|
match workerState.inventory.find? (· == n.toString) with
|
|
|
|
addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
|
|
|
|
| none =>
|
|
|
|
|
|
|
|
-- 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) :=
|
|
|
|
where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
|
|
|
|
-- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
|
|
|
|
-- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
|
|
|
|
@ -308,7 +304,7 @@ where
|
|
|
|
private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream)
|
|
|
|
private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream)
|
|
|
|
(snaps : Array Snapshot) : IO Unit := do
|
|
|
|
(snaps : Array Snapshot) : IO Unit := do
|
|
|
|
let trees := snaps.map fun snap => snap.infoTree
|
|
|
|
let trees := snaps.map fun snap => snap.infoTree
|
|
|
|
let references := findModuleRefs m.text trees (localVars := true)
|
|
|
|
let references ← findModuleRefs m.text trees (localVars := true) |>.toLspModuleRefs
|
|
|
|
let param := { version := m.version, references : LeanIleanInfoParams }
|
|
|
|
let param := { version := m.version, references : LeanIleanInfoParams }
|
|
|
|
hOut.writeLspNotification { method, param }
|
|
|
|
hOut.writeLspNotification { method, param }
|
|
|
|
|
|
|
|
|
|
|
|
@ -322,74 +318,133 @@ where
|
|
|
|
uri : String
|
|
|
|
uri : String
|
|
|
|
deriving ToJson, FromJson
|
|
|
|
deriving ToJson, FromJson
|
|
|
|
|
|
|
|
|
|
|
|
/-- Checks whether game level has been completed and sends a notification to the client -/
|
|
|
|
structure GameDiagnostics where
|
|
|
|
def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
|
|
|
|
diagnostics : List Diagnostic
|
|
|
|
-- check if there is any error or warning
|
|
|
|
deriving ToJson, FromJson
|
|
|
|
for snap in snaps do
|
|
|
|
|
|
|
|
if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning
|
|
|
|
structure GameParams where
|
|
|
|
then return
|
|
|
|
uri : String
|
|
|
|
let param := { uri := m.uri : GameCompletedParams}
|
|
|
|
diagnostics : GameDiagnostics
|
|
|
|
hOut.writeLspNotification { method := "$/game/completed", param }
|
|
|
|
deriving ToJson, FromJson
|
|
|
|
|
|
|
|
|
|
|
|
/-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
|
|
|
|
/-- WIP: publish diagnostics, all intermediate goals and if the game is completed. -/
|
|
|
|
private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
|
|
|
|
def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.InitializeParams) (hOut : FS.Stream) :
|
|
|
|
(gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams)
|
|
|
|
IO Unit := do
|
|
|
|
: AsyncElabM (Option Snapshot) := do
|
|
|
|
-- let text := m.text
|
|
|
|
cancelTk.check
|
|
|
|
|
|
|
|
let s ← get
|
|
|
|
-- -- `snap` is the one snapshot containing the entire proof.
|
|
|
|
let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
|
|
|
|
-- let mut goals : Array <| InteractiveGoalsWithHints := #[]
|
|
|
|
if lastSnap.isAtEnd then
|
|
|
|
-- for pos in text.positions do
|
|
|
|
publishGameCompleted m ctx.hOut s.snaps
|
|
|
|
-- let source := text.getLineBefore pos
|
|
|
|
publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
|
|
|
|
-- -- iterate over all newlines in the proof and get the goals and hints at each position
|
|
|
|
publishProgressDone m ctx.hOut
|
|
|
|
-- if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? text pos then
|
|
|
|
-- This will overwrite existing ilean info for the file, in case something
|
|
|
|
-- pure ()
|
|
|
|
-- went wrong during the incremental updates.
|
|
|
|
-- let goalAtPos : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
|
|
|
|
publishIleanInfoFinal m ctx.hOut s.snaps
|
|
|
|
-- fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
|
|
|
|
return none
|
|
|
|
-- -- TODO: What does this function body do?
|
|
|
|
publishProgressAtPos m lastSnap.endPos ctx.hOut
|
|
|
|
-- -- let ciAfter := { ci with mctx := ti.mctxAfter }
|
|
|
|
-- Make sure that there is at least one snap after the head snap, so that
|
|
|
|
-- let ci := if useAfter then
|
|
|
|
-- we can see the current goal even on an empty document
|
|
|
|
-- { ci with mctx := tacticInfo.mctxAfter }
|
|
|
|
let couldBeEndSnap := s.snaps.size > 1
|
|
|
|
-- else
|
|
|
|
let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
|
|
|
|
-- { ci with mctx := tacticInfo.mctxBefore }
|
|
|
|
gameWorkerState initParams
|
|
|
|
-- -- compute the interactive goals
|
|
|
|
set { s with snaps := s.snaps.push snap }
|
|
|
|
-- let goalMvars : List MVarId ← ci.runMetaM {} do
|
|
|
|
-- TODO(MH): check for interrupt with increased precision
|
|
|
|
-- return if useAfter then tacticInfo.goalsAfter else tacticInfo.goalsBefore
|
|
|
|
cancelTk.check
|
|
|
|
|
|
|
|
/- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
|
|
|
|
-- let interactiveGoals : List InteractiveGoalWithHints ← ci.runMetaM {} do
|
|
|
|
while preferring newer versions over old ones. The former is necessary because we do
|
|
|
|
-- goalMvars.mapM fun goal => do
|
|
|
|
not explicitly clear older diagnostics, while the latter is necessary because we do
|
|
|
|
-- let hints ← findHints goal m initParams
|
|
|
|
not guarantee that diagnostics are emitted in order. Specifically, it may happen that
|
|
|
|
-- let interactiveGoal ← goalToInteractive goal
|
|
|
|
we interrupted this elaboration task right at this point and a newer elaboration task
|
|
|
|
-- return ⟨interactiveGoal, hints⟩
|
|
|
|
emits diagnostics, after which we emit old diagnostics because we did not yet detect
|
|
|
|
-- -- TODO: This code is way old, can it be deleted?
|
|
|
|
the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
|
|
|
|
-- -- compute the goal diff
|
|
|
|
because we cannot guarantee that no further diagnostics are emitted after clearing
|
|
|
|
-- -- let goals ← ciAfter.runMetaM {} (do
|
|
|
|
them. -/
|
|
|
|
-- -- try
|
|
|
|
-- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
|
|
|
|
-- -- Widget.diffInteractiveGoals useAfter ti goals
|
|
|
|
-- because empty diagnostics clear existing error/information squiggles. Therefore we always
|
|
|
|
-- -- catch _ =>
|
|
|
|
-- want to publish in case there was previously a message at this position.
|
|
|
|
-- -- -- fail silently, since this is just a bonus feature
|
|
|
|
publishDiagnostics m snap.diagnostics.toArray ctx.hOut
|
|
|
|
-- -- return goals
|
|
|
|
publishIleanInfoUpdate m ctx.hOut #[snap]
|
|
|
|
-- -- )
|
|
|
|
return some snap
|
|
|
|
-- return interactiveGoals
|
|
|
|
|
|
|
|
-- let goalAtPos : Array InteractiveGoalWithHints := ⟨goalAtPos.foldl (· ++ ·) []⟩
|
|
|
|
/-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
|
|
|
|
-- goals := goals.push ⟨goalAtPos, source⟩
|
|
|
|
def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
|
|
|
|
-- else
|
|
|
|
(startAfterMs : UInt32) (gameWorkerState : WorkerState)
|
|
|
|
-- -- No goals present
|
|
|
|
: ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
|
|
|
|
-- goals := goals.push default
|
|
|
|
let ctx ← read
|
|
|
|
|
|
|
|
let some headerSnap := snaps[0]? | panic! "empty snapshots"
|
|
|
|
-- -- Question: Is there a difference between the diags of this snap and the last snap?
|
|
|
|
if headerSnap.msgLog.hasErrors then
|
|
|
|
-- -- Should we get the diags from there?
|
|
|
|
-- Treat header processing errors as fatal so users aren't swamped with
|
|
|
|
-- let diag : Array Widget.InteractiveDiagnostic := snap.interactiveDiags.toArray
|
|
|
|
-- followup errors
|
|
|
|
|
|
|
|
publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
|
|
|
|
-- -- Level is completed if there are no errrors or warnings
|
|
|
|
publishIleanInfoFinal m ctx.hOut #[headerSnap]
|
|
|
|
-- let completed : Bool := ¬ diag.any (fun d =>
|
|
|
|
return AsyncList.ofList [headerSnap]
|
|
|
|
-- d.severity? == some .error ∨ d.severity? == some .warning)
|
|
|
|
else
|
|
|
|
|
|
|
|
-- This will overwrite existing ilean info for the file since this has a
|
|
|
|
-- let param : ProofState := {
|
|
|
|
-- higher version number.
|
|
|
|
-- steps := goals,
|
|
|
|
publishIleanInfoUpdate m ctx.hOut snaps
|
|
|
|
-- diagnostics := diag,
|
|
|
|
return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
|
|
|
|
-- completed := completed }
|
|
|
|
IO.sleep startAfterMs
|
|
|
|
|
|
|
|
AsyncList.unfoldAsync (nextSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
|
|
|
|
-- 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
|
|
|
|
|
|
|
|
for snap in snaps do
|
|
|
|
|
|
|
|
if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning
|
|
|
|
|
|
|
|
then return
|
|
|
|
|
|
|
|
let param := { uri := m.uri : GameCompletedParams}
|
|
|
|
|
|
|
|
hOut.writeLspNotification { method := "$/game/completed", param }
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/-- 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
|
|
|
|
|
|
|
|
publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
|
|
|
|
|
|
|
|
publishProgressDone m ctx.hOut
|
|
|
|
|
|
|
|
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 }
|
|
|
|
|
|
|
|
cancelTk.check
|
|
|
|
|
|
|
|
publishProofState m snap initParams ctx.hOut
|
|
|
|
|
|
|
|
publishDiagnostics m snap.diagnostics.toArray ctx.hOut
|
|
|
|
|
|
|
|
publishIleanInfoUpdate m ctx.hOut #[snap]
|
|
|
|
|
|
|
|
return some snap
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-- 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
|
|
|
|
|
|
|
|
publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
|
|
|
|
|
|
|
|
publishIleanInfoFinal m ctx.hOut #[headerSnap]
|
|
|
|
|
|
|
|
return AsyncList.ofList [headerSnap]
|
|
|
|
|
|
|
|
else
|
|
|
|
|
|
|
|
publishIleanInfoUpdate m ctx.hOut snaps
|
|
|
|
|
|
|
|
return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
|
|
|
|
|
|
|
|
IO.sleep startAfterMs
|
|
|
|
|
|
|
|
AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
|
|
|
|
|
|
|
|
|
|
|
|
end Elab
|
|
|
|
end Elab
|
|
|
|
|
|
|
|
|
|
|
|
@ -439,7 +494,7 @@ def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
|
|
|
|
validSnaps := validSnaps.dropLast
|
|
|
|
validSnaps := validSnaps.dropLast
|
|
|
|
-- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
|
|
|
|
-- 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)
|
|
|
|
-- 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)
|
|
|
|
(startAfterMs := ctx.initParams.editDelay.toUInt32)
|
|
|
|
StateT.lift <| modify fun st => { st with
|
|
|
|
StateT.lift <| modify fun st => { st with
|
|
|
|
doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
|
|
|
|
doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
|
|
|
|
@ -453,6 +508,12 @@ def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
|
|
|
|
fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
|
|
|
|
fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
|
|
|
|
fileMap := default
|
|
|
|
fileMap := default
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/-- `gameDir` and `module` were added.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
TODO: In general this resembles little similarity with the
|
|
|
|
|
|
|
|
original code, and I don't know why...
|
|
|
|
|
|
|
|
-/
|
|
|
|
|
|
|
|
-- @[inherit_doc Lean.Server.FileWorker.compileHeader]
|
|
|
|
def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
|
|
|
|
def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
|
|
|
|
(gameDir : String) (module : Name):
|
|
|
|
(gameDir : String) (module : Name):
|
|
|
|
IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
|
|
|
|
IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
|
|
|
|
@ -488,7 +549,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
|
|
|
|
let cmdState := Elab.Command.mkState headerEnv {} opts
|
|
|
|
let cmdState := Elab.Command.mkState headerEnv {} opts
|
|
|
|
let cmdState := { cmdState with infoState := {
|
|
|
|
let cmdState := { cmdState with infoState := {
|
|
|
|
enabled := true
|
|
|
|
enabled := true
|
|
|
|
trees := #[Elab.InfoTree.context ({
|
|
|
|
trees := #[Elab.InfoTree.context (.commandCtx {
|
|
|
|
env := headerEnv
|
|
|
|
env := headerEnv
|
|
|
|
fileMap := m.text
|
|
|
|
fileMap := m.text
|
|
|
|
ngen := { namePrefix := `_worker }
|
|
|
|
ngen := { namePrefix := `_worker }
|
|
|
|
@ -505,7 +566,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
|
|
|
|
let headerSnap := {
|
|
|
|
let headerSnap := {
|
|
|
|
beginPos := 0
|
|
|
|
beginPos := 0
|
|
|
|
stx := headerStx
|
|
|
|
stx := headerStx
|
|
|
|
mpState := {}
|
|
|
|
mpState := {} -- was `headerParserState`
|
|
|
|
cmdState := cmdState
|
|
|
|
cmdState := cmdState
|
|
|
|
interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
|
|
|
|
interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
|
|
|
|
tacticCache := (← IO.mkRef {})
|
|
|
|
tacticCache := (← IO.mkRef {})
|
|
|
|
@ -513,49 +574,52 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
|
|
|
|
publishDiagnostics m headerSnap.diagnostics.toArray hOut
|
|
|
|
publishDiagnostics m headerSnap.diagnostics.toArray hOut
|
|
|
|
return (headerSnap, srcSearchPath)
|
|
|
|
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)
|
|
|
|
def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
|
|
|
|
(gameDir : String) (gameWorkerState : WorkerState) : IO (WorkerContext × Server.FileWorker.WorkerState) := do
|
|
|
|
(gameDir : String) (gameWorkerState : WorkerState) : IO (WorkerContext × Server.FileWorker.WorkerState) := do
|
|
|
|
let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
|
|
|
|
let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
|
|
|
|
|
|
|
|
|
|
|
|
let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
|
|
|
|
let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
|
|
|
|
gameDir gameWorkerState.levelInfo.module
|
|
|
|
(gameDir := gameDir) (module := gameWorkerState.levelInfo.module)
|
|
|
|
let cancelTk ← CancelToken.new
|
|
|
|
let cancelTk ← CancelToken.new
|
|
|
|
let ctx :=
|
|
|
|
let ctx := {
|
|
|
|
{ hIn := i
|
|
|
|
hIn := i
|
|
|
|
hOut := o
|
|
|
|
hOut := o
|
|
|
|
hLog := e
|
|
|
|
hLog := e
|
|
|
|
headerTask
|
|
|
|
headerTask
|
|
|
|
initParams
|
|
|
|
initParams
|
|
|
|
clientHasWidgets
|
|
|
|
clientHasWidgets
|
|
|
|
}
|
|
|
|
}
|
|
|
|
let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
|
|
|
|
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))
|
|
|
|
| Except.error e => throw (e : ElabTaskError))
|
|
|
|
let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
|
|
|
|
let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
|
|
|
|
return (ctx,
|
|
|
|
return (ctx, {
|
|
|
|
{ doc := doc
|
|
|
|
doc := doc
|
|
|
|
initHeaderStx := headerStx
|
|
|
|
initHeaderStx := headerStx
|
|
|
|
currHeaderStx := headerStx
|
|
|
|
currHeaderStx := headerStx
|
|
|
|
importCachingTask? := none
|
|
|
|
importCachingTask? := none
|
|
|
|
pendingRequests := RBMap.empty
|
|
|
|
pendingRequests := RBMap.empty
|
|
|
|
rpcSessions := RBMap.empty
|
|
|
|
rpcSessions := RBMap.empty
|
|
|
|
})
|
|
|
|
})
|
|
|
|
|
|
|
|
|
|
|
|
end Initialization
|
|
|
|
end Initialization
|
|
|
|
|
|
|
|
|
|
|
|
section NotificationHandling
|
|
|
|
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
|
|
|
|
def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do
|
|
|
|
let docId := p.textDocument
|
|
|
|
let docId := p.textDocument
|
|
|
|
let changes := p.contentChanges
|
|
|
|
let changes := p.contentChanges
|
|
|
|
let oldDoc := (← StateT.lift get).doc
|
|
|
|
let oldDoc := (← StateT.lift get).doc -- needed a lift to our custom `WorkerM`
|
|
|
|
let some newVersion ← pure docId.version?
|
|
|
|
let newVersion := docId.version?.getD 0
|
|
|
|
| throwServerError "Expected version number"
|
|
|
|
if ¬ changes.isEmpty then
|
|
|
|
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 newDocText := foldDocumentChanges changes oldDoc.meta.text
|
|
|
|
let newDocText := foldDocumentChanges changes oldDoc.meta.text
|
|
|
|
|
|
|
|
-- modification: set the `DependencyBuildMode` from
|
|
|
|
|
|
|
|
-- `oldDoc.meta.dependencyBuildMode` to `.always`
|
|
|
|
updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
|
|
|
|
updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
|
|
|
|
|
|
|
|
|
|
|
|
end NotificationHandling
|
|
|
|
end NotificationHandling
|
|
|
|
@ -591,39 +655,34 @@ end MessageHandling
|
|
|
|
section MainLoop
|
|
|
|
section MainLoop
|
|
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
/--
|
|
|
|
Erase finished tasks if there are no errors.
|
|
|
|
The main-loop. Copied from `Lean.Server.FileWorker.mainLoop`. Use custom `WorkerM` as well
|
|
|
|
-/
|
|
|
|
as custom `handleNotification`.
|
|
|
|
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.
|
|
|
|
|
|
|
|
-/
|
|
|
|
-/
|
|
|
|
|
|
|
|
--@[inherit_doc Lean.Server.FileWorker.mainLoop]
|
|
|
|
partial def mainLoop : WorkerM Unit := do
|
|
|
|
partial def mainLoop : WorkerM Unit := do
|
|
|
|
let ctx ← read
|
|
|
|
let ctx ← read
|
|
|
|
let mut st ← StateT.lift get
|
|
|
|
let mut st ← StateT.lift get
|
|
|
|
let msg ← ctx.hIn.readLspMessage
|
|
|
|
let msg ← ctx.hIn.readLspMessage
|
|
|
|
let pendingRequests ← st.pendingRequests.foldM (fun acc id task =>
|
|
|
|
-- Erase finished tasks if there are no errors.
|
|
|
|
filterFinishedTasks acc id task) st.pendingRequests
|
|
|
|
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 }
|
|
|
|
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
|
|
|
|
for (id, seshRef) in st.rpcSessions do
|
|
|
|
let sesh ← seshRef.get
|
|
|
|
let sesh ← seshRef.get
|
|
|
|
if (← sesh.hasExpired) then
|
|
|
|
if (← sesh.hasExpired) then
|
|
|
|
st := { st with rpcSessions := st.rpcSessions.erase id }
|
|
|
|
st := { st with rpcSessions := st.rpcSessions.erase id }
|
|
|
|
|
|
|
|
|
|
|
|
set st
|
|
|
|
set st
|
|
|
|
|
|
|
|
|
|
|
|
-- Process the RPC-message and restart main-loop.
|
|
|
|
-- Process the RPC-message and restart main-loop.
|
|
|
|
match msg with
|
|
|
|
match msg with
|
|
|
|
| Message.request id "shutdown" none =>
|
|
|
|
| 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⟩
|
|
|
|
ctx.hOut.writeLspResponse ⟨id, Json.null⟩
|
|
|
|
mainLoop
|
|
|
|
mainLoop
|
|
|
|
| Message.request id method (some params) =>
|
|
|
|
| Message.request id method (some params) =>
|
|
|
|
@ -633,6 +692,7 @@ partial def mainLoop : WorkerM Unit := do
|
|
|
|
| Message.notification "exit" none =>
|
|
|
|
| Message.notification "exit" none =>
|
|
|
|
let doc := st.doc
|
|
|
|
let doc := st.doc
|
|
|
|
doc.cancelTk.set
|
|
|
|
doc.cancelTk.set
|
|
|
|
|
|
|
|
doc.cmdSnaps.cancel
|
|
|
|
return ()
|
|
|
|
return ()
|
|
|
|
| Message.notification method (some params) =>
|
|
|
|
| Message.notification method (some params) =>
|
|
|
|
-- Custom notification handler
|
|
|
|
-- Custom notification handler
|
|
|
|
@ -643,10 +703,15 @@ partial def mainLoop : WorkerM Unit := do
|
|
|
|
|
|
|
|
|
|
|
|
end MainLoop
|
|
|
|
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
|
|
|
|
def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
|
|
|
|
let i ← maybeTee "fwIn.txt" false i
|
|
|
|
let i ← maybeTee "fwIn.txt" false i
|
|
|
|
let o ← maybeTee "fwOut.txt" true o
|
|
|
|
let o ← maybeTee "fwOut.txt" true o
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-- BIG MODIFICATION
|
|
|
|
let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
|
|
|
|
let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
|
|
|
|
o.writeLspResponse {
|
|
|
|
o.writeLspResponse {
|
|
|
|
id := initRequest.id
|
|
|
|
id := initRequest.id
|
|
|
|
@ -662,16 +727,16 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
|
|
|
|
discard $ i.readLspNotificationAs "initialized" InitializedParams
|
|
|
|
discard $ i.readLspNotificationAs "initialized" InitializedParams
|
|
|
|
let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
|
|
|
|
let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let doc := param.textDocument
|
|
|
|
let doc := param.textDocument
|
|
|
|
/- NOTE(WN): `toFileMap` marks line beginnings as immediately following
|
|
|
|
-- modification: using `.always`
|
|
|
|
"\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. -/
|
|
|
|
|
|
|
|
let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
|
|
|
|
let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
|
|
|
|
let e := e.withPrefix s!"[{param.textDocument.uri}] "
|
|
|
|
let e := e.withPrefix s!"[{param.textDocument.uri}] "
|
|
|
|
let _ ← IO.setStderr e
|
|
|
|
let _ ← IO.setStderr e
|
|
|
|
try
|
|
|
|
try
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-- BIG MODIFICATION
|
|
|
|
let game ← loadGameData gameDir
|
|
|
|
let game ← loadGameData gameDir
|
|
|
|
-- TODO: We misuse the `rootUri` field to the gameName
|
|
|
|
-- TODO: We misuse the `rootUri` field to the gameName
|
|
|
|
let rootUri? : Option String := some (toString game.name)
|
|
|
|
let rootUri? : Option String := some (toString game.name)
|
|
|
|
@ -691,6 +756,8 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
|
|
|
|
-- Run the main loop
|
|
|
|
-- Run the main loop
|
|
|
|
let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
|
|
|
|
let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
|
|
|
|
StateT.run (s := gameWorkerState) <| (mainLoop)
|
|
|
|
StateT.run (s := gameWorkerState) <| (mainLoop)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
return (0 : UInt32)
|
|
|
|
return (0 : UInt32)
|
|
|
|
catch e =>
|
|
|
|
catch e =>
|
|
|
|
IO.eprintln e
|
|
|
|
IO.eprintln e
|
|
|
|
@ -703,8 +770,12 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
|
|
|
|
/--
|
|
|
|
/--
|
|
|
|
The main function. Simply wrapping `initAndRunWorker`.
|
|
|
|
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.
|
|
|
|
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
|
|
|
|
def workerMain (opts : Options) (args : List String): IO UInt32 := do
|
|
|
|
let i ← IO.getStdin
|
|
|
|
let i ← IO.getStdin
|
|
|
|
let o ← IO.getStdout
|
|
|
|
let o ← IO.getStdout
|
|
|
|
@ -712,9 +783,6 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do
|
|
|
|
try
|
|
|
|
try
|
|
|
|
let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
|
|
|
|
let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
|
|
|
|
let exitCode ← initAndRunWorker i o e opts 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
|
|
|
|
o.flush
|
|
|
|
e.flush
|
|
|
|
e.flush
|
|
|
|
IO.Process.exit exitCode.toUInt8
|
|
|
|
IO.Process.exit exitCode.toUInt8
|
|
|
|
|
Jon Eugster
12 months ago