Como testar no Lean

Rodando os testes

Para rodar os testes, certifique-se de que o Lean 4 está instalado.

No diretório do exercício, rode:

lake test

Resolvendo o exercício

Uma solução para um exercício é um módulo Lean. O nome do módulo é definido em uma instrução de importação no início da suíte 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 arquivo 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. Esse ExerciseName antes de someFun é um namespace, definido no módulo com o mesmo nome, ou seja, ExerciseName. Isso significa que você precisa criar um arquivo chamado ExerciseName.lean com esta forma:

namespace ExerciseName

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

end ExerciseName

Repare que os testes geralmente chamam 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 de retorno de cada função têm um tipo. Pode ser um dos tipos básicos do Lean (por exemplo, Nat, List Int ou Option String) ou um tipo definido por você.

Você vai encontrar um arquivo com o nome correto já no lugar, na mesma pasta do módulo de testes. Esse arquivo deve ter um stub com a maior parte das informações iniciais, para que você possa usá-lo como ponto de partida para a sua solução.

Só tenha em mente que esse stub está ali apenas para você começar. Fique à vontade para mudá-lo por completo se você achar que é o certo a fazer.

Usando pacotes

Projetos Lean que usam o Lake sempre podem importar 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. Essa importação deve ficar no início do arquivo:

import Std

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

Neste exemplo, o tipo HashMap está qualificado com Std, o namespace onde ele é 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 := ...

Pacotes externos não ficam disponíveis diretamente e precisam ser adicionados como dependência no lakefile.toml.

Enquanto você trabalha localmente, pode usar qualquer pacote que quiser. O executor de testes online, porém, tem acesso apenas à biblioteca padrão Std.