After building Lean you can run all the tests using
make test ARGS=-j4
Change the 4 to the maximum number of parallel tests you want to
allow. The best choice is the number of CPU cores on your machine as
the tests are mostly CPU bound. You can find the number of processors
on linux using
nproc and on Windows it is the
You can run tests after building a specific stage by
-C stageN argument. The default when run as above is stage 1. The
Lean tests will automatically use that stage's corresponding Lean
make test will not pick up new test files; run
to update the list of tests.
You can also use
ctest directly if you are in the right folder. So
to run stage1 tests with a 300 second timeout run this:
ctest -j 4 --output-on-failure --timeout 300
ctest flags are
-R <name of test> to run a single test, and
--rerun-failed to run all tests that failed during the last run.
You can also pass
ctest flags via
make test ARGS="--rerun-failed".
To get verbose output from ctest pass the
--verbose command line
option. Test output is normally suppressed and only summary
information is displayed. This option will show all test output.
All these tests are included by src/shell/CMakeLists.txt:
tests/lean: contains tests that come equipped with a .lean.expected.out file. The driver script
test_single.shruns each test and checks the actual output (*.produced.out) with the checked in expected output.
tests/lean/run: contains tests that are run through the lean command line one file at a time. These tests only look for error codes and do not check the expected output even though output is produced, it is ignored.
tests/lean/interactive: are designed to test server requests at a given position in the input file. Each .lean file contains comments that indicate how to simulate a client request at that position. using a
--^point to the line position. Example:
open Foo in theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 := Bla. --^ textDocument/completion
In this example, the test driver
test_single.shwill simulate an auto-completion request at
Bla.. The expected output is stored in a .lean.expected.out in the json format that is part of the Language Server Protocol.
This can also be used to test the following additional requests:
--^ textDocument/hover --^ textDocument/typeDefinition --^ textDocument/definition --^ $/lean/plainGoal --^ $/lean/plainTermGoal --^ insert: ... --^ collectDiagnostics
tests/lean/server: Tests more of the Lean
--serverprotocol. There are just a few of them, and it uses .log files containing JSON.
tests/compiler: contains tests that will run the Lean compiler and build an executable that is executed and the output is compared to the .lean.expected.out file. This test also contains a subfolder
foreignwhich shows how to extend Lean using C++.
tests/lean/trust0: tests that run Lean in a mode that Lean doesn't even trust the .olean files (i.e., trust 0).
tests/bench: contains performance tests.
tests/plugin: tests that compiled Lean code can be loaded into
--plugincommand line option.
Every test file should contain:
- an initial
/-! -/module docstring summarizing the test's purpose
- a module docstring for each test section that describes what is tested and, if not 100% clear, why that is the desirable behavior
At the time of writing, most tests do not follow these new guidelines yet.
For an example of a conforming test, see
When the Lean source code or the standard library are modified, some of the
tests break because the produced output is slightly different, and we have
to reflect the changes in the
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. On Ubuntu, we can do it by simply executing
sudo apt-get install meld
bad_class.lean test is broken. We can see the problem by going to
tests/lean directory and
./test_single.sh -i bad_class.lean
-i option is provided,
meld is automatically invoked
whenever there is discrepancy between the produced and expected
meld can also be used to repair the problems.
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