update lean

4 years ago · f4508d81af
parent eda5357723
commit f4508d81af
7 changed files with 95 additions and 62 deletions
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@ -9,11 +9,10 @@ open Lean
 open Elab
 open Parser

-private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message :=
+private def mkErrorMessage (c : InputContext) (pos : String.Pos) (errorMsg : String) : Message :=
  let pos := c.fileMap.toPosition pos
  { fileName := c.fileName, pos := pos, data := errorMsg }

-open Parser in
 private def mkEOI (pos : String.Pos) : Syntax :=
  let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring pos) ""
  mkNode `Lean.Parser.Module.eoi #[atom]
@ -28,23 +27,27 @@ partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
  if inputCtx.input.atEnd pos ∧ couldBeEndSnap then
    stx := mkEOI pos
    return (stx, { pos, recovering }, messages, 0)
-  let c := mkParserContext inputCtx pmctx
-  let s := { cache := initCacheForInput c.input, pos := pos : ParserState }
-  let s := whitespace c s
+
+  let tokens := getTokenTable pmctx.env
+
+  let s   := whitespace.run inputCtx pmctx tokens { cache := initCacheForInput inputCtx.input, pos }
  let endOfWhitespace := s.pos
-  let s := (Tactic.sepByIndentSemicolon tacticParser).fn c s
+
+  let p   :=  (Tactic.sepByIndentSemicolon tacticParser).fn
+  let s   := p.run inputCtx pmctx tokens { cache := initCacheForInput inputCtx.input, pos }
+
  pos := s.pos
  match s.errorMsg with
  | none =>
    stx := s.stxStack.back
    recovering := false
  | some errorMsg =>
-    messages := messages.add <| mkErrorMessage c s.pos (toString errorMsg)
+    messages := messages.add <|  mkErrorMessage inputCtx s.pos (toString errorMsg)
    recovering := true
    stx := s.stxStack.back
-    if ¬ c.input.atEnd s.pos then
-      messages := messages.add <| mkErrorMessage c s.pos "end of input"
-  return (stx, { pos := c.input.endPos, recovering }, messages, endOfWhitespace)
+    if ¬ inputCtx.input.atEnd s.pos then
+      messages := messages.add <|  mkErrorMessage inputCtx s.pos "end of input"
+  return (stx, { pos := inputCtx.input.endPos, recovering }, messages, endOfWhitespace)

 end MyModule

@ -329,10 +332,11 @@ section Initialization
      | Except.error e   => throw (e : ElabTaskError))
    let doc : EditableDocument := ⟨meta, AsyncList.delayed snaps, cancelTk⟩
    return (ctx,
-    { doc             := doc
-      pendingRequests := RBMap.empty
-      rpcSessions     := RBMap.empty
-    })
+        { doc             := doc
+          initHeaderStx   := Syntax.missing
+          pendingRequests := RBMap.empty
+          rpcSessions     := RBMap.empty
+        })

 end Initialization

--- a/server/leanserver/GameServer/Watchdog.lean
+++ b/server/leanserver/GameServer/Watchdog.lean
@ -18,12 +18,10 @@ open System.Uri
    for (_, fw) in workers do
      if let WorkerState.running := fw.state then
        workerTasks := workerTasks.push <| fw.commTask.map (ServerEvent.workerEvent fw)
-        if let some ge ← fw.groupedEditsRef.get then
-          workerTasks := workerTasks.push <| ge.signalTask.map (ServerEvent.workerEvent fw)

    let ev ← IO.waitAny (clientTask :: workerTasks.toList)

-    if ← Game.handleServerEvent ev then
+    if ← Game.handleServerEvent ev then -- handle Game requests
      mainLoop (←runClientTask)
    else
      match ev with
@ -35,60 +33,28 @@ open System.Uri
        | Message.request id method (some params) =>
          handleRequest id method (toJson params)
          mainLoop (←runClientTask)
-        | Message.notification "textDocument/didChange" (some params) =>
-          let p ← parseParams DidChangeTextDocumentParams (toJson params)
-          let fw ← findFileWorker! p.textDocument.uri
-          let now ← monoMsNow
-          /- We wait `editDelay`ms since last edit before applying the changes. -/
-          let applyTime := now + st.editDelay
-          let queuedMsgs? ← fw.groupedEditsRef.modifyGet fun
-            | some ge => (some ge.queuedMsgs, some { ge with
-              applyTime := applyTime
-              params.textDocument := p.textDocument
-              params.contentChanges := ge.params.contentChanges ++ p.contentChanges
-              -- drain now-outdated messages and respond with `contentModified` below
-              queuedMsgs := #[] })
-            | none    => (none, some {
-              applyTime := applyTime
-              params := p
-              /- This is overwritten just below. -/
-              signalTask := Task.pure WorkerEvent.processGroupedEdits
-              queuedMsgs := #[] })
-          match queuedMsgs? with
-          | some queuedMsgs =>
-            for msg in queuedMsgs do
-              match msg with
-              | JsonRpc.Message.request id _ _ =>
-                fw.erasePendingRequest id
-                (← read).hOut.writeLspResponseError {
-                  id := id
-                  code := ErrorCode.contentModified
-                  message := "File changed."
-                }
-              | _ => pure () -- notifications do not need to be cancelled
-          | _ =>
-            let t ← fw.runEditsSignalTask
-            fw.groupedEditsRef.modify (Option.map fun ge => { ge with signalTask := t } )
+        | Message.response .. =>
+          -- TODO: handle client responses
          mainLoop (←runClientTask)
+        | Message.responseError _ _ e .. =>
+          throwServerError s!"Unhandled response error: {e}"
        | Message.notification method (some params) =>
          handleNotification method (toJson params)
          mainLoop (←runClientTask)
-        | Message.response "register_ilean_watcher" _      =>
-          mainLoop (←runClientTask)
        | _ => throwServerError "Got invalid JSON-RPC message"
      | ServerEvent.clientError e => throw e
      | ServerEvent.workerEvent fw ev =>
        match ev with
-        | WorkerEvent.processGroupedEdits =>
-          handleEdits fw
-          mainLoop clientTask
        | WorkerEvent.ioError e =>
-          throwServerError s!"IO error while processing events for {fw.doc.meta.uri}: {e}"
+          throwServerError s!"IO error while processing events for {fw.doc.uri}: {e}"
        | WorkerEvent.crashed _ =>
-          handleCrash fw.doc.meta.uri #[]
+          handleCrash fw.doc.uri #[]
          mainLoop clientTask
        | WorkerEvent.terminated =>
          throwServerError "Internal server error: got termination event for worker that should have been removed"
+        | .importsChanged =>
+          startFileWorker fw.doc
+          mainLoop clientTask

 def initAndRunWatchdogAux : GameServerM Unit := do
  let st ← read
@ -156,7 +122,6 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
    args           := args
    fileWorkersRef := fileWorkersRef
    initParams     := initRequest.param
-    editDelay      := initRequest.param.initializationOptions? |>.bind InitializationOptions.editDelay? |>.getD 200
    workerPath
    srcSearchPath
    references
--- a/server/leanserver/lean-toolchain
+++ b/server/leanserver/lean-toolchain
@ -1 +1 @@
-leanprover/lean4:nightly-2022-10-29
+leanprover/lean4:nightly-2022-12-03
--- a/server/testgame/gameserver
+++ b/server/testgame/gameserver
--- a/server/testgame/lake-manifest.json
+++ b/server/testgame/lake-manifest.json
@ -0,0 +1,64 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/xubaiw/CMark.lean",
+    "subDir?": null,
+    "rev": "2cc7cdeef67184f84db6731450e4c2b258c28fe8",
+    "name": "CMark",
+    "inputRev?": "main"}},
+  {"git":
+   {"url": "https://github.com/leanprover/lake",
+    "subDir?": null,
+    "rev": "235383015cdcb0082777b0347b84dba01843c79c",
+    "name": "lake",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/leanprover/doc-gen4",
+    "subDir?": null,
+    "rev": "7009910876145a9a1220359f968ba7045dd05290",
+    "name": "doc-gen4",
+    "inputRev?": "main"}},
+  {"git":
+   {"url": "https://github.com/mhuisi/lean4-cli",
+    "subDir?": null,
+    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "name": "Cli",
+    "inputRev?": "nightly"}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "9b15aa6f091a623f992d6fff76167864794ce350",
+    "name": "mathlib",
+    "inputRev?": "9b15aa6f091a623f992d6fff76167864794ce350"}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf",
+    "name": "Qq",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "70c59fcfc63de90786d59222c32468dab87964c5",
+    "name": "aesop",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/hargonix/LeanInk",
+    "subDir?": null,
+    "rev": "9f3101452135964ac9107ec8e9910bfd14022bbc",
+    "name": "leanInk",
+    "inputRev?": "doc-gen"}},
+  {"path": {"name": "GameServer", "dir": "./../leanserver"}},
+  {"git":
+   {"url": "https://github.com/xubaiw/Unicode.lean",
+    "subDir?": null,
+    "rev": "6dd6ae3a3839c8350a91876b090eda85cf538d1d",
+    "name": "Unicode",
+    "inputRev?": "main"}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "42bb39d34ec7dcb07580458efa4a7936bd5192b7",
+    "name": "std",
+    "inputRev?": "main"}}]}
--- a/server/testgame/lakefile.lean
+++ b/server/testgame/lakefile.lean
@ -4,7 +4,7 @@ open Lake DSL
 require GameServer from ".."/"leanserver"

 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"@"b1cf06cb126ee163a7dc895c1aee17946ff20900"
+  "https://github.com/leanprover-community/mathlib4.git"@"9b15aa6f091a623f992d6fff76167864794ce350"

 package TestGame

--- a/server/testgame/lean-toolchain
+++ b/server/testgame/lean-toolchain
@ -1 +1 @@
-leanprover/lean4:nightly-2022-10-29
+leanprover/lean4:nightly-2022-12-03