اجرای تستها
برای اجرای تستها، مطمئن شوید که 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]
در این مثال، فایل تست در خط ۲ ماژولی به اسم ExerciseName را import میکند.
تست 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)، یا نوعی که خود کاربر تعریف کرده است.
فایلی با اسم درست را از قبل در همان پوشهی ماژول تست پیدا میکنید.
این فایل باید یک stub با بیشتر اطلاعات اولیه داشته باشد تا بتوانید از آن به عنوان نقطهی شروعی برای راهحل خود استفاده کنید.
فقط در نظر داشته باشید که این stub تنها برای شروع کار شما گذاشته شده است.
اگر فکر میکنید کار درستی است، راحت آن را کاملاً تغییر دهید.
استفاده از پکیجها
پروژههای Lean که از Lake استفاده میکنند همیشه میتوانند کتابخانهی استاندارد Std را import کنند؛ این کتابخانه شامل ساختارهای دادهی اضافی، ورودی/خروجی و APIهای سیستمی و دیگر ابزارهای پایه است.
این import باید در ابتدای فایل باشد:
import Std
def someMap : Std.HashMap Int Nat := ...
در این مثال، نوع HashMap با Std، فضای نامی که در آن تعریف شده است، مشخص شده است.
همهی منابع کتابخانهی استاندارد در همان فضای نام، یعنی Std، قرار دارند.
همچنین میتوان ماژولی را باز کرد تا همهی ساختارهای داده و توابع آن بدون این مشخصکردن فضای نام در دسترس باشند:
import Std
open Std
def someSet : TreeSet String := ...
پکیجهای خارجی مستقیماً در دسترس نیستند و باید به عنوان یک وابستگی در lakefile.toml اضافه شوند.
وقتی به صورت محلی کار میکنید، میتوانید از هر پکیجی که دوست دارید استفاده کنید.
اما اجراکنندهی تست آنلاین فقط به کتابخانهی استاندارد Std دسترسی دارد.
