chore: script to copy .produced.out ~> .expected.out

doc/fixing_tests.md

@@ -30,14 +30,10 @@ When the `-i` option is provided, `meld` is automatically invoked
 whenever there is discrepancy between the produced and expected
 outputs. `meld` can also be used to repair the problems.
 
-In Emacs, we can also execute `M-x lean-diff-test-file` to check/diff the file of the current buffer.
-
-Here is the list of directories where produced output is compared with
-the expected output (stored in a `*.expected.out` file).
-
-- [`tests/lean`](../tests/lean)
-- [`tests/lean/interactive`](../tests/lean/interactive)
-
-Remark: in the directory `tests/lean/interactive`, the input test files have extension `.input`.
-They simulate commands sent from editors to Lean.
-The `.lean` files in this directory are used to simulate files opened by the user.
+In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer.
+To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`.
+When using the Nix setup, add `--keep-failed` to the `nix build` call and then call
+```sh
+tests/lean/copy-produced <build-dir>/source/tests/lean
+```
+instead where `<build-dir>` is the path printed out by `nix build`.

tests/lean/copy-produced

@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+
+root="$(realpath $(dirname $0))"
+cd ${1:-$PWD}
+for f in *.produced.out; do
+    cp $f "$root/${f/produced/expected}"
+done