Teste sur le parcours Lean

Apprends à tester tes exercices Lean sur Exercism

Lance les tests

Pour lancer les tests, assure-toi que Lean 4 est installé.

Depuis le dossier de l'exercice, lance :

lake test

Résous l'exercice

La solution d'un exercice est un module Lean. Le nom du module est défini dans une import statement au début de la suite de tests :

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]

Dans cet exemple, le fichier de test importe, à la ligne 2, un module nommé ExerciseName. Le test first test appelle une fonction ExerciseName.someFun avec les arguments someArg1 et someArg2. Ce ExerciseName devant someFun est un espace de noms, défini dans le module du même nom, c'est-à-dire ExerciseName. Cela signifie que tu dois créer un fichier nommé ExerciseName.lean qui ressemble à ceci :

namespace ExerciseName

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

end ExerciseName

À noter que les tests appellent généralement une ou plusieurs fonctions avec un certain nombre d'arguments. Elles sont toutes censées être définies dans le module de la solution, au sein d'un espace de noms portant le même nom que le module.

Chaque argument et la valeur de retour de chaque fonction ont un type. Il peut s'agir de l'un des types de base de Lean (par exemple Nat, List Int ou Option String), ou d'un type défini par l'utilisateur.

Tu trouveras déjà, dans le même dossier que le module de test, un fichier portant le bon nom. Ce fichier contient normalement un stub avec la plupart des informations initiales, afin que tu puisses t'en servir comme point de départ pour ta solution.

Garde simplement à l'esprit que ce stub n'est là que pour t'aider à démarrer. N'hésite pas à le modifier entièrement si tu penses que c'est la bonne chose à faire.

Utilise des paquets

Les projets Lean qui utilisent Lake peuvent toujours importer la bibliothèque standard Std, qui contient des structures de données supplémentaires, des API d'E/S et de système, ainsi que d'autres utilitaires de base. Cet import doit se trouver au début du fichier :

import Std

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

Dans cet exemple, le type HashMap est qualifié par Std, l'espace de noms où il est défini. Toutes les ressources de la bibliothèque standard se trouvent dans le même espace de noms, Std.

Il est aussi possible d'ouvrir un module pour que toutes ses structures de données et ses fonctions soient disponibles sans cette qualification par l'espace de noms :

import Std

open Std

def someSet : TreeSet String := ...

Les paquets externes ne sont pas directement disponibles et doivent être ajoutés comme dépendance dans lakefile.toml.

Quand tu travailles en local, tu peux utiliser le paquet que tu veux. L'exécuteur de tests en ligne, lui, n'a accès qu'à la bibliothèque standard Std.