Тестування на треку Lean

Як тестувати свої вправи з Lean на Exercism

Запуск тестів

Щоб запустити тести, переконайтеся, що 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]

У цьому прикладі тестовий файл у другому рядку імпортує модуль із назвою ExerciseName. Тест first test викликає функцію ExerciseName.someFun з аргументами someArg1 та someArg2. Цей ExerciseName перед someFun є простором імен, визначеним у модулі з тією ж назвою, тобто ExerciseName. Це означає, що потрібно створити файл із назвою ExerciseName.lean, який має такий вигляд:

namespace ExerciseName

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

end ExerciseName

Зауважте, що тести зазвичай викликають одну чи більше функцій із кількома аргументами. Усі вони мають бути визначені в модулі рішення, у просторі імен із тією ж назвою, що й модуль.

Кожен аргумент і повернене значення кожної функції має певний тип. Це може бути один із базових типів Lean (наприклад, Nat, List Int або Option String) чи тип, визначений користувачем.

Файл із правильною назвою вже лежить у тій самій теці, що й тестовий модуль. Цей файл має містити заготовку з більшістю початкових відомостей, щоб можна було взяти її за відправну точку для рішення.

Просто майте на увазі, що ця заготовка потрібна лише для того, щоб почати. Якщо вважаєте, що так буде правильно, сміливо переробіть її повністю.

Використання пакетів

Проєкти Lean, що використовують Lake, завжди можуть імпортувати стандартну бібліотеку Std, яка містить додаткові структури даних, засоби введення-виведення та системні API, а також інші базові утиліти. Цей імпорт має бути на початку файлу:

import Std

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

У цьому прикладі тип HashMap кваліфіковано через Std, простір імен, у якому його визначено. Усі ресурси стандартної бібліотеки перебувають у тому самому просторі імен, Std.

Також можна відкрити модуль, щоб усі його структури даних і функції були доступні без цієї кваліфікації простором імен:

import Std

open Std

def someSet : TreeSet String := ...

Зовнішні пакети недоступні напряму, і їх потрібно додати як залежність у lakefile.toml.

Працюючи локально, можна використовувати будь-який пакет. Однак онлайн-засіб запуску тестів має доступ лише до стандартної бібліотеки Std.