Testen auf dem Lean-Track

Lerne, wie du deine Lean-Übungen auf Exercism testest

Tests ausführen

Um die Tests auszuführen, stelle sicher, dass Lean 4 installiert ist.

Führe im Übungsverzeichnis Folgendes aus:

lake test

Die Übung lösen

Eine Lösung für eine Übung ist ein Lean-Modul. Der Name des Moduls wird in einer Import-Anweisung am Anfang der Testsuite definiert:

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]

In diesem Beispiel importiert die Testdatei in Zeile 2 ein Modul namens ExerciseName. Der Test first test ruft eine Funktion ExerciseName.someFun mit den Argumenten someArg1 und someArg2 auf. Dieses ExerciseName vor someFun ist ein Namespace, der im Modul mit demselben Namen definiert ist, also ExerciseName. Das bedeutet, du musst eine Datei namens ExerciseName.lean erstellen, die so aussieht:

namespace ExerciseName

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

end ExerciseName

Beachte, dass Tests normalerweise eine oder mehrere Funktionen mit einer Reihe von Argumenten aufrufen. Sie alle sollen im Lösungsmodul definiert sein, und zwar in einem Namespace mit demselben Namen wie das Modul.

Jedes Argument und jeder Rückgabewert einer Funktion hat einen Typ. Das kann einer der grundlegenden Typen in Lean sein (zum Beispiel Nat, List Int oder Option String) oder ein benutzerdefinierter Typ.

Eine Datei mit dem richtigen Namen findest du bereits im selben Ordner wie das Testmodul. Diese Datei sollte einen Stub mit den meisten Ausgangsinformationen enthalten, damit du sie als Startpunkt für deine Lösung verwenden kannst.

Denk daran, dass dieser Stub nur als Einstieg für dich gedacht ist. Ändere ihn gerne komplett, wenn du meinst, dass es das Richtige ist.

Pakete verwenden

Lean-Projekte, die Lake verwenden, können immer die Standardbibliothek Std importieren, die zusätzliche Datenstrukturen, I/O- und System-APIs sowie weitere grundlegende Hilfsmittel enthält. Dieser Import sollte am Anfang der Datei stehen:

import Std

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

In diesem Beispiel wird der Typ HashMap mit Std qualifiziert, dem Namespace, in dem er definiert ist. Alle Ressourcen der Standardbibliothek liegen im selben Namespace, Std.

Du kannst ein Modul auch öffnen, sodass alle seine Datenstrukturen und Funktionen ohne diese Namespace-Qualifizierung verfügbar sind:

import Std

open Std

def someSet : TreeSet String := ...

Externe Pakete sind nicht direkt verfügbar und müssen als Abhängigkeit in lakefile.toml hinzugefügt werden.

Wenn du lokal arbeitest, kannst du jedes Paket verwenden, das dir gefällt. Der Online-Test-Runner hat jedoch nur Zugriff auf die Standardbibliothek Std.