Setting up linting and testing for your Lean project

This guide explains how to add a linting step and a testing step to your Lean project, to help you maintain your code in good shape. Doing so will enable the lake lint and lake test commands. These will be automatically run in CI if you install lean-action. We will assume your project has a dependency on Batteries or Mathlib, which is the case if you follow the recommended lake new ... math template.

Adding a linter

To add a linter to your project, edit your lakefile and set the lintDriver field to an executable. The linter executable included with Batteries (and therefore Mathlib) is called batteries/runLinter.

For a lakefile.toml, add a line lintDriver = "batteries/runLinter" to the first block in the file. For example:

 name = "foo"
 version = "0.1.0"
 keywords = ["math"]
 defaultTargets = ["Foo"]
+lintDriver = "batteries/runLinter"

For a lakefile.lean, add a line lintDriver := "batteries/runLinter" to the package declaration. For example:

 package foo where
+  lintDriver := "batteries/runLinter"

The command lake lint will build and run the executable specified by lintDriver. If it exits with a nonzero status code, the linter is considered to have failed.

Adding a test driver

To add a test driver to your project, edit your lakefile and set the testDriver field to a library to build or an executable to run. In our example, we assume you have a directory FooTest containing test files. We will configure the test to succeed when all files in FooTest build successfully.

For a lakefile.toml, add a line testDriver = "FooTest" to the first block in the file, then add a lean_lib declaration for FooTest. For example:

 name = "foo"
 version = "0.1.0"
 keywords = ["math"]
 defaultTargets = ["Foo"]
+testDriver = "fooTest"
+
+[[lean_lib]]
+name = "FooTest"
+globs = ["FooTest.+"] # Build all files in the directory `FooTest`.

For a lakefile.lean, add a line testDriver := "FooTest" to the package declaration, then add a lean_lib declaration for FooTest. For example:

 package foo where
+  testDriver := "FooTest"
+
+lean_lib FooTest where
+  globs := #[.submodules `FooTest] -- Build all files in the directory `FooTest`.

The command lake test will build and run the executable specified by testDriver. If it exits with a nonzero status code, the tests are considered to have failed. There is currently no reusable test executable.