chore: use --run for servertests

/cc @Garmelon
This commit is contained in:
Sebastian Ullrich 2021-12-21 16:03:55 +01:00
parent cbdad10419
commit 5b653197db
5 changed files with 6 additions and 9 deletions

View file

@ -1,7 +1,7 @@
import Lean.Data.Lsp
open IO Lean Lsp
#eval (do
def main : IO Unit := do
Ipc.runWith (←IO.appPath) #["--server"] do
let hIn ← Ipc.stdin
hIn.write (←FS.readBinFile "init_vscode_1_47_2.log")
@ -30,4 +30,3 @@ open IO Lean Lsp
assert! shutResp.result.isNull
Ipc.writeNotification ⟨"exit", Json.null⟩
discard $ Ipc.waitForExit
: IO Unit)

View file

@ -1,8 +1,9 @@
import Lean.Data.Lsp
open IO Lean Lsp
def main : IO Unit := do
pure ()
#exit
#eval (do
Ipc.runWith (←IO.appPath) #["--server"] do
let hIn ← Ipc.stdin
hIn.write (←FS.readBinFile "init_vscode_1_47_2.log")
@ -36,4 +37,3 @@ open IO Lean Lsp
assert! shutResp.result.isNull
Ipc.writeNotification ⟨"exit", Json.null⟩
discard $ Ipc.waitForExit
: IO Unit)

View file

@ -1,7 +1,7 @@
import Lean.Data.Lsp
open IO Lean Lsp
#eval (do
def main : IO Unit := do
Ipc.runWith (←IO.appPath) #["--server"] do
let hIn ← Ipc.stdin
hIn.write (←FS.readBinFile "init_vscode_1_47_2.log")
@ -14,4 +14,3 @@ open IO Lean Lsp
assert! shutdownResp.result.isNull
Ipc.writeNotification ⟨"exit", Json.null⟩
discard Ipc.waitForExit
: IO Unit)

View file

@ -1,7 +1,7 @@
import Lean.Data.Lsp
open IO Lean Lsp
#eval (do
def main : IO Unit := do
Ipc.runWith (←IO.appPath) #["--worker"] do
let hIn ← Ipc.stdin
hIn.write (←FS.readBinFile "init_vscode_1_47_2.log")
@ -14,4 +14,3 @@ open IO Lean Lsp
Ipc.writeNotification ⟨"exit", Json.null⟩
discard Ipc.waitForExit
: IO Unit)

View file

@ -1,4 +1,4 @@
#!/usr/bin/env bash
source ../../common.sh
exec_check lean -j 0 "$f"
exec_check lean -j 0 --run "$f"