From d7fe05b29d52e367a794bbd99e8045ff6aaca5b2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 15 Jan 2021 16:06:06 +0100 Subject: [PATCH] chore: script to copy .produced.out ~> .expected.out --- doc/fixing_tests.md | 18 +++++++----------- tests/lean/copy-produced | 7 +++++++ 2 files changed, 14 insertions(+), 11 deletions(-) create mode 100755 tests/lean/copy-produced diff --git a/doc/fixing_tests.md b/doc/fixing_tests.md index 0f0fd235b0..b23abf0e29 100644 --- a/doc/fixing_tests.md +++ b/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 /source/tests/lean +``` +instead where `` is the path printed out by `nix build`. diff --git a/tests/lean/copy-produced b/tests/lean/copy-produced new file mode 100755 index 0000000000..877d08f558 --- /dev/null +++ b/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