패키지

패키지 (Packages)

Idris는 패키지 설명 파일(package description file)에서 패키지를 빌드하는 단순한 시스템을 포함해요. 이 파일들은 Idris 컴파일러와 함께 사용해 Idris 프로그램과 패키지의 개발 과정을 관리할 수 있어요.

출처: 문서

본문

패키지 설명 (Package Descriptions)

패키지 설명은 다음 요소를 포함해요:

  • 키워드 package 뒤에 패키지 이름이 오는 헤더(header). 패키지 이름은 유효한 Idris 식별자(identifier)면 무엇이든 될 수 있어요. iPKG 형식은 유효한 파일명이라면 무엇이든 받아들이는 따옴표 버전(quoted version)도 취해요.

  • 패키지 내용물을 설명하는 필드, <field> = <value>

필드 중 적어도 하나는 modules 필드여야 하며, 그 값은 모듈들의 쉼표로 구분된 목록이에요. 예를 들어 두 모듈 foo.idr와 bar.idr를 소스 파일로 가진 라이브러리 test는 다음과 같이 작성돼요:

package test

modules = foo, bar

패키지 파일의 다른 예는 Idris 메인 저장소의 libs 디렉터리와 서드파티 라이브러리에서 찾을 수 있어요.

메타데이터 (Metadata)

Idris v0.12부터 iPKG 형식은 패키지와 연관된 추가 메타데이터를 지원해요.

추가된 필드는 다음과 같아요:

  • brief = "<text>", 패키지에 대한 간단한 설명을 담는 문자열 리터럴.

  • version = <text>, 패키지와 연관시킬 버전 문자열.

  • readme = <file>, README 파일의 위치.

  • license = <text>, 라이선싱 정보에 대한 문자열 설명.

  • author = <text>, 작성자 정보.

  • maintainer = <text>, 유지 관리자(Maintainer) 정보.

  • homepage = <url>, 패키지와 연관된 웹사이트.

  • sourceloc = <url>, 소스를 찾을 수 있는 DVCS의 위치.

  • bugtracker = <url>, 프로젝트 버그 추적기의 위치.

공통 필드 (Common Fields)

ipkg 파일에 있을 수 있는 다른 일반적인 필드는 다음과 같아요:

  • sourcedir = <dir>, 소스를 담는 (현재 디렉터리에 상대적인) 디렉터리를 취함. 기본값은 현재 디렉터리.

  • executable = <output>, 생성할 실행 파일의 이름을 취함. 실행 파일 이름은 유효한 Idris 식별자면 무엇이든 될 수 있어요. iPKG 형식은 유효한 파일명이라면 무엇이든 받아들이는 따옴표 버전도 취해요.

  • main = <module>, 메인 모듈의 이름을 취하며, executable 필드가 있으면 반드시 있어야 해요.

  • opts = "<idris options>", Idris에 옵션을 전달할 수 있게 함.

  • pkgs = <pkg name> (',' <pkg name>)+, Idris 패키지가 요구하는 패키지 이름들의 쉼표로 구분된 목록.

C 바인딩 (Binding to C)

더 고급의 경우, 특히 외부 C 라이브러리에 대한 바인딩 생성을 지원할 때 다음 옵션을 사용할 수 있어요:

  • makefile = <file>, Idris 모듈보다 먼저 빌드될 Makefile을 지정함. 예를 들어 C 라이브러리와의 링크를 지원하기 위해. 빌드할 때 Idris는 환경 변수 IDRIS_INCLUDES(C include 플래그 포함)와 IDRIS_LDFLAGS(C 링크 플래그 포함)를 설정해서, Makefile 내부에서 사용할 수 있게 해줘요.

  • libs = <libs>, 패키지를 사용할 수 있으려면 반드시 있어야 하는 라이브러리들의 쉼표로 구분된 목록.

  • objs = <objs>, 설치할 추가 파일들(객체 파일, 헤더)의 쉼표로 구분된 목록. 아마 Makefile이 생성할 것.

테스팅 (Testing)

Idris 패키지를 테스트하기 위한 기본적인 테스트 하네스(testing harness)가 있으며, IO 컨텍스트에서 실행돼요.

iPKG 파일은 테스트에 사용할 함수들을 지정하는 데 사용돼요.

다음 옵션을 사용할 수 있어요:

  • tests = <test functions>, 실행할 모든 테스트 함수의 한정 이름(qualified names).
중요 (Important)

테스트 함수를 포함한 모듈도 반드시 모듈 목록에 추가해야 해요.

주석 (Comments)

패키지 파일은 표준 Idris 한 줄 -- 및 여러 줄 {- -} 형식을 사용한 주석을 지원해요.

패키지 파일 사용하기 (Using Package files)

Idris 패키지 파일 test.ipkg가 주어지면 다음과 같이 Idris 컴파일러와 함께 사용할 수 있어요:

  • idris --build test.ipkg는 패키지 안의 모든 모듈을 빌드함

  • idris --install test.ipkg는 패키지를 설치해 다른 Idris 라이브러리와 프로그램이 접근할 수 있게 함

  • idris --clean test.ipkg는 빌드할 때 생성된 모든 중간 코드와 실행 파일을 삭제함

  • idris --mkdoc test.ipkg는 프로젝트 루트 디렉터리의 test_doc 폴더에 패키지용 HTML 문서를 빌드함

  • idris --installdoc test.ipkg는 패키지 문서를 idris --docdir에 위치한 Idris 중앙 문서 폴더에 설치함

  • idris --checkpkg test.ipkg는 패키지 안의 모든 모듈을 타입 검사만 함. 빌드가 타입 검사와 코드 생성을 함께 하는 것과는 다름

  • idris --testpkg test.ipkg는 tests 매개 변수에 지정한 임베디드 테스트를 컴파일·실행함

패키지를 빌드하거나 설치할 때 명령줄 플래그 --warnipkg는 프로젝트를 감사(audit)하고 잠재적인 문제를 경고해줘요.

테스트 패키지가 설치되고 나면 명령줄 옵션

--package test가 이를 접근 가능하게 해줘요 (-p test로 축약).

예를 들어:

idris -p test Main.idr

더 알아보기 (Learn more)