Testar no percurso de Lean

Executar os testes

Para executar os testes, certifica-te de que tens o Lean 4 instalado.

A partir da pasta do exercício, executa:

lake test

Resolver o exercício

Uma solução para um exercício é um módulo Lean. O nome do módulo é definido numa instrução de importação no início do conjunto de testes:

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]

Neste exemplo, o ficheiro de testes importa, na linha 2, um módulo chamado ExerciseName. O teste first test chama uma função ExerciseName.someFun com os argumentos someArg1 e someArg2. Este ExerciseName antes de someFun é um namespace, definido no módulo com o mesmo nome, ou seja, ExerciseName. Isto significa que tens de criar um ficheiro com o nome ExerciseName.lean com este aspeto:

namespace ExerciseName

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

end ExerciseName

Repara que os testes costumam chamar uma ou mais funções com um certo número de argumentos. Espera-se que todas elas estejam definidas no módulo da solução, dentro de um namespace com o mesmo nome do módulo.

Cada argumento e o valor devolvido de cada função têm um tipo. Esse tipo pode ser um dos tipos básicos de Lean (por exemplo, Nat, List Int ou Option String), ou um tipo definido pelo utilizador.

Vais encontrar um ficheiro com o nome correto já criado na mesma pasta do módulo de testes. Esse ficheiro deve ter um stub com a maior parte das informações iniciais, para que o possas usar como ponto de partida para a tua solução.

Lembra-te apenas de que este stub existe só para te ajudar a começar. Sente-te à vontade para o alterar por completo, se achares que é o melhor a fazer.

Usar pacotes

Os projetos Lean que usam o Lake podem importar sempre a biblioteca padrão Std, que contém estruturas de dados adicionais, APIs de E/S e de sistema, e outros utilitários básicos. Esta importação deve estar no início do ficheiro:

import Std

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

Neste exemplo, o tipo HashMap está qualificado com Std, o namespace onde é definido. Todos os recursos da biblioteca padrão estão no mesmo namespace, Std.

Também é possível abrir um módulo para que todas as suas estruturas de dados e funções fiquem disponíveis sem essa qualificação de namespace:

import Std

open Std

def someSet : TreeSet String := ...

Os pacotes externos não estão disponíveis diretamente e têm de ser adicionados como dependência no lakefile.toml.

Enquanto trabalhas localmente, podes usar o pacote que quiseres. No entanto, o executor de testes online só tem acesso à biblioteca padrão Std.