test: remove flaky test case

leanprover · Aug 7, 2024 · 1152148 · 1152148
1 parent 574066b
commit 1152148
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 9 deletions.
diff --git a/tests/lean/Process.lean b/tests/lean/Process.lean
@@ -7,13 +7,9 @@ def usingIO {α} (x : IO α) : IO α := x
   let child ← spawn { cmd := "sh", args := #["-c", "exit 1"] };
   child.wait
 
-#eval usingIO do
-  let child ← spawn { cmd := "sh", args := #["-c", "echo hi!"] };
-  child.wait
-
 #eval usingIO do
   let child ← spawn { cmd := "sh", args := #["-c", "echo ho!"], stdout := Stdio.piped };
-  discard $ child.wait;
+  child.wait >>= IO.println;
   child.stdout.readToEnd
 
 #eval usingIO do
@@ -53,10 +49,12 @@ def usingIO {α} (x : IO α) : IO α := x
     cmd := "lean",
     args := #["--stdin"]
     stdin := IO.Process.Stdio.piped
+    stdout := IO.Process.Stdio.piped
   }
   let (stdin, lean) ← lean.takeStdin
   stdin.putStr "#exit\n"
-  lean.wait
+  let _ ← lean.wait
+  lean.stdout.readToEnd
 
 #eval usingIO do
   let child ← spawn { cmd := "sh", args := #["-c", "cat"], stdin := .piped, stdout := .piped }

diff --git a/tests/lean/Process.lean.expected.out b/tests/lean/Process.lean.expected.out
@@ -1,5 +1,4 @@
 1
-hi!
 0
 "ho!\n"
 "hu!\n"
@@ -8,8 +7,7 @@ flush of broken pipe failed
 100000
 0
 0
-<stdin>:1:0: warning: using 'exit' to interrupt Lean
-0
 0
+"<stdin>:1:0: warning: using 'exit' to interrupt Lean\n"
 none
 some 0