08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
60 lines
1.8 KiB
Text
60 lines
1.8 KiB
Text
--
|
||
open IO.Process
|
||
|
||
def usingIO {α} (x : IO α) : IO α := x
|
||
|
||
#eval usingIO do
|
||
let child ← spawn { cmd := "sh", args := #["-c", "exit 1"] };
|
||
child.wait
|
||
|
||
#eval usingIO do
|
||
let child ← spawn { cmd := "sh", args := #["-c", "echo ho!"], stdout := Stdio.piped };
|
||
child.wait >>= IO.println;
|
||
child.stdout.readToEnd
|
||
|
||
#eval usingIO do
|
||
let child ← spawn { cmd := "head", args := #["-n1"], stdin := Stdio.piped, stdout := Stdio.piped };
|
||
child.stdin.putStrLn "hu!";
|
||
child.stdin.flush;
|
||
discard $ child.wait;
|
||
child.stdout.readToEnd
|
||
|
||
#eval usingIO do
|
||
-- produce enough output to fill both pipes on all platforms
|
||
let out ← output { cmd := "sh", args := #["-c", "printf '%100000s' >& 2; printf '%100001s'"] };
|
||
IO.println out.stdout.length;
|
||
IO.println out.stderr.length
|
||
|
||
#eval usingIO do
|
||
-- With a non-empty stdin, cat would wait on input forever
|
||
let child ← spawn { cmd := "sh", args := #["-c", "cat"], stdin := Stdio.null };
|
||
child.wait
|
||
|
||
#eval usingIO do
|
||
let child ← spawn { cmd := "sh", args := #["-c", "echo nullStdout"], stdout := Stdio.null };
|
||
child.wait
|
||
|
||
#eval usingIO do
|
||
let child ← spawn { cmd := "sh", args := #["-c", "echo nullStderr >& 2"], stderr := Stdio.null };
|
||
child.wait
|
||
|
||
#eval usingIO do
|
||
let lean ← IO.Process.spawn {
|
||
cmd := "lean",
|
||
args := #["--stdin"]
|
||
stdin := IO.Process.Stdio.piped
|
||
stdout := IO.Process.Stdio.piped
|
||
}
|
||
let (stdin, lean) ← lean.takeStdin
|
||
stdin.putStr "#exit\n"
|
||
let _ ← lean.wait
|
||
lean.stdout.readToEnd
|
||
|
||
#eval usingIO do
|
||
let child ← spawn { cmd := "sh", args := #["-c", "cat"], stdin := .piped, stdout := .piped }
|
||
IO.println (← child.tryWait)
|
||
-- We take stdin in here such that it is closed automatically by dropping the object right away.
|
||
-- This will kill the `cat` process.
|
||
let (stdin, child) ← child.takeStdin
|
||
IO.sleep 1000
|
||
child.tryWait
|