2.3. Starting a Project🔗

Lean으로 작성한 프로그램이 본격화될수록 실행 파일을 만드는 사전 컴파일(AOT) 기반 작업 흐름이 더 매력적이다. 다른 언어와 마찬가지로 Lean에는 여러 파일로 된 패키지를 빌드하고 의존성을 관리하는 도구가 있다. 표준 Lean 빌드 도구는 Lake(“Lean Make”의 줄임말)다. Lake는 보통 의존성을 선언적으로 지정하고 빌드할 대상을 설명하는 TOML 파일로 구성한다. 고급 사용 사례에서는 Lake 자체를 Lean으로 구성할 수도 있다.

2.3.1. First steps🔗

Lake를 사용하는 프로젝트를 시작하려면 greeting 파일이나 디렉터리가 없는 디렉터리에서 lake new greeting 명령을 사용하라. 이 명령은 다음 파일을 담은 greeting 디렉터리를 만든다.

Main.lean은 Lean 컴파일러가 main 동작을 찾는 파일이다.
Greeting.lean과 Greeting/Basic.lean은 프로그램을 지원하는 라이브러리의 뼈대다.
lakefile.toml은 애플리케이션을 빌드하는 데 lake가 필요한 구성을 담는다.
lean-toolchain은 프로젝트에 사용하는 특정 Lean 버전의 식별자를 담는다.

또한 lake new는 프로젝트를 Git 저장소로 초기화하고 중간 빌드 결과를 무시하도록 .gitignore 파일을 구성한다. 일반적으로 애플리케이션 로직의 대부분은 프로그램용 라이브러리 모음에 들어가고, Main.lean에는 명령줄을 해석하고 핵심 애플리케이션 로직을 실행하는 작은 래퍼가 들어간다. 이미 존재하는 디렉터리에 프로젝트를 만들려면 lake new 대신 lake init을 실행하라.

기본적으로 라이브러리 파일 Greeting/Basic.lean에는 정의 하나가 들어 있다.

File: Greeting/Basic.leandef hello := "world"

라이브러리 파일 Greeting.lean은 Greeting/Basic.lean을 가져온다.

File: Greeting.lean-- This module serves as the root of the `Greeting` library.-- Import modules here that should be built as part of the library.import Greeting.Basic

따라서 Greeting/Basic.lean에 정의한 모든 것이 Greeting.lean을 가져오는 파일에서도 사용 가능하다. import 문에서 점은 디스크의 디렉터리로 해석된다.

실행 파일의 소스인 Main.lean에는 다음이 들어 있다.

File: Main.leanimport Greetingdef main : IO Unit := IO.println s!"Hello, {hello}!"

Main.lean이 Greeting.lean을 가져오고 Greeting.lean이 Greeting/Basic.lean을 가져오므로 hello의 정의를 main에서 사용할 수 있다.

패키지를 빌드하려면 lake build 명령을 실행하라. 몇 개의 빌드 명령이 지나가면 결과 바이너리가 .lake/build/bin에 놓인다. ./.lake/build/bin/greeting을 실행하면 Hello, world!이 출력된다. 바이너리를 직접 실행하는 대신 lake exe 명령으로 필요할 때 바이너리를 빌드한 뒤 실행할 수 있다. lake exe greeting을 실행해도 Hello, world!이 출력된다.

2.3.2. Lakefiles🔗

lakefile.toml은 배포할 Lean 코드의 일관된 모음인 패키지를 설명한다. npm·nuget 패키지나 Rust 크레이트와 비슷하다. 패키지는 임의의 수의 라이브러리와 실행 파일을 포함할 수 있다. Lake 문서는 Lake 구성에서 사용할 수 있는 옵션을 설명한다. 생성된 lakefile.toml에는 다음 내용이 들어 있다.

                File: lakefile.tomlname = "greeting"version = "0.1.0"defaultTargets = ["greeting"][[lean_lib]]name = "Greeting"[[lean_exe]]name = "greeting"root = "Main"

이 초기 Lake 구성은 세 항목으로 이루어진다.

파일 맨 위의 패키지 설정,
Greeting이라는 이름의 라이브러리 선언,
greeting이라는 이름의 실행 파일.

각 Lake 구성 파일에는 정확히 하나의 패키지와 임의의 수의 의존성·라이브러리·실행 파일이 들어간다. 관례상 패키지와 실행 파일 이름은 소문자로 시작하고 라이브러리 이름은 대문자로 시작한다. 의존성은 다른 Lean 패키지(로컬 패키지 또는 원격 Git 저장소)의 선언이다. Lake 구성 파일의 항목으로 소스 파일 위치, 모듈 계층, 컴파일러 플래그 등을 구성할 수 있다. 그러나 일반적으로 기본값이면 충분하다. Lean 형식으로 작성한 Lake 구성 파일에는 외부 라이브러리(Lean으로 작성하지 않았지만 결과 실행 파일에 정적으로 링크하는 라이브러리), 라이브러리/실행 파일 분류에 자연스럽게 맞지 않는 빌드 대상인 사용자 정의 대상, 패키지 구성의 메타데이터에도 접근할 수 있는 IO 동작(main과 비슷함)인 스크립트도 포함할 수 있다.

라이브러리, 실행 파일, 사용자 정의 대상은 모두 대상(target)이라고 한다. 기본적으로 lake build는 defaultTargets 목록에 지정된 대상을 빌드한다. 기본 대상이 아닌 대상을 빌드하려면 lake build 뒤에 대상 이름을 인수로 지정하라.

2.3.3. Libraries and Imports🔗

Lean 라이브러리는 이름을 가져올 수 있도록 계층적으로 조직한 소스 파일 모음이며 이를 모듈이라고 한다. 기본적으로 라이브러리에는 이름과 일치하는 루트 파일 하나가 있다. 이 경우 Greeting 라이브러리의 루트 파일은 Greeting.lean이다. Main.lean의 첫 줄인 import Greeting은 Greeting.lean의 내용을 Main.lean에서 사용할 수 있게 한다.

Greeting 디렉터리를 만들고 그 안에 파일을 넣어 라이브러리에 모듈 파일을 추가할 수 있다. 디렉터리 구분자를 점으로 바꾸면 이 이름을 가져올 수 있다. 예를 들어 다음 내용의 Greeting/Smile.lean 파일을 만들면:

File: Greeting/Smile.leandef Expression.happy : String := "a big smile"

따라서 Main.lean에서 다음과 같이 정의를 사용할 수 있다.

                File: Main.leanimport Greetingimport Greeting.Smileopen Expressiondef main : IO Unit :=  IO.println s!"Hello, {hello}, with {happy}!"

모듈 이름 계층과 네임스페이스 계층은 분리되어 있다. Lean에서 모듈은 코드 배포의 단위이고 네임스페이스는 코드 조직의 단위다. 즉 Greeting.Smile 모듈에 정의한 이름이 대응하는 Greeting.Smile 네임스페이스에 자동으로 들어가지는 않는다. 특히 happy는 Expression 네임스페이스에 있다. 모듈은 원하는 네임스페이스에 이름을 넣을 수 있고, 이를 가져오는 코드가 네임스페이스를 open할지는 선택이다. import는 소스 파일의 내용을 사용할 수 있게 하고, open은 접두사 없이 네임스페이스의 이름을 현재 문맥에서 사용할 수 있게 한다.

open Expression 줄은 Expression.happy라는 이름을 main에서 happy로 사용할 수 있게 한다. 네임스페이스를 선택적으로 열어 명시적 접두사 없이 일부 이름만 사용할 수도 있다. 원하는 이름을 괄호 안에 쓰면 된다. 예를 들어 Nat.toFloat는 자연수를 Float으로 변환한다. open Nat (toFloat)을 사용하면 이를 toFloat로 사용할 수 있다.