From 1152148026019779753eb8c790c64569f34bf456 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 7 Aug 2024 10:02:27 +0200 Subject: [PATCH] test: remove flaky test case --- tests/lean/Process.lean | 10 ++++------ tests/lean/Process.lean.expected.out | 4 +--- 2 files changed, 5 insertions(+), 9 deletions(-) diff --git a/tests/lean/Process.lean b/tests/lean/Process.lean index b2107c2c4782..147917c8a9e6 100644 --- 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 index 5d186fa1f4e6..aefb784c4ed2 100644 --- 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 -:1:0: warning: using 'exit' to interrupt Lean -0 0 +":1:0: warning: using 'exit' to interrupt Lean\n" none some 0