diff --git a/tests/lean/server/diags.lean b/tests/lean/server/diags.lean
index c8cd3c2a13..71895faf51 100644
--- a/tests/lean/server/diags.lean
+++ b/tests/lean/server/diags.lean
@@ -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)
diff --git a/tests/lean/server/edits.lean b/tests/lean/server/edits.lean
index a5bd750a6a..0b25b34232 100644
--- a/tests/lean/server/edits.lean
+++ b/tests/lean/server/edits.lean
@@ -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)
diff --git a/tests/lean/server/init_exit.lean b/tests/lean/server/init_exit.lean
index efc9d2a810..d5addb231a 100644
--- a/tests/lean/server/init_exit.lean
+++ b/tests/lean/server/init_exit.lean
@@ -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)
\ No newline at end of file
diff --git a/tests/lean/server/init_exit_worker.lean b/tests/lean/server/init_exit_worker.lean
index cb4b46ba2d..1032ffc908 100644
--- a/tests/lean/server/init_exit_worker.lean
+++ b/tests/lean/server/init_exit_worker.lean
@@ -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)
\ No newline at end of file
diff --git a/tests/lean/server/test_single.sh b/tests/lean/server/test_single.sh
index bb152166f6..d44dfb1e03 100755
--- a/tests/lean/server/test_single.sh
+++ b/tests/lean/server/test_single.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -j 0 "$f"
+exec_check lean -j 0 --run "$f"