diff --git a/scripts/test.lean b/scripts/test.lean index 980729db03..43df619246 100644 --- a/scripts/test.lean +++ b/scripts/test.lean @@ -13,6 +13,9 @@ If no arguments are provided, run everything in the `test/` directory. If arguments are provided, assume they are names of files in the `test/` directory, and just run those. + +Requires not only that tests succeed, but that they produce no output on stdout or stderr. +The flag `--allow-noisy` can be used to allow tests to produce output. -/ def main (args : List String) : IO Unit := do -- We first run `lake build`, to ensure oleans are available. @@ -20,7 +23,8 @@ def main (args : List String) : IO Unit := do -- but currently with parallelism this results in build jobs interfering with each other. _ ← (← IO.Process.spawn { cmd := "lake", args := #["build"] }).wait -- Collect test targets, either from the command line or by walking the `test/` directory. - let targets ← match args with + let allowNoisy := args.contains "--allow-noisy" + let targets ← match args.erase "--allow-noisy" with | [] => System.FilePath.walkDir "./test" | _ => pure <| (args.map fun t => mkFilePath [".", "test", t] |>.withExtension "lean") |>.toArray let existing ← targets.filterM fun t => do pure <| (← t.pathExists) && !(← t.isDir) @@ -31,13 +35,18 @@ def main (args : List String) : IO Unit := do { cmd := "lake", args := #["env", "lean", t.toString], env := #[("LEAN_ABORT_ON_PANIC", "1")] } - if out.exitCode = 0 then - IO.println s!"Test succeeded: {t}" + let mut exitCode := out.exitCode + if exitCode = 0 then + if out.stdout.isEmpty && out.stderr.isEmpty then + IO.println s!"Test succeeded: {t}" + else + IO.println s!"Test succeeded with noisy output: {t}" + unless allowNoisy do exitCode := 1 else IO.eprintln s!"Test failed: `lake env lean {t}` produced:" - unless out.stdout.isEmpty do IO.eprintln out.stdout - unless out.stderr.isEmpty do IO.eprintln out.stderr - pure out.exitCode + unless out.stdout.isEmpty do IO.eprintln out.stdout + unless out.stderr.isEmpty do IO.eprintln out.stderr + pure exitCode -- Wait on all the jobs and exit with 1 if any failed. let mut exitCode : UInt8 := 0 for t in tasks do