Tesztelés a Lean-kurzuson

A tesztek futtatása

A tesztek futtatásához győződj meg róla, hogy telepítve van a Lean 4.

A feladat könyvtárából futtasd:

lake test

A feladat megoldása

Egy feladat megoldása egy Lean-modul. A modul nevét a teszthalmaz elején található import utasítás határozza meg:

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]

Ebben a példában a tesztfájl a 2. sorban importál egy ExerciseName nevű modult. A first test teszt meghívja az ExerciseName.someFun függvényt a következő argumentumokkal: someArg1 és someArg2. A someFun előtti ExerciseName egy névtér, amelyet az azonos nevű modul definiál, azaz az ExerciseName. Ez azt jelenti, hogy létre kell hoznod egy ExerciseName.lean nevű fájlt, amely így néz ki:

namespace ExerciseName

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

end ExerciseName

Vedd figyelembe, hogy a tesztek általában egy vagy több függvényt hívnak meg, több argumentummal. Mindegyiket a megoldásmodulban kell definiálni, egy olyan névtérben, amelynek a neve megegyezik a modul nevével.

Minden függvény minden argumentumának és visszatérési értékének van valamilyen típusa. Ez lehet a Lean valamelyik alaptípusa (például Nat, List Int vagy Option String), vagy egy felhasználó által definiált típus.

A tesztmodullal azonos mappában már ott találsz egy megfelelő nevű fájlt. Ebben a fájlban egy váz található a legtöbb kiindulási információval, hogy kiindulópontként szolgálhasson a megoldásodhoz.

Csak tartsd észben, hogy ez a váz csak azért van, hogy elindulhass vele. Nyugodtan írd át teljesen, ha úgy gondolod, hogy az a helyes.

Csomagok használata

A Lake-et használó Lean-projektek mindig importálhatják a Std szabványkönyvtárat, amely további adatszerkezeteket, I/O és rendszer-API-kat, valamint más alapvető segédprogramokat tartalmaz. Ez az import a fájl elején legyen:

import Std

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

Ebben a példában a HashMap típus a Std névtérrel van minősítve, amelyben definiálva van. A szabványkönyvtár minden erőforrása ugyanabban a Std nevű névtérben található.

Arra is van lehetőség, hogy megnyiss egy modult, így minden adatszerkezete és függvénye elérhetővé válik névtér-minősítés nélkül:

import Std

open Std

def someSet : TreeSet String := ...

A külső csomagok nem érhetők el közvetlenül, ezért függőségként fel kell venned őket a lakefile.toml-ban.

Ha helyben dolgozol, bármilyen csomagot szabadon használhatsz. Az online tesztfuttató azonban csak a Std szabványkönyvtárhoz fér hozzá.