Leanトラックでのテスト

ExercismでLeanの演習をテストする方法を学びます

テストの実行

テストを実行するには、Lean 4がインストールされていることを確認してください。

演習のディレクトリで、次を実行します：

lake test

演習を解く

演習の解答は、Leanのモジュールです。 モジュールの名前は、テストスイートの先頭にある*import文*で定義されます：

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

テストは通常、いくつかの引数を持つ1つ以上の関数を呼び出すことに注意してください。 それらはすべて、解答のモジュール内で、モジュールと同じ名前の名前空間の中に定義されている必要があります。

各引数と、各関数の戻り値には、それぞれ型があります。 これはLeanの基本型（たとえばNat、List Int、Option String）のいずれかであることもあれば、ユーザー定義型であることもあります。

テストモジュールと同じフォルダーに、正しい名前のファイルがすでに用意されています。 このファイルには、ほとんどの初期情報を含むスタブがあり、解答の出発点として使えます。

このスタブはあくまで学習を始めるためのものだということだけ、覚えておいてください。 必要だと思ったら、遠慮なく完全に書き換えてください。

パッケージを使う

Lakeを使うLeanプロジェクトは、いつでも標準ライブラリStdをインポートできます。Stdには、追加のデータ構造やI/O、システムAPI、その他の基本的なユーティリティが含まれています。 このインポートは、ファイルの先頭に書きます：

import Std

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

この例では、型HashMapは、それが定義されている名前空間であるStdで修飾されています。 標準ライブラリのすべてのリソースは、同じ名前空間Stdにあります。

モジュールを開くことで、そのデータ構造と関数をすべて、この名前空間の修飾なしで使えるようにすることもできます：

import Std

open Std

def someSet : TreeSet String := ...

外部パッケージはそのままでは使えず、lakefile.tomlに依存関係として追加する必要があります。

ローカルで作業している間は、好きなパッケージを自由に使えます。 ただし、オンラインのテストランナーが使えるのは、標準ライブラリStdだけです。