use full jsonrpc protocol
This commit is contained in:
Alexander Bentkamp
+2
-2
@@ -40,12 +40,12 @@
|
|||||||
},
|
},
|
||||||
"scripts": {
|
"scripts": {
|
||||||
"start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
|
"start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
|
||||||
"start_server": "cd server && NODE_ENV=development nodemon -e js,lean --exec \"(cd leanserver && lake build) && (cd testgame && lake build) && node ./index.js\"",
|
"start_server": "cd server && NODE_ENV=development nodemon -e mjs,lean --exec \"(cd leanserver && lake build) && (cd testgame && lake build) && node ./index.mjs\"",
|
||||||
"start_client": "NODE_ENV=development webpack-dev-server --hot",
|
"start_client": "NODE_ENV=development webpack-dev-server --hot",
|
||||||
"build": "npm run build_server && npm run build_client",
|
"build": "npm run build_server && npm run build_client",
|
||||||
"build_server": "server/build.sh",
|
"build_server": "server/build.sh",
|
||||||
"build_client": "NODE_ENV=production webpack",
|
"build_client": "NODE_ENV=production webpack",
|
||||||
"production": "NODE_ENV=production node server/index.js"
|
"production": "NODE_ENV=production node server/index.mjs"
|
||||||
},
|
},
|
||||||
"eslintConfig": {
|
"eslintConfig": {
|
||||||
"extends": [
|
"extends": [
|
||||||
|
|||||||
@@ -1,2 +0,0 @@
|
|||||||
import GameServer.Commands
|
|
||||||
import GameServer.Server
|
|
||||||
@@ -1,86 +0,0 @@
|
|||||||
const WebSocket = require("ws");
|
|
||||||
const express = require("express");
|
|
||||||
const app = express()
|
|
||||||
const path = require("path")
|
|
||||||
const { spawn } = require('child_process');
|
|
||||||
|
|
||||||
const PORT = process.env.PORT || 8080;
|
|
||||||
|
|
||||||
const server = app
|
|
||||||
.use(express.static(path.join(__dirname, '../client/dist/')))
|
|
||||||
.listen(PORT, () => console.log(`Listening on ${PORT}`));
|
|
||||||
|
|
||||||
const wss = new WebSocket.Server({ server })
|
|
||||||
|
|
||||||
const environment = process.env.NODE_ENV
|
|
||||||
const isDevelopment = environment === 'development'
|
|
||||||
|
|
||||||
let cmd, cmdArgs;
|
|
||||||
if (isDevelopment) {
|
|
||||||
cmd = "./leanserver/build/bin/gameserver";
|
|
||||||
cmdArgs = ["TestGame","testgame"];
|
|
||||||
} else{
|
|
||||||
cmd = "docker";
|
|
||||||
cmdArgs = ["run", "--runtime=runsc", "--network=none", "--rm", "-i", "testgame:latest"];
|
|
||||||
}
|
|
||||||
|
|
||||||
class ClientConnection {
|
|
||||||
|
|
||||||
content = Buffer.alloc(0)
|
|
||||||
|
|
||||||
constructor(ws){
|
|
||||||
console.log("Socket opened.")
|
|
||||||
this.ws = ws
|
|
||||||
|
|
||||||
this.ws.on("message", (msg) => {
|
|
||||||
console.log(msg.toString("utf8"));
|
|
||||||
this.send(JSON.parse(msg.toString("utf8")));
|
|
||||||
})
|
|
||||||
|
|
||||||
this.ws.on("close", () => {
|
|
||||||
this.lean.kill();
|
|
||||||
console.log("Socket closed.")
|
|
||||||
})
|
|
||||||
|
|
||||||
this.lean = spawn(cmd, cmdArgs);
|
|
||||||
|
|
||||||
this.lean.stdout.on('readable', () => {
|
|
||||||
this.read();
|
|
||||||
});
|
|
||||||
|
|
||||||
this.lean.stderr.on('data', (data) => {
|
|
||||||
console.error(`stderr: ${data}`);
|
|
||||||
});
|
|
||||||
}
|
|
||||||
|
|
||||||
read () {
|
|
||||||
let chr;
|
|
||||||
while (chr = this.lean.stdout.read(1)) {
|
|
||||||
this.content = Buffer.concat([this.content,chr])
|
|
||||||
if (chr.toString() == "\n") {
|
|
||||||
console.log(this.content.toString())
|
|
||||||
this.ws.send(this.content.toString());
|
|
||||||
this.content = Buffer.alloc(0)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
send(data) {
|
|
||||||
const str = JSON.stringify(data) + "\n";
|
|
||||||
const byteLength = Buffer.byteLength(str, "utf-8");
|
|
||||||
|
|
||||||
this.lean.stdin.cork();
|
|
||||||
this.lean.stdin.write(str);
|
|
||||||
this.lean.stdin.uncork();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
wss.on("connection", function(ws) { // what should a websocket do on connection
|
|
||||||
new ClientConnection(ws)
|
|
||||||
})
|
|
||||||
|
|
||||||
// server.on('upgrade', async function upgrade(request, socket, head) {
|
|
||||||
// wss.handleUpgrade(request, socket, head, function done(ws) {
|
|
||||||
// wss.emit('connection', ws, request);
|
|
||||||
// });
|
|
||||||
// });
|
|
||||||
@@ -0,0 +1,49 @@
|
|||||||
|
import { WebSocketServer } from 'ws';
|
||||||
|
import express from 'express'
|
||||||
|
import path from 'path'
|
||||||
|
import { spawn } from 'child_process';
|
||||||
|
import * as url from 'url';
|
||||||
|
import * as rpc from 'vscode-ws-jsonrpc';
|
||||||
|
import * as jsonrpcserver from 'vscode-ws-jsonrpc/server';
|
||||||
|
|
||||||
|
|
||||||
|
const __filename = url.fileURLToPath(import.meta.url);
|
||||||
|
const __dirname = url.fileURLToPath(new URL('.', import.meta.url));
|
||||||
|
|
||||||
|
const app = express()
|
||||||
|
|
||||||
|
const PORT = process.env.PORT || 8080;
|
||||||
|
|
||||||
|
const server = app
|
||||||
|
.use(express.static(path.join(__dirname, '../client/dist/')))
|
||||||
|
.listen(PORT, () => console.log(`Listening on ${PORT}`));
|
||||||
|
|
||||||
|
const wss = new WebSocketServer({ server })
|
||||||
|
|
||||||
|
const environment = process.env.NODE_ENV
|
||||||
|
const isDevelopment = environment === 'development'
|
||||||
|
|
||||||
|
let cmd, cmdArgs;
|
||||||
|
if (isDevelopment) {
|
||||||
|
cmd = "./leanserver/build/bin/gameserver";
|
||||||
|
cmdArgs = ["--server"];
|
||||||
|
} else{
|
||||||
|
cmd = "docker";
|
||||||
|
cmdArgs = ["run", "--runtime=runsc", "--network=none", "--rm", "-i", "testgame:latest"];
|
||||||
|
}
|
||||||
|
|
||||||
|
wss.addListener("connection", function(ws) {
|
||||||
|
const socket = {
|
||||||
|
onMessage: (cb) => {ws.on("message", cb)},
|
||||||
|
onError: (cb) => {ws.on("error", cb)},
|
||||||
|
onClose: (cb) => {ws.on("onclose", cb)},
|
||||||
|
send: ws.send
|
||||||
|
}
|
||||||
|
const reader = new rpc.WebSocketMessageReader(socket);
|
||||||
|
const writer = new rpc.WebSocketMessageWriter(socket);
|
||||||
|
const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
|
||||||
|
const serverConnection = jsonrpcserver.createServerProcess('Lean Server', cmd, cmdArgs);
|
||||||
|
jsonrpcserver.forward(socketConnection, serverConnection, message => {
|
||||||
|
return message;
|
||||||
|
});
|
||||||
|
})
|
||||||
+475
-21
@@ -1,30 +1,484 @@
|
|||||||
import GameServer.Server
|
import GameServer.Server
|
||||||
|
import Lean
|
||||||
|
|
||||||
|
|
||||||
|
namespace MyModule
|
||||||
|
open Lean
|
||||||
|
open Elab
|
||||||
|
open Parser
|
||||||
|
|
||||||
|
private def mkErrorMessage (c : ParserContext) (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]
|
||||||
|
|
||||||
|
partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext) (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) : Syntax × ModuleParserState × MessageLog := Id.run do
|
||||||
|
let mut pos := mps.pos
|
||||||
|
let mut recovering := mps.recovering
|
||||||
|
let mut messages := messages
|
||||||
|
let mut stx := Syntax.missing -- will always be assigned below
|
||||||
|
if inputCtx.input.atEnd pos ∧ couldBeEndSnap then
|
||||||
|
stx := mkEOI pos
|
||||||
|
return (stx, { pos, recovering }, messages)
|
||||||
|
let c := mkParserContext inputCtx pmctx
|
||||||
|
let s := { cache := initCacheForInput c.input, pos := pos : ParserState }
|
||||||
|
let s := whitespace c s
|
||||||
|
let s := (Tactic.sepByIndentSemicolon tacticParser).fn c s
|
||||||
|
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)
|
||||||
|
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)
|
||||||
|
|
||||||
|
end MyModule
|
||||||
|
|
||||||
|
namespace MyServer.FileWorker
|
||||||
|
open Lean
|
||||||
|
open Lean.Server
|
||||||
|
open Lean.Server.FileWorker
|
||||||
|
open Lsp
|
||||||
|
open IO
|
||||||
|
open Snapshots
|
||||||
|
open JsonRpc
|
||||||
|
|
||||||
|
section Elab
|
||||||
|
|
||||||
|
open Elab Meta Expr in
|
||||||
|
def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) (couldBeEndSnap : Bool) : IO Snapshot := do
|
||||||
|
let cmdState := snap.cmdState
|
||||||
|
let scope := cmdState.scopes.head!
|
||||||
|
let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
|
||||||
|
let (tacticStx, cmdParserState, msgLog) :=
|
||||||
|
MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap
|
||||||
|
let cmdPos := tacticStx.getPos?.get!
|
||||||
|
if Parser.isEOI tacticStx then
|
||||||
|
let endSnap : Snapshot := {
|
||||||
|
beginPos := cmdPos
|
||||||
|
stx := tacticStx
|
||||||
|
mpState := cmdParserState
|
||||||
|
cmdState := snap.cmdState
|
||||||
|
interactiveDiags := ← withNewInteractiveDiags msgLog
|
||||||
|
tacticCache := snap.tacticCache
|
||||||
|
}
|
||||||
|
return endSnap
|
||||||
|
else
|
||||||
|
let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog }
|
||||||
|
/- The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel` has exclusive
|
||||||
|
access to the cache, we create a fresh reference here. Before this change, the
|
||||||
|
following `snap.tacticCache.modify` would reset the tactic post cache while another snapshot was still using it. -/
|
||||||
|
let tacticCacheNew ← IO.mkRef (← snap.tacticCache.get)
|
||||||
|
let cmdCtx : Elab.Command.Context := {
|
||||||
|
cmdPos := snap.endPos
|
||||||
|
fileName := inputCtx.fileName
|
||||||
|
fileMap := inputCtx.fileMap
|
||||||
|
tacticCache? := some tacticCacheNew
|
||||||
|
}
|
||||||
|
let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get scope.opts) <| liftM (m := BaseIO) do
|
||||||
|
Elab.Command.catchExceptions
|
||||||
|
(getResetInfoTrees *> do
|
||||||
|
let level := `level1
|
||||||
|
let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[]
|
||||||
|
let tacticStx := (tacticStx.getArgs.push done).map (⟨.⟩)
|
||||||
|
let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
|
||||||
|
let cmdStx ← `(command| example : $(mkIdent level) := by {unfold $(mkIdent level); $(⟨tacticStx⟩)} )
|
||||||
|
Elab.Command.elabCommandTopLevel cmdStx)
|
||||||
|
cmdCtx cmdStateRef
|
||||||
|
let postNew := (← tacticCacheNew.get).post
|
||||||
|
snap.tacticCache.modify fun _ => { pre := postNew, post := {} }
|
||||||
|
let mut postCmdState ← cmdStateRef.get
|
||||||
|
if !output.isEmpty then
|
||||||
|
postCmdState := {
|
||||||
|
postCmdState with
|
||||||
|
messages := postCmdState.messages.add {
|
||||||
|
fileName := inputCtx.fileName
|
||||||
|
severity := MessageSeverity.information
|
||||||
|
pos := inputCtx.fileMap.toPosition snap.endPos
|
||||||
|
data := output
|
||||||
|
}
|
||||||
|
}
|
||||||
|
let postCmdSnap : Snapshot := {
|
||||||
|
beginPos := cmdPos
|
||||||
|
stx := tacticStx
|
||||||
|
mpState := cmdParserState
|
||||||
|
cmdState := postCmdState
|
||||||
|
interactiveDiags := ← withNewInteractiveDiags postCmdState.messages
|
||||||
|
tacticCache := (← IO.mkRef {})
|
||||||
|
}
|
||||||
|
return postCmdSnap
|
||||||
|
|
||||||
|
where
|
||||||
|
/-- Compute the current interactive diagnostics log by finding a "diff" relative to the parent
|
||||||
|
snapshot. We need to do this because unlike the `MessageLog` itself, interactive diags are not
|
||||||
|
part of the command state. -/
|
||||||
|
withNewInteractiveDiags (msgLog : MessageLog) : IO (PersistentArray Widget.InteractiveDiagnostic) := do
|
||||||
|
let newMsgCount := msgLog.msgs.size - snap.msgLog.msgs.size
|
||||||
|
let mut ret := snap.interactiveDiags
|
||||||
|
for i in List.iota newMsgCount do
|
||||||
|
let newMsg := msgLog.msgs.get! (msgLog.msgs.size - i)
|
||||||
|
ret := ret.push (← Widget.msgToInteractiveDiagnostic inputCtx.fileMap newMsg hasWidgets)
|
||||||
|
return ret
|
||||||
|
|
||||||
|
private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream)
|
||||||
|
(snaps : Array Snapshot) : IO Unit := do
|
||||||
|
let trees := snaps.map fun snap => snap.infoTree
|
||||||
|
let references := findModuleRefs m.text trees (localVars := true)
|
||||||
|
let param := { version := m.version, references : LeanIleanInfoParams }
|
||||||
|
hOut.writeLspNotification { method, param }
|
||||||
|
|
||||||
|
private def publishIleanInfoUpdate : DocumentMeta → FS.Stream → Array Snapshot → IO Unit :=
|
||||||
|
publishIleanInfo "$/lean/ileanInfoUpdate"
|
||||||
|
|
||||||
|
private def publishIleanInfoFinal : DocumentMeta → FS.Stream → Array Snapshot → IO Unit :=
|
||||||
|
publishIleanInfo "$/lean/ileanInfoFinal"
|
||||||
|
|
||||||
|
/-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
|
||||||
|
private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
|
||||||
|
: AsyncElabM (Option Snapshot) := do
|
||||||
|
cancelTk.check
|
||||||
|
let s ← get
|
||||||
|
let lastSnap := s.snaps.back
|
||||||
|
if lastSnap.isAtEnd then
|
||||||
|
publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
|
||||||
|
publishProgressDone m ctx.hOut
|
||||||
|
-- This will overwrite existing ilean info for the file, in case something
|
||||||
|
-- went wrong during the incremental updates.
|
||||||
|
publishIleanInfoFinal m ctx.hOut s.snaps
|
||||||
|
return none
|
||||||
|
publishProgressAtPos m lastSnap.endPos ctx.hOut
|
||||||
|
-- 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
|
||||||
|
set { s with snaps := s.snaps.push snap }
|
||||||
|
-- TODO(MH): check for interrupt with increased precision
|
||||||
|
cancelTk.check
|
||||||
|
/- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
|
||||||
|
while prefering newer versions over old ones. The former is necessary because we do
|
||||||
|
not explicitly clear older diagnostics, while the latter is necessary because we do
|
||||||
|
not guarantee that diagnostics are emitted in order. Specifically, it may happen that
|
||||||
|
we interrupted this elaboration task right at this point and a newer elaboration task
|
||||||
|
emits diagnostics, after which we emit old diagnostics because we did not yet detect
|
||||||
|
the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
|
||||||
|
because we cannot guarantee that no further diagnostics are emitted after clearing
|
||||||
|
them. -/
|
||||||
|
-- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot
|
||||||
|
-- because empty diagnostics clear existing error/information squiggles. Therefore we always
|
||||||
|
-- want to publish in case there was previously a message at this position.
|
||||||
|
publishDiagnostics m snap.diagnostics.toArray ctx.hOut
|
||||||
|
publishIleanInfoUpdate m ctx.hOut #[snap]
|
||||||
|
return some snap
|
||||||
|
|
||||||
|
/-- 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)
|
||||||
|
: ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
|
||||||
|
let ctx ← read
|
||||||
|
let headerSnap := snaps[0]!
|
||||||
|
if headerSnap.msgLog.hasErrors then
|
||||||
|
-- Treat header processing errors as fatal so users aren't swamped with
|
||||||
|
-- followup errors
|
||||||
|
publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
|
||||||
|
publishIleanInfoFinal m ctx.hOut #[headerSnap]
|
||||||
|
return AsyncList.ofList [headerSnap]
|
||||||
|
else
|
||||||
|
-- This will overwrite existing ilean info for the file since this has a
|
||||||
|
-- higher version number.
|
||||||
|
publishIleanInfoUpdate m ctx.hOut snaps
|
||||||
|
return AsyncList.ofList snaps.toList ++ (← AsyncList.unfoldAsync (nextSnap ctx m cancelTk) { snaps })
|
||||||
|
|
||||||
|
end Elab
|
||||||
|
|
||||||
|
section Updates
|
||||||
|
|
||||||
|
def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
|
||||||
|
let ctx ← read
|
||||||
|
let oldDoc := (←get).doc
|
||||||
|
-- The watchdog only restarts the file worker when the semantic content of the header changes.
|
||||||
|
-- If e.g. a newline is deleted, it will not restart this file worker, but we still
|
||||||
|
-- need to reparse the header so that the offsets are correct.
|
||||||
|
let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext
|
||||||
|
let cancelTk ← CancelToken.new
|
||||||
|
-- Wait for at least one snapshot from the old doc, we don't want to unnecessarily re-run `print-paths`
|
||||||
|
let headSnapTask := oldDoc.cmdSnaps.waitHead?
|
||||||
|
let newSnaps ← EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) fun headSnap?? => do
|
||||||
|
let headSnap? ← MonadExcept.ofExcept headSnap??
|
||||||
|
-- There is always at least one snapshot absent exceptions
|
||||||
|
let headSnap := headSnap?.get!
|
||||||
|
let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState }
|
||||||
|
oldDoc.cancelTk.set
|
||||||
|
let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
|
||||||
|
-- Ignore exceptions, we are only interested in the successful snapshots
|
||||||
|
let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
|
||||||
|
-- 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.
|
||||||
|
let mut validSnaps := cmdSnaps.takeWhile (fun s => s.endPos < changePos)
|
||||||
|
if validSnaps.length ≤ 1 then
|
||||||
|
validSnaps := [newHeaderSnap]
|
||||||
|
else
|
||||||
|
/- 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.
|
||||||
|
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
|
||||||
|
the entire file. -/
|
||||||
|
let mut lastSnap := validSnaps.getLast!
|
||||||
|
let preLastSnap := if validSnaps.length ≥ 2
|
||||||
|
then validSnaps.get! (validSnaps.length - 2)
|
||||||
|
else newHeaderSnap
|
||||||
|
let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap
|
||||||
|
if newLastStx != lastSnap.stx then
|
||||||
|
validSnaps := validSnaps.dropLast
|
||||||
|
unfoldSnaps newMeta validSnaps.toArray cancelTk ctx
|
||||||
|
modify fun st => { st with doc := ⟨newMeta, AsyncList.delayed newSnaps, cancelTk⟩ }
|
||||||
|
|
||||||
|
end Updates
|
||||||
|
|
||||||
|
section Initialization
|
||||||
|
|
||||||
|
|
||||||
|
def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
|
||||||
|
input := "" -- No header!
|
||||||
|
fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
|
||||||
|
fileMap := default
|
||||||
|
|
||||||
|
def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
|
||||||
|
: IO (Snapshot × SearchPath) := do
|
||||||
|
let (headerStx, headerParserState, msgLog) ← Parser.parseHeader m.mkInputContext
|
||||||
|
let mut srcSearchPath ← initSrcSearchPath (← getBuildDir)
|
||||||
|
searchPathRef.set [(← Lean.findSysroot) / "lib" / "lean", (← getBuildDir) / "lib"]
|
||||||
|
let lakePath ← match (← IO.getEnv "LAKE") with
|
||||||
|
| some path => pure <| System.FilePath.mk path
|
||||||
|
| none =>
|
||||||
|
let lakePath ← match (← IO.getEnv "LEAN_SYSROOT") with
|
||||||
|
| some path => pure <| System.FilePath.mk path / "bin" / "lake"
|
||||||
|
| _ => pure <| (← appDir) / "lake"
|
||||||
|
pure <| lakePath.withExtension System.FilePath.exeExtension
|
||||||
|
let (headerEnv, msgLog) ← try
|
||||||
|
if let some path := System.Uri.fileUriToPath? m.uri then
|
||||||
|
-- NOTE: we assume for now that `lakefile.lean` does not have any non-stdlib deps
|
||||||
|
-- NOTE: lake does not exist in stage 0 (yet?)
|
||||||
|
if path.fileName != "lakefile.lean" && (← System.FilePath.pathExists lakePath) then
|
||||||
|
let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx).toArray hOut
|
||||||
|
srcSearchPath ← initSrcSearchPath (← getBuildDir) pkgSearchPath
|
||||||
|
let env ← importModules [{module := `Init}, {module := `Lib}] opts 0
|
||||||
|
pure (env, msgLog)
|
||||||
|
catch e => -- should be from `lake print-paths`
|
||||||
|
let msgs := MessageLog.empty.add { fileName := "<ignored>", pos := ⟨0, 0⟩, data := e.toString }
|
||||||
|
pure (← mkEmptyEnvironment, msgs)
|
||||||
|
let mut headerEnv := headerEnv
|
||||||
|
try
|
||||||
|
if let some path := System.Uri.fileUriToPath? m.uri then
|
||||||
|
headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
|
||||||
|
catch _ => pure ()
|
||||||
|
let cmdState := Elab.Command.mkState headerEnv msgLog opts
|
||||||
|
let cmdState := { cmdState with infoState := {
|
||||||
|
enabled := true
|
||||||
|
trees := #[Elab.InfoTree.context ({
|
||||||
|
env := headerEnv
|
||||||
|
fileMap := m.text
|
||||||
|
ngen := { namePrefix := `_worker }
|
||||||
|
}) (Elab.InfoTree.node
|
||||||
|
(Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx })
|
||||||
|
(headerStx[1].getArgs.toList.map (fun importStx =>
|
||||||
|
Elab.InfoTree.node (Elab.Info.ofCommandInfo {
|
||||||
|
elaborator := `import
|
||||||
|
stx := importStx
|
||||||
|
}) #[].toPArray'
|
||||||
|
)).toPArray'
|
||||||
|
)].toPArray'
|
||||||
|
}}
|
||||||
|
let headerSnap := {
|
||||||
|
beginPos := 0
|
||||||
|
stx := headerStx
|
||||||
|
mpState := headerParserState
|
||||||
|
cmdState := cmdState
|
||||||
|
interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
|
||||||
|
tacticCache := (← IO.mkRef {})
|
||||||
|
}
|
||||||
|
publishDiagnostics m headerSnap.diagnostics.toArray hOut
|
||||||
|
return (headerSnap, srcSearchPath)
|
||||||
|
|
||||||
|
|
||||||
|
def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
|
||||||
|
: IO (WorkerContext × WorkerState) := do
|
||||||
|
let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
|
||||||
|
let headerTask ← EIO.asTask $ compileHeader meta o opts (hasWidgets := clientHasWidgets)
|
||||||
|
let cancelTk ← CancelToken.new
|
||||||
|
let ctx :=
|
||||||
|
{ hIn := i
|
||||||
|
hOut := o
|
||||||
|
hLog := e
|
||||||
|
headerTask
|
||||||
|
initParams
|
||||||
|
clientHasWidgets
|
||||||
|
}
|
||||||
|
let snaps ← EIO.mapTask (t := headerTask) (match · with
|
||||||
|
| Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk ctx
|
||||||
|
| Except.error e => throw (e : ElabTaskError))
|
||||||
|
let doc : EditableDocument := ⟨meta, AsyncList.delayed snaps, cancelTk⟩
|
||||||
|
return (ctx,
|
||||||
|
{ doc := doc
|
||||||
|
pendingRequests := RBMap.empty
|
||||||
|
rpcSessions := RBMap.empty
|
||||||
|
})
|
||||||
|
|
||||||
|
end Initialization
|
||||||
|
|
||||||
|
section NotificationHandling
|
||||||
|
|
||||||
|
def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do
|
||||||
|
let docId := p.textDocument
|
||||||
|
let changes := p.contentChanges
|
||||||
|
let oldDoc := (←get).doc
|
||||||
|
let some newVersion ← pure docId.version?
|
||||||
|
| throwServerError "Expected version number"
|
||||||
|
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
|
||||||
|
updateDocument ⟨docId.uri, newVersion, newDocText⟩
|
||||||
|
|
||||||
|
end NotificationHandling
|
||||||
|
|
||||||
|
section MessageHandling
|
||||||
|
|
||||||
|
def handleNotification (method : String) (params : Json) : WorkerM Unit := do
|
||||||
|
let handle := fun paramType [FromJson paramType] (handler : paramType → WorkerM Unit) =>
|
||||||
|
parseParams paramType params >>= handler
|
||||||
|
match method with
|
||||||
|
| "textDocument/didChange" => handle DidChangeTextDocumentParams handleDidChange
|
||||||
|
| "$/cancelRequest" => handle CancelParams handleCancelRequest
|
||||||
|
| "$/lean/rpc/release" => handle RpcReleaseParams handleRpcRelease
|
||||||
|
| "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams handleRpcKeepAlive
|
||||||
|
| _ => throwServerError s!"Got unsupported notification method: {method}"
|
||||||
|
|
||||||
|
end MessageHandling
|
||||||
|
|
||||||
|
section MainLoop
|
||||||
|
partial def mainLoop : WorkerM Unit := do
|
||||||
|
let ctx ← read
|
||||||
|
let mut st ← get
|
||||||
|
let msg ← ctx.hIn.readLspMessage
|
||||||
|
let 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
|
||||||
|
let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.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
|
||||||
|
let sesh ← seshRef.get
|
||||||
|
if (← sesh.hasExpired) then
|
||||||
|
st := { st with rpcSessions := st.rpcSessions.erase id }
|
||||||
|
|
||||||
|
set st
|
||||||
|
match msg with
|
||||||
|
| Message.request id method (some params) =>
|
||||||
|
handleRequest id method (toJson params)
|
||||||
|
mainLoop
|
||||||
|
| Message.notification "exit" none =>
|
||||||
|
let doc := st.doc
|
||||||
|
doc.cancelTk.set
|
||||||
|
return ()
|
||||||
|
| Message.notification method (some params) =>
|
||||||
|
handleNotification method (toJson params)
|
||||||
|
mainLoop
|
||||||
|
| _ => throwServerError "Got invalid JSON-RPC message"
|
||||||
|
end MainLoop
|
||||||
|
|
||||||
|
def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
|
||||||
|
let i ← maybeTee "fwIn.txt" false i
|
||||||
|
let o ← maybeTee "fwOut.txt" true o
|
||||||
|
let initParams ← i.readLspRequestAs "initialize" InitializeParams
|
||||||
|
let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
|
||||||
|
let doc := param.textDocument
|
||||||
|
/- NOTE(WN): `toFileMap` marks line beginnings as immediately following
|
||||||
|
"\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⟩
|
||||||
|
let e := e.withPrefix s!"[{param.textDocument.uri}] "
|
||||||
|
let _ ← IO.setStderr e
|
||||||
|
try
|
||||||
|
let (ctx, st) ← initializeWorker meta i o e initParams.param opts
|
||||||
|
let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) mainLoop
|
||||||
|
return (0 : UInt32)
|
||||||
|
catch e =>
|
||||||
|
IO.eprintln e
|
||||||
|
publishDiagnostics meta #[{ range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, severity? := DiagnosticSeverity.error, message := e.toString }] o
|
||||||
|
return (1 : UInt32)
|
||||||
|
|
||||||
|
def workerMain (opts : Options) : IO UInt32 := do
|
||||||
|
let i ← IO.getStdin
|
||||||
|
let o ← IO.getStdout
|
||||||
|
let e ← IO.getStderr
|
||||||
|
try
|
||||||
|
let exitCode ← initAndRunWorker i o e opts
|
||||||
|
-- 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
|
||||||
|
e.flush
|
||||||
|
IO.Process.exit exitCode.toUInt8
|
||||||
|
catch err =>
|
||||||
|
e.putStrLn s!"worker initialization error: {err}"
|
||||||
|
return (1 : UInt32)
|
||||||
|
|
||||||
|
end MyServer.FileWorker
|
||||||
|
|
||||||
|
def main : List String → IO UInt32 := fun args => do
|
||||||
|
let e ← IO.getStderr
|
||||||
|
if args[0]? == some "--server" then
|
||||||
|
Lean.Server.Watchdog.watchdogMain []
|
||||||
|
else if args[0]? == some "--worker" then
|
||||||
|
MyServer.FileWorker.workerMain {}
|
||||||
|
else
|
||||||
|
e.putStrLn s!"Expected `--server` or `--worker`"
|
||||||
|
return 1
|
||||||
|
|
||||||
|
|
||||||
-- TODO: Potentially it could be useful to pass in the `gameName` via the websocket connection
|
-- TODO: Potentially it could be useful to pass in the `gameName` via the websocket connection
|
||||||
|
|
||||||
unsafe def main (args : List String) : IO Unit := do
|
-- unsafe def main (args : List String) : IO UInt32 := do
|
||||||
|
|
||||||
-- Check if required arguments are given by the user
|
|
||||||
if args.length != 2 then
|
|
||||||
throw (IO.userError $ "Expected two arguments:" ++
|
|
||||||
"The name of the game module and the path to the game project.")
|
|
||||||
let gameName := args[0]!
|
|
||||||
let gameDir := args[1]!
|
|
||||||
|
|
||||||
-- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
|
-- -- Check if required arguments are given by the user
|
||||||
let out ← IO.Process.output
|
-- if args.length != 2 then
|
||||||
{ cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
|
-- throw (IO.userError $ "Expected two arguments:" ++
|
||||||
if out.exitCode != 0 then
|
-- "The name of the game module and the path to the game project.")
|
||||||
IO.eprintln out.stderr
|
-- let gameName := args[0]!
|
||||||
return
|
-- let gameDir := args[1]!
|
||||||
|
|
||||||
-- Make the paths relative to the current directory
|
-- -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
|
||||||
let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
|
-- let out ← IO.Process.output
|
||||||
let currentDir ← IO.currentDir
|
-- { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
|
||||||
let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
|
-- if out.exitCode != 0 then
|
||||||
|
-- IO.eprintln out.stderr
|
||||||
|
-- return
|
||||||
|
|
||||||
-- Set the search path
|
-- -- Make the paths relative to the current directory
|
||||||
Lean.searchPathRef.set paths
|
-- let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
|
||||||
|
-- let currentDir ← IO.currentDir
|
||||||
|
-- let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
|
||||||
|
|
||||||
-- Run the game
|
-- -- Set the search path
|
||||||
Server.runGame gameName
|
-- Lean.searchPathRef.set paths
|
||||||
|
|
||||||
|
-- -- Run the game
|
||||||
|
-- Server.runGame gameName
|
||||||
|
|||||||
@@ -5,7 +5,7 @@ package GameServer
|
|||||||
|
|
||||||
lean_lib GameServer
|
lean_lib GameServer
|
||||||
|
|
||||||
@[defaultTarget]
|
@[default_target]
|
||||||
lean_exe gameserver {
|
lean_exe gameserver {
|
||||||
root := `Main
|
root := `Main
|
||||||
supportInterpreter := true
|
supportInterpreter := true
|
||||||
|
|||||||
@@ -1 +1 @@
|
|||||||
leanprover/lean4:nightly-2022-09-23
|
leanprover/lean4:nightly-2022-10-29
|
||||||
|
|||||||
@@ -63,12 +63,13 @@ Start by casting `induction_on n`.
|
|||||||
"
|
"
|
||||||
|
|
||||||
Statement (n : ℕ) : 0 + n = n := by
|
Statement (n : ℕ) : 0 + n = n := by
|
||||||
induction_on n
|
sorry
|
||||||
rewrite [add_zero]
|
-- induction_on n
|
||||||
rfl
|
-- rewrite [add_zero]
|
||||||
rewrite [add_succ]
|
-- rfl
|
||||||
rewrite [ind_hyp]
|
-- rewrite [add_succ]
|
||||||
rfl
|
-- rewrite [ind_hyp]
|
||||||
|
-- rfl
|
||||||
|
|
||||||
Message : (0 : ℕ) + 0 = 0 => "
|
Message : (0 : ℕ) + 0 = 0 => "
|
||||||
We now have *two goals!* The
|
We now have *two goals!* The
|
||||||
|
|||||||
@@ -16,5 +16,5 @@ axiom add_zero : ∀ a : ℕ, a + 0 = a
|
|||||||
|
|
||||||
axiom add_succ : ∀ a b : ℕ, a + succ b = succ (a + b)
|
axiom add_succ : ∀ a b : ℕ, a + succ b = succ (a + b)
|
||||||
|
|
||||||
@[elabAsElim] axiom myInduction {P : ℕ → Prop} (n : ℕ) (h₀ : P 0) (h : ∀ n, P n → P (succ n)) : P n
|
@[elab_as_elim] axiom myInduction {P : ℕ → Prop} (n : ℕ) (h₀ : P 0) (h : ∀ n, P n → P (succ n)) : P n
|
||||||
|
|
||||||
|
|||||||
@@ -8,5 +8,5 @@ elab "swap" : tactic => do
|
|||||||
| g₁::g₂::t => setGoals (g₂::g₁::t)
|
| g₁::g₂::t => setGoals (g₂::g₁::t)
|
||||||
| _ => pure ()
|
| _ => pure ()
|
||||||
|
|
||||||
macro "induction_on" n:ident : tactic =>
|
-- macro "induction_on" n:ident : tactic =>
|
||||||
`(tactic| refine myInduction $n ?base ?inductive_step; swap; clear $n; intro $n $(mkIdent `ind_hyp); swap)
|
-- `(tactic| refine myInduction $n ?base ?inductive_step; swap; clear $n; intro $n $(mkIdent `ind_hyp); swap)
|
||||||
@@ -5,5 +5,5 @@ require GameServer from ".."/"leanserver"
|
|||||||
|
|
||||||
package TestGame
|
package TestGame
|
||||||
|
|
||||||
@[defaultTarget]
|
@[default_target]
|
||||||
lean_lib TestGame
|
lean_lib TestGame
|
||||||
|
|||||||
@@ -1 +1 @@
|
|||||||
leanprover/lean4:nightly-2022-09-23
|
leanprover/lean4:nightly-2022-10-29
|
||||||
|
|||||||
Reference in New Issue
Block a user