@ -5,6 +5,7 @@ import GameServer.ImportModules
import GameServer.SaveData
import GameServer.SaveData
namespace MyModule
namespace MyModule
open Lean
open Lean
open Elab
open Elab
open Parser
open Parser
@ -48,7 +49,8 @@ partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
end MyModule
end MyModule
namespace MyServer.FileWorker
namespace GameServer.FileWorker
open Lean
open Lean
open Lean.Server
open Lean.Server
open Lean.Server.FileWorker
open Lean.Server.FileWorker
@ -57,103 +59,147 @@ open IO
open Snapshots
open Snapshots
open JsonRpc
open JsonRpc
structure GameWorkerState :=
/--
Game-specific state to be packed on top of the `Lean.Server.FileWorker.WorkerState`
used by the lean server.
-/
structure WorkerState :=
/--
Collection of items which are considered unlocked.
Tactics and theorems are mixed together.
-/
inventory : Array String
inventory : Array String
/--
/--
Check for tactics/theorems that are not unlocked.
Difficulty determines whether tactics/theorems can be locked.
0: no check
* 0: do not check
1: give warnings
* 1: give warnings when locked items are used
2: give errors
* 2: give errors when locked items are used
-/
-/
difficulty : Nat
difficulty : Nat
/--
`levelInfo` contains all the (static) information about the level which is not influenced
by the user's progress.
-/
levelInfo : LevelInfo
levelInfo : LevelInfo
deriving ToJson, FromJson
deriving ToJson, FromJson
abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
/--
Pack the `GameServer.FileWorker.WorkerState` on top of the normal worker monad
`Server.FileWorker.WorkerM`.
-/
abbrev WorkerM := StateT WorkerState Server.FileWorker.WorkerM
section Elab
section Elab
/-- Add a message. use `(severity := .warning)` to specify the severity-/
def addMessage (info : SourceInfo) (inputCtx : Parser.InputContext)
(severity := MessageSeverity.warning) (s : MessageData) :
Elab.Command.CommandElabM Unit := do
modify fun st => { st with
messages := st.messages.add {
fileName := inputCtx.fileName
severity := severity
pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
data := s }}
/-- Deprecated! -/
def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
Elab.Command.CommandElabM Unit := do
Elab.Command.CommandElabM Unit := do
modify fun st => { st with
modify fun st => { st with
messages := st.messages.add {
messages := st.messages.add {
fileName := inputCtx.fileName
fileName := inputCtx.fileName
severity := MessageSeverity.error
severity := MessageSeverity.error
pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
data := s
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
/--
set `allowed` of allowed tactics. -/
Find all tactics in syntax object that are forbidden according to a
partial def findForbiddenTactics (inputCtx : Parser.InputContext)
set `allowed` of allowed tactics.
(gameWorkerState : GameWorkerState) (stx : Syntax) :
-/
Elab.Command.CommandElabM Unit := do
partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : WorkerState)
let levelInfo := gameWorkerState.levelInfo
(stx : Syntax) : Elab.Command.CommandElabM Unit := do
let levelInfo := workerState.levelInfo
-- Parse the syntax object and look for tactics and declarations.
match stx with
match stx with
| .missing => return ()
| .missing => return ()
| .node _info _kind args =>
| .node _info _kind args =>
-- Go inside a node.
for arg in args do
for arg in args do
findForbiddenTactics inputCtx gameW orkerState arg
findForbiddenTactics inputCtx w orkerState arg
| .atom info val =>
| .atom info val =>
-- ignore syntax elements that do not start with a letter
-- Atoms might be tactic names or other keywords.
-- and ignore "with" keyword
-- Note: We whitelisted known keywords because we cannot
let allowed := ["with", "fun", "at", "only", "by", "to"]
-- distinguish keywords from tactic names.
let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"]
-- Ignore syntax elements that do not start with a letter or are listed above.
if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-- Treat `simp?` and `simp!` like `simp`
let val := val.dropRightWhile (fun c => c == '!' || c == '?')
match levelInfo.tactics.find? (·.name.toString == val) with
match levelInfo.tactics.find? (·.name.toString == val) with
| none =>
| none =>
-- Note: This case means that the tactic will never be introduced in the game.
-- Tactic will never be introduced in the game.
match gameWorkerState.inventory.find? (· == val) with
match workerState.inventory.find? (· == val) with
| some _ =>
-- Tactic is in the inventory, allow it.
-- Note: This case shouldn't be possible...
pure ()
| none =>
| none =>
addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
-- Tactic is not in the inventory.
| some _ => pure () -- tactic is in the inventory, allow it.
addMessageByDifficulty info s!"The tactic '{val}' is not available in this game!"
| some tac =>
| some tac =>
if tac.locked then
-- Tactic is introduced at some point in the game.
match gameWorkerState.inventory.find? (· == val) with
if tac.disabled then
-- Tactic is disabled in this level.
addMessageByDifficulty info s!"The tactic '{val}' is disabled in this level!"
else if tac.locked then
match workerState.inventory.find? (· == val) with
| none =>
| none =>
addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
-- Tactic is marked as locked and not in the inventory.
| some _ => pure () -- tactic is in the inventory, allow it.
addMessageByDifficulty info s!"You have not unlocked the tactic '{val}' yet!"
else if tac.disabled then
| some _ =>
addWarningMessage info s!"The tactic '{val}' is disabled in this level!"
-- Tactic is in the inventory, allow it.
pure ()
| .ident info _rawVal val _preresolved =>
| .ident info _rawVal val _preresolved =>
let ns ←
-- Try to resolve the name
try resolveGlobalConst (mkIdent val)
let ns ←
catch | _ => pure [] -- catch "unknown constant" error
try resolveGlobalConst (mkIdent val)
for n in ns do
-- Catch "unknown constant" error
let some (.thmInfo ..) := (← getEnv).find? n
catch | _ => pure []
| return () -- not a theorem -> ignore
for n in ns do
let some (.thmInfo ..) := (← getEnv).find? n
-- Not a theorem, no checks needed.
| return ()
if some n = levelInfo.statementName then
-- Forbid the theorem we are proving currently
-- Forbid the theorem we are proving currently
if some n = levelInfo.statementName then
addMessage info inputCtx (severity := .error)
addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
s!"Structural recursion: you can't use '{n}' to proof itself!"
let theoremsAndDefs := levelInfo.lemmas ++ levelInfo.definitions
let lemmasAndDefs := levelInfo.lemmas ++ levelInfo.definitions
match theoremsAndDefs.find? (·.name == n) with
match lemmasAndDefs.find? (fun l => l.name == n) with
| none =>
| none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
-- Theorem will never be introduced in this game
| some lem =>
addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
if lem.locked then
| some thm =>
addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
-- Theorem is introduced at some point in the game.
else if lem.disabled then
if thm.disabled then
addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!"
-- Theorem is disabled in this level.
where addWarningMessage (info : SourceInfo) (s : MessageData) :=
addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
let difficulty := gameWorkerState.difficulty
else if thm.locked then
-- Theorem is still locked.
addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
-- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
-- deppending on difficulty.
let difficulty := workerState.difficulty
if difficulty > 0 then
if difficulty > 0 then
modify fun st => { st with
addMessage info inputCtx (if difficulty > 1 then .error else .warning) s
messages := st.messages.add {
fileName := inputCtx.fileName
severity := if difficulty > 1 then MessageSeverity.error else MessageSeverity.warning
pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
data := s
}
}
else pure ()
else pure ()
-- where addErrorMessage (info : SourceInfo) (s : MessageData) :=
-- pure ()
open Elab Meta Expr in
open Elab Meta Expr in
def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
(couldBeEndSnap : Bool) (gameWorkerState : Game WorkerState)
(couldBeEndSnap : Bool) (gameWorkerState : WorkerState)
(initParams : Lsp.InitializeParams) : IO Snapshot := do
(initParams : Lsp.InitializeParams) : IO Snapshot := do
-- Recognize end snap
-- Recognize end snap
if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
@ -287,7 +333,7 @@ where
/-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
/-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
(gameWorkerState : Game WorkerState) (initParams : Lsp.InitializeParams)
(gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams)
: AsyncElabM (Option Snapshot) := do
: AsyncElabM (Option Snapshot) := do
cancelTk.check
cancelTk.check
let s ← get
let s ← get
@ -327,7 +373,7 @@ where
/-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
/-- 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)
def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
(startAfterMs : UInt32) (gameWorkerState : Game WorkerState)
(startAfterMs : UInt32) (gameWorkerState : WorkerState)
: ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
: ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
let ctx ← read
let ctx ← read
let some headerSnap := snaps[0]? | panic! "empty snapshots"
let some headerSnap := snaps[0]? | panic! "empty snapshots"
@ -350,226 +396,254 @@ end Elab
section Updates
section Updates
/-- Given the new document, updates editable doc state. -/
/-- Given the new document, updates editable doc state. -/
def updateDocument (newMeta : DocumentMeta) : Game WorkerM Unit := dodef updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
let s ← get let s ← get
let ctx ← read let ctx ← read
let oldDoc := (← StateT.lift get).doc let oldDoc := (← StateT.lift get).doc
oldDoc.cancelTk.set oldDoc.cancelTk.set
let initHeaderStx := (← StateT.lift get).initHeaderStx let initHeaderStx := (← StateT.lift get).initHeaderStx
let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext
let cancelTk ← CancelToken.new let cancelTk ← CancelToken.new
let headSnapTask := oldDoc.cmdSnaps.waitHead? let headSnapTask := oldDoc.cmdSnaps.waitHead?
let newSnaps ← if initHeaderStx != newHeaderStx then let newSnaps ← if initHeaderStx != newHeaderStx then
EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
IO.sleep ctx.initParams.editDelay.toUInt32
IO.sleep ctx.initParams.editDelay.toUInt32
cancelTk.check
cancelTk.check
IO.Process.exit 2
IO.Process.exit 2
else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do
-- There is always at least one snapshot absent exceptions
-- There is always at least one snapshot absent exceptions
let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots"
let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots"
let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState }
let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState }
let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
-- Ignore exceptions, we are only interested in the successful snapshots
-- Ignore exceptions, we are only interested in the successful snapshots
let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
-- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
-- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
-- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
-- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
if h : validSnaps.length ≤ 1 then
if h : validSnaps.length ≤ 1 then
validSnaps := [newHeaderSnap]
validSnaps := [newHeaderSnap]
else
else
/- When at least one valid non-header snap exists, it may happen that a change does not fall
/- When at least one valid non-header snap exists, it may happen that a change does not fall
within the syntactic range of that last snap but still modifies it by appending tokens.
within the syntactic range of that last snap but still modifies it by appending tokens.
We check for this here. We do not currently handle crazy grammars in which an appended
We check for this here. We do not currently handle crazy grammars in which an appended
token can merge two or more previous commands into one. To do so would require reparsing
token can merge two or more previous commands into one. To do so would require reparsing
the entire file. -/
the entire file. -/
have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h
have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h
let mut lastSnap := validSnaps.getLast (by subst ·; simp at h)
let mut lastSnap := validSnaps.getLast (by subst ·; simp at h)
let preLastSnap :=
let preLastSnap :=
have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this
have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this
have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide)
have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide)
validSnaps[validSnaps.length - 2]
validSnaps[validSnaps.length - 2]
let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap
let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap
if newLastStx != lastSnap.stx then
if newLastStx != lastSnap.stx then
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
unfoldSnaps 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 }}
end Updates
end Updates
section Initialization
section Initialization
def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext wheredef DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
input := "" -- No header! input := "" -- No header!
fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
fileMap := default fileMap := default
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 × ×
IO (Syntax × ×
-- Determine search paths of the game project by running `lake env printenv LEAN_PATH`. -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
let out ← IO.Process.output let out ← IO.Process.output
{ cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
{ cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
if out.exitCode != 0 then if out.exitCode != 0 then
throwServerError s!"Error while running Lake: {out.stderr}"
throwServerError s!"Error while running Lake: {out.stderr}"
-- Make the paths relative to the current directory -- Make the paths relative to the current directory
let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
let currentDir ← IO.currentDir let currentDir ← IO.currentDir
let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
-- Set the search path -- Set the search path
Lean.searchPathRef.set paths Lean.searchPathRef.set paths
let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }] let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }]
-- use empty header -- use empty header
let (headerStx, headerParserState, msgLog) ← Parser.parseHeader let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
{m.mkInputContext with
{m.mkInputContext with
input := ""
input := ""
fileMap := FileMap.ofString ""}
fileMap := FileMap.ofString ""}
(headerStx, ·) <$> EIO.asTask do (headerStx, ·) <$> EIO.asTask do
let mut srcSearchPath : SearchPath := paths --← initSrcSearchPath (← getBuildDir)
let mut srcSearchPath : SearchPath := paths --← initSrcSearchPath (← getBuildDir)
let headerEnv := env
let headerEnv := env
let mut headerEnv := headerEnv
let mut headerEnv := headerEnv
try
try
if let some path := System.Uri.fileUriToPath? m.uri then
if let some path := System.Uri.fileUriToPath? m.uri then
headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
catch _ => pure ()
catch _ => pure ()
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 ({
env := headerEnv
env := headerEnv
fileMap := m.text
fileMap := m.text
ngen := { namePrefix := `_worker }
ngen := { namePrefix := `_worker }
}) (Elab.InfoTree.node
}) (Elab.InfoTree.node
(Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx })
(Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx })
(headerStx[1].getArgs.toList.map (fun importStx =>
(headerStx[1].getArgs.toList.map (fun importStx =>
Elab.InfoTree.node (Elab.Info.ofCommandInfo {
Elab.InfoTree.node (Elab.Info.ofCommandInfo {
elaborator := `import
elaborator := `import
stx := importStx
stx := importStx
}) #[].toPArray'
}) #[].toPArray'
)).toPArray'
)).toPArray'
)].toPArray'
)].toPArray'
}}
}}
let headerSnap := {
let headerSnap := {
beginPos := 0
beginPos := 0
stx := headerStx
stx := headerStx
mpState := {}
mpState := {}
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 {})
}
}
publishDiagnostics m headerSnap.diagnostics.toArray hOut
publishDiagnostics m headerSnap.diagnostics.toArray hOut
return (headerSnap, srcSearchPath)
return (headerSnap, srcSearchPath)
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 : Game WorkerState) : IO (WorkerContext ×
(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 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, _) => unfoldSnaps 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
def handleDidChange (p : DidChangeTextDocumentParams) : Game WorkerM Unit := dodef 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
let some newVersion ← pure docId.version? let some newVersion ← pure docId.version?
| throwServerError "Expected version number"
| throwServerError "Expected version number"
if newVersion ≤ oldDoc.meta.version then if newVersion ≤ oldDoc.meta.version then
-- TODO(WN): This happens on restart sometimes.
-- TODO(WN): This happens on restart sometimes.
IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
else if ¬ changes.isEmpty then else if ¬ changes.isEmpty then
let newDocText := foldDocumentChanges changes oldDoc.meta.text
let newDocText := foldDocumentChanges changes oldDoc.meta.text
updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
end NotificationHandling
end NotificationHandling
section MessageHandling
section MessageHandling
def handleNotification (method : String) (params : Json) : GameWorkerM Unit := do
let handle := fun paramType [FromJson paramType] (handler : paramType → GameWorkerM Unit) =>
/--
(StateT.lift <| parseParams paramType params) >>= handler
Modified notification handler.
match method with
| "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
Compare to `Lean.Server.FileWorker.handleNotification`.
| "$/cancelRequest" => handle CancelParams (handleCancelRequest ·)
We use the modified `WorkerM` and use our custom `handleDidChange`.
| "$/setTrace" => pure ()
| "$/lean/rpc/release" => handle RpcReleaseParams (handleRpcRelease ·)
-/
| "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
def handleNotification (method : String) (params : Json) : WorkerM Unit := do
| _ => throwServerError s!"Got unsupported notification method: {method}"
let handle := fun paramType [FromJson paramType] (handler : paramType → WorkerM Unit) =>
(StateT.lift <| parseParams paramType params) >>= handler
match method with
-- Modified `textDocument/didChange`, using a custom `handleDidChange`
| "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
-- unmodified
| "$/cancelRequest" => handle CancelParams (handleCancelRequest ·)
-- unmodified
| "$/lean/rpc/release" => handle RpcReleaseParams (handleRpcRelease ·)
-- unmodified
| "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
-- New. TODO: What is this for?
| "$/setTrace" => pure ()
| _ => throwServerError s!"Got unsupported notification method: {method}"
end MessageHandling
end MessageHandling
section MainLoop
section MainLoop
partial def mainLoop : GameWorkerM Unit := do
let ctx ← read
/--
let mut st ← StateT.lift get
Erase finished tasks if there are no errors.
let msg ← ctx.hIn.readLspMessage
-/
let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
private def filterFinishedTasks (acc : PendingRequestMap) (id : RequestID)
: IO PendingRequestMap := do
(task : Task (Except IO.Error Unit)) : IO PendingRequestMap := do
if (← hasFinished task) then
if (← hasFinished task) then
/- Handler tasks are constructed so that the only possible errors here
/- Handler tasks are constructed so that the only possible errors here
are failures of writing a response into the stream. -/
are failures of writing a response into the stream. -/
if let Except.error e := task.get then
if let Except.error e := task.get then
throwServerError s!"Failed responding to request {id}: {e}"
throwServerError s!"Failed responding to request {id}: {e}"
pure <| acc.erase id
pure <| acc.erase id
else pure acc
else pure acc
let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
st := { st with pendingRequests }
/--
The main-loop.
-- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired.
-/
for (id, seshRef) in st.rpcSessions do
partial def mainLoop : WorkerM Unit := do
let sesh ← seshRef.get
let ctx ← read
if (← sesh.hasExpired) then
let mut st ← StateT.lift get
st := { st with rpcSessions := st.rpcSessions.erase id }
let msg ← ctx.hIn.readLspMessage
let pendingRequests ← st.pendingRequests.foldM (fun acc id task =>
set st
filterFinishedTasks acc id task) st.pendingRequests
match msg with
st := { st with pendingRequests }
| Message.request id method (some params) =>
-- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired.
handleRequest id method (toJson params)
for (id, seshRef) in st.rpcSessions do
mainLoop
let sesh ← seshRef.get
| Message.notification "exit" none =>
if (← sesh.hasExpired) then
let doc := st.doc
st := { st with rpcSessions := st.rpcSessions.erase id }
doc.cancelTk.set
return ()
set st
| Message.request id "shutdown" none =>
ctx.hOut.writeLspResponse ⟨id, Json.null⟩
-- Process the RPC-message and restart main-loop.
mainLoop
match msg with
| Message.notification method (some params) =>
| Message.request id "shutdown" none =>
handleNotification method (toJson params)
ctx.hOut.writeLspResponse ⟨id, Json.null⟩
mainLoop
mainLoop
| _ => throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
| Message.request id method (some params) =>
-- Requests are handled by the unmodified lean server.
handleRequest id method (toJson params)
mainLoop
| Message.notification "exit" none =>
let doc := st.doc
doc.cancelTk.set
return ()
| Message.notification method (some params) =>
-- Custom notification handler
handleNotification method (toJson params)
mainLoop
| _ =>
throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
end MainLoop
end MainLoop
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
@ -608,12 +682,13 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
let levelInfo ← loadLevelData gameDir levelId.world levelId.level
let levelInfo ← loadLevelData gameDir levelId.world levelId.level
let some initializationOptions := initRequest.param.initializationOptions?
let some initializationOptions := initRequest.param.initializationOptions?
| throwServerError "no initialization options found"
| throwServerError "no initialization options found"
let gameWorkerState : Game WorkerState:= {
let gameWorkerState : WorkerState := {
inventory := initializationOptions.inventory
inventory := initializationOptions.inventory
difficulty := initializationOptions.difficulty
difficulty := initializationOptions.difficulty
levelInfo
levelInfo
}
}
let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState
let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState
-- 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)
@ -625,6 +700,11 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
message := e.toString }] o
message := e.toString }] o
return (1 : UInt32)
return (1 : UInt32)
/--
The main function. Simply wrapping `initAndRunWorker`.
TODO: The first arg `args[0]` is always expected to be `--server`. We could drop this completely.
-/
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
@ -632,8 +712,9 @@ 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
-- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit,
-- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code
-- 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
@ -641,4 +722,4 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do
e.putStrLn s!"worker initialization error: {err}"
e.putStrLn s!"worker initialization error: {err}"
return (1 : UInt32)
return (1 : UInt32)
end My Server.FileWorker
end Game Server.FileWorker
Jon Eugster
1 year ago