2.3. 프로젝트 시작하기🔗

Lean으로 작성된 프로그램이 더 본격적으로 발전할수록, 실행 파일을 결과물로 내는 사전 컴파일러 기반 워크플로가 더 매력적으로 다가옵니다. 다른 언어들과 마찬가지로, Lean에는 여러 파일로 이루어진 패키지를 빌드하고 의존성을 관리하는 도구가 있습니다. Lean의 표준 빌드 도구는 Lake(“Lean Make”의 줄임말)라고 불립니다. Lake는 일반적으로 의존성을 선언적으로 명시하고 빌드할 대상을 기술하는 TOML 파일을 사용하여 설정합니다. 고급 사용 사례를 위해, Lake는 Lean 자체로도 설정할 수 있습니다.

2.3.1. 첫걸음🔗

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. Lakefile🔗

lakefile.toml은 패키지를 기술하며, 이는 배포를 위한 일관된 Lean 코드 모음으로, npm이나 nuget 패키지 또는 Rust crate와 유사합니다. 패키지는 라이브러리나 실행 파일을 몇 개든 포함할 수 있습니다. 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 설정은 세 가지 항목으로 구성됩니다:

파일 상단의 package 설정,
Greeting이라는 이름의 library 선언과
greeting이라는 이름의 실행 파일입니다.

각 Lake 설정 파일은 정확히 하나의 패키지를 포함하지만, 의존성, 라이브러리, 실행 파일은 임의의 개수만큼 포함할 수 있습니다. 관례상, 패키지와 실행 파일 이름은 소문자로 시작하고, 라이브러리는 대문자로 시작합니다. 의존성은 다른 Lean 패키지(로컬 또는 원격 Git 저장소로부터)에 대한 선언입니다. Lake 설정 파일의 항목들은 소스 파일 위치, 모듈 계층 구조, 컴파일러 플래그와 같은 것들을 설정할 수 있게 해줍니다. 하지만 일반적으로 기본값들은 합리적입니다. Lean 형식으로 작성된 Lake 설정 파일에는 추가로 외부 라이브러리(Lean으로 작성되지 않았으며 결과물인 실행 파일과 정적으로 링크되는 라이브러리), 커스텀 타겟(라이브러리·실행 파일 분류 체계에 자연스럽게 들어맞지 않는 빌드 타겟), 그리고 스크립트(main과 마찬가지로 본질적으로 IO 액션이지만, 패키지 설정에 관한 메타데이터에도 추가로 접근할 수 있는 것)가 포함될 수 있습니다.

라이브러리, 실행 파일, 커스텀 타겟은 모두 targets라고 불립니다. 기본적으로 lake build는 defaultTargets 목록에 지정된 대상들을 빌드합니다. 기본 대상이 아닌 대상을 빌드하려면, lake build 뒤에 인자로 대상의 이름을 지정하십시오.

2.3.3. 라이브러리와 임포트🔗

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로 사용할 수 있게 만들 수 있습니다.