From c3b4ed8267cb8e901cf110e7767842ee565cc144 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Feb 2015 11:52:33 -0800
Subject: [PATCH] doc(fixing_tests.md): add documentation for fixing broken
 tests

---
 doc/fixing_tests.md | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 doc/fixing_tests.md

diff --git a/doc/fixing_tests.md b/doc/fixing_tests.md
new file mode 100644
index 000000000..df3d5d4be
--- /dev/null
+++ b/doc/fixing_tests.md
@@ -0,0 +1,31 @@
+Fixing Tests
+============
+
+The test suite contains some tests that compare the produced output
+with the expected output. For example, the directory `tests/lean`
+contains files such as [`bad_class.lean`](../tests/lean/bad_class.lean) and
+[`bad_class.lean.expected.out`](../tests/lean/bad_class.lean.expected.out).
+The later contains the expected output for the test file `bad_class.lean`.
+
+When the Lean source code or the standard library are modified, some of these
+tests break because the produced output is slightly different, and we have
+to reflect the changes int the `.lean.expected.out` files.
+We should not blindly copy the new produced output since we may accidentally
+miss a bug introduced by recent changes.
+The test suite contains commands that allow us to see what changed in a convenient way.
+First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by simply executing
+
+```
+sudo apt-get install meld
+```
+
+Now, suppose `bad_class.lean` test is broken. We can see the problem by going to `test/lean` directory and
+executing
+
+```
+./test_single.sh ../../bin/lean bad_class.lean yes
+```
+
+When the `yes` 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.