Lean으로 배우는 함수형 프로그래밍

2.3. 프로젝트 시작하기🔗

Lean으로 작성하는 프로그램이 본격적인 규모로 커질수록, 실행 파일을 만들어 내는 사전(ahead-of-time) 컴파일러 기반 워크플로가 더욱 매력적입니다. 다른 언어와 마찬가지로 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을 임포트하므로, main에서 hello의 정의를 사용할 수 있습니다.

패키지를 빌드하려면 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 크레이트와 비슷합니다. 패키지에는 라이브러리나 실행 파일이 몇 개든 들어갈 수 있습니다. 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으로 작성되지 않았으며 결과 실행 파일에 정적으로 링크되는 라이브러리인 외부 라이브러리, 라이브러리/실행 파일 분류 체계에 자연스럽게 들어맞지 않는 빌드 타깃인 사용자 정의 타깃, 그리고 본질적으로 (main과 비슷한) IO 액션이지만 패키지 설정에 관한 메타데이터에도 접근할 수 있는 스크립트 역시 포함될 수 있습니다.

라이브러리, 실행 파일, 사용자 정의 타깃을 모두 타깃이라고 부릅니다. 기본적으로 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 줄은 main 안에서 Expression.happy라는 이름을 happy로 사용할 수 있게 합니다. 네임스페이스는 선택적으로 열 수도 있으며, 이렇게 하면 일부 이름만 명시적인 접두사 없이 사용할 수 있습니다. 이렇게 하려면 원하는 이름을 괄호 안에 적습니다. 예를 들어, Nat.toFloat는 자연수를 Float로 변환합니다. open Nat (toFloat)를 사용하면 이 함수를 toFloat로 사용할 수 있습니다.