Skip to content

Commit

Permalink
test: unflakify test cases (#4940)
Browse files Browse the repository at this point in the history
With the recent unification of server and cmdline processing,
`IO.Process` tests that previously broke the server because they
directly wrote to stdout are now flaky on the cmdline because
elaboration and reporting are happening in separate threads. By removing
direct writes to stdout, the race condition is removed and the file can
actually be edited in the language server as well again.
  • Loading branch information
Kha authored Aug 7, 2024
1 parent 473b345 commit 1efd665
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 9 deletions.
10 changes: 4 additions & 6 deletions tests/lean/Process.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 }
Expand Down
4 changes: 1 addition & 3 deletions tests/lean/Process.lean.expected.out
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
1
hi!
0
"ho!\n"
"hu!\n"
Expand All @@ -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

0 comments on commit 1efd665

Please sign in to comment.