Lean 轨道上的测试

运行测试

要运行测试，请先确认已安装 Lean 4。

在练习目录下，运行：

lake test

解决练习

一道练习的解答就是一个 Lean 模块。 模块的名字由测试套件开头的一条 导入语句 定义：

import LeanTest
import ExerciseName

open LeanTest

def exerciseNameTests : TestSuite :=
  (TestSuite.empty "ExerciseName")
  |>.addTest "first test" (do
        return assertEqual someVal (ExerciseName.someFun someArg1 someArg2))
    ...

def main : IO UInt32 := do
  runTestSuitesWithExitCode [exerciseNameTests]

在这个例子中，测试文件在第 2 行导入了名为ExerciseName的模块。 测试first test调用函数ExerciseName.someFun，并传入实参someArg1和someArg2。 someFun前面的这个ExerciseName是一个命名空间，定义在同名的模块中，也就是ExerciseName。 这意味着你需要创建一个名为ExerciseName.lean的文件，内容如下：

namespace ExerciseName

def someFun (someArg1 : Type1) (someArg2 : Type2) : ReturnType :=
    ...

end ExerciseName

注意，测试通常会调用一个或多个函数，并传入若干实参。 这些函数都应该定义在解答模块里，位于与模块同名的命名空间中。

每个函数的每个实参以及返回值都有各自的类型。 它可能是 Lean 中的某个基础类型（例如Nat、List Int或Option String），也可能是用户自定义的类型。

你会发现，在与测试模块同一个文件夹里已经有一个名字正确的文件。 这个文件里应该有一个 桩代码，包含大部分初始信息，你可以把它作为解答的起点。

请记住，这个桩代码只是为了帮你上手。 如果你觉得合适，完全可以把它彻底改掉。

使用包

使用 Lake 的 Lean 项目总是可以导入标准库Std，其中包含更多数据结构、I/O 和系统 API，以及其他基础工具。 这条导入语句应该放在文件开头：

import Std

def someMap : Std.HashMap Int Nat := ...

在这个例子中，类型HashMap用Std进行了限定，Std就是定义它的命名空间。 标准库中的所有资源都在同一个命名空间Std中。

你也可以打开一个模块，这样它的所有数据结构和函数都不需要这个命名空间限定就能使用：

import Std

open Std

def someSet : TreeSet String := ...

外部包不能直接使用，必须在lakefile.toml中作为依赖添加。

在本地开发时，你可以使用任何你喜欢的包。 但在线测试运行器只能访问标准库Std。