Merge main into nightly-testing

scripts/test.lean

@@ -13,14 +13,18 @@ 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.
   -- Alternatively, we could use `lake lean` below instead of `lake env lean`,
   -- 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