I test sul percorso Lean

Eseguire i test

Per eseguire i test, assicurati di avere Lean 4 installato.

Dalla directory dell'esercizio, esegui:

lake test

Risolvere l'esercizio

La soluzione di un esercizio è un modulo Lean. Il nome del modulo è definito in una istruzione di import all'inizio della suite di test:

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 questo esempio, il file di test importa, alla riga 2, un modulo chiamato ExerciseName. Il test first test chiama una funzione ExerciseName.someFun con gli argomenti someArg1 e someArg2. Questo ExerciseName prima di someFun è un namespace, definito nel modulo con lo stesso nome, cioè ExerciseName. Questo significa che devi creare un file chiamato ExerciseName.lean che si presenta così:

namespace ExerciseName

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

end ExerciseName

Nota che i test di solito chiamano una o più funzioni con un certo numero di argomenti. Tutte devono essere definite nel modulo della soluzione, all'interno di un namespace con lo stesso nome del modulo.

Ogni argomento e il valore restituito di ciascuna funzione hanno un tipo. Può trattarsi di uno dei tipi di base di Lean (per esempio, Nat, List Int o Option String), oppure di un tipo definito dall'utente.

Troverai già un file con il nome corretto nella stessa cartella del modulo di test. Questo file dovrebbe contenere uno stub con la maggior parte delle informazioni iniziali, così da poterlo usare come punto di partenza per la soluzione.

Tieni solo presente che questo stub serve solo per iniziare. Sentiti libero di modificarlo completamente se pensi che sia la cosa giusta da fare.

Usare i pacchetti

I progetti Lean che usano Lake possono sempre importare la libreria standard Std, che contiene strutture dati aggiuntive, API di I/O e di sistema, e altre utilità di base. Questo import dovrebbe trovarsi all'inizio del file:

import Std

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

In questo esempio, il tipo HashMap è qualificato con Std, il namespace in cui è definito. Tutte le risorse della libreria standard si trovano nello stesso namespace, Std.

È anche possibile aprire un modulo in modo che tutte le sue strutture dati e funzioni siano disponibili senza questa qualificazione del namespace:

import Std

open Std

def someSet : TreeSet String := ...

I pacchetti esterni non sono disponibili direttamente e devono essere aggiunti come dipendenza in lakefile.toml.

Quando lavori in locale, puoi usare qualsiasi pacchetto tu voglia. Il test runner online, invece, ha accesso solo alla libreria standard Std.