Lean 트랙에서 테스트하기

테스트 실행하기

테스트를 실행하려면 Lean 4가 설치되어 있어야 해요.

연습 문제 디렉터리에서 다음을 실행해요:

lake test

연습 문제 풀기

연습 문제의 풀이는 Lean 모듈이에요. 모듈의 이름은 테스트 스위트 맨 앞의 import 문 에 정의돼요:

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]

이 예제에서 테스트 파일은 2번째 줄에서 ExerciseName이라는 모듈을 임포트해요. first test 테스트는 someArg1과 someArg2를 인자로 넘겨 ExerciseName.someFun 함수를 호출해요. someFun 앞에 있는 이 ExerciseName은 네임스페이스로, 같은 이름의 모듈, 즉 ExerciseName에 정의돼 있어요. 즉, 다음과 같은 ExerciseName.lean 파일을 만들어야 해요:

namespace ExerciseName

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

end ExerciseName

테스트는 보통 여러 인자를 받는 함수를 하나 이상 호출해요. 그 함수들은 모두 모듈과 같은 이름의 네임스페이스 안에서, 풀이 모듈에 정의되어 있어야 해요.

각 인자와 각 함수의 반환값에는 타입이 있어요. Lean의 기본 타입(예를 들어 Nat, List Int, Option String)일 수도 있고, 사용자가 정의한 타입일 수도 있어요.

테스트 모듈과 같은 폴더에 올바른 이름의 파일이 이미 있을 거예요. 이 파일에는 대부분의 초기 정보가 담긴 _스텁_이 있어서, 풀이를 시작하는 출발점으로 삼을 수 있어요.

다만 이 스텁은 시작을 돕기 위한 것일 뿐이라는 점만 기억해요. 필요하다고 생각되면 얼마든지 완전히 바꿔도 돼요.

패키지 사용하기

Lake을 사용하는 Lean 프로젝트는 항상 표준 라이브러리 Std를 임포트할 수 있는데, 여기에는 추가 자료 구조와 I/O, 시스템 API, 그리고 다른 기본 유틸리티가 들어 있어요. 이 임포트는 파일 맨 앞에 있어야 해요:

import Std

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

이 예제에서 HashMap 타입은 그것이 정의된 네임스페이스인 Std로 한정돼 있어요. 표준 라이브러리의 모든 자원은 같은 네임스페이스인 Std에 있어요.

네임스페이스 한정 없이 어떤 모듈의 모든 자료 구조와 함수를 사용할 수 있도록 모듈을 열 수도 있어요:

import Std

open Std

def someSet : TreeSet String := ...

외부 패키지는 바로 사용할 수 없고, lakefile.toml에 의존성으로 추가해야 해요.

로컬에서 작업할 때는 원하는 패키지를 마음대로 사용할 수 있어요. 하지만 온라인 테스트 러너는 표준 라이브러리 Std에만 접근할 수 있어요.