패키지

패키지 (Packages)

Idris는 이름 붙은 패키지 설명 파일에서 패키지와 실행 파일을 빌드하는 간단한 빌드 시스템을 포함해요. 이 파일들은 개발 과정을 관리하기 위해 Idris 컴파일러와 함께 사용될 수 있어요.

출처: 문서

본문

패키지 설명 (Package Descriptions)

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

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

• 패키지 내용을 기술하는 필드, <field> = <value>.

적어도 하나의 필드는 modules 필드여야 하며, 값은 모듈들의 쉼표로 구분된 목록이에요. 예를 들어 모듈 Maths.idr, Maths.NumOps.idr, Maths.BinOps.idr, Maths.HexOps.idr을 가진 idris 패키지 maths가 주어졌다면, 그에 해당하는 패키지 파일은 다음과 같아요:

package maths

modules = Maths
        , Maths.NumOps
        , Maths.BinOps
        , Maths.HexOps

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

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

Idris 자체가 패키지에 대해 알고 있고, 예를 들어 패키지 빌드, 패키지 설치, 패키지 정리를 돕는 특수 명령이 제공돼요. 예를 들어 앞서의 maths 패키지가 주어졌다면 다음과 같이 Idris를 사용할 수 있어요:

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

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

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

maths 패키지가 설치되고 나면, 명령줄 옵션

--package maths가 그것을 접근 가능하게 해줘요 (-p maths로 축약).

예를 들어:

idris -p maths Main.idr

Idris 패키지 테스팅 (Testing Idris Packages)

통합 빌드 시스템은 간단한 테스트 프레임워크를 포함해요. 이 프레임워크는 ipkg 파일의 tests 아래에 나열된 함수들을 모아요. 모든 테스트 함수는 IO ()를 반환해야 해요.

idris --testpkg yourmodule.ipkg를 입력하면, 빌드 시스템이 단일 main 함수 아래에 테스트 함수들을 나열해 여러분의 머신의 새로운 환경에 임시 파일을 만들어요.

이 임시 파일을 실행 파일로 컴파일한 다음 실행해요. 테스트 자체가 자신의 성공 또는 실패를 보고할 책임이 있어요.

테스트 함수는 일반적으로 putStrLn을 사용해 테스트 결과를 보고해요. 테스트 프레임워크는 보고에 대한 어떤 표준도 부과하지 않으며, 따라서 테스트 결과를 집계하지 않아요.

예를 들어, 샘플 패키지 maths의 NumOps라는 모듈에 정의된 다음 함수 목록을 봅시다:

module Maths.NumOps

%access export -- to make functions under test visible

double : Num a => a -> a
double a = a + a

triple : Num a => a -> a
triple a = a + double a

한정 이름 Test.NumOps를 가진 간단한 테스트 모듈은 다음과 같이 선언될 수 있어요:

module Test.NumOps

import Maths.NumOps

%access export  -- to make the test functions visible

assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
assertEq g e = if g == e
    then putStrLn "Test Passed"
    else putStrLn "Test Failed"

assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
assertNotEq g e = if not (g == e)
    then putStrLn "Test Passed"
    else putStrLn "Test Failed"

testDouble : IO ()
testDouble = assertEq (double 2) 4

testTriple : IO ()
testTriple = assertNotEq (triple 2) 5

함수 assertEq와 assertNotEq는 통과가 기대되는 동등성 테스트와 실패가 기대되는 동등성 테스트를 실행하는 데 사용돼요. 실제 테스트는 testDouble과 testTriple이며, maths.ipkg 파일에 다음과 같이 선언돼요:

package maths

modules = Maths.NumOps
        , Test.NumOps

tests = Test.NumOps.testDouble
      , Test.NumOps.testTriple

그러면 테스트 프레임워크를 idris --testpkg maths.ipkg로 호출할 수 있어요:

> idris --testpkg maths.ipkg
Type checking ./Maths/NumOps.idr
Type checking ./Test/NumOps.idr
Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr
Test Passed
Test Passed

우리가 assertEq와 assertNoEq 함수로 준비한 대로 Test Passed를 출력해 두 테스트가 모두 성공을 보고한 방식을 유의하세요.

Atom을 사용한 패키지 종속성 (Package Dependencies Using Atom)

Atom 에디터를 사용하고 다른 패키지에 대한 종속성이 있다면 — 예를 들어 import Lightyear 또는 import Pruviloj에 해당 — Atom에게 로드되어야 한다는 것을 알려야 해요. 이를 달성하는 가장 쉬운 방법은 .ipkg 파일을 사용하는 것이에요. ipkg 파일의 일반적인 내용은 튜토리얼의 다음 절에서 기술하겠지만, 지금은 이 사소한 경우에 대한 간단한 레시피를 보여줄게요:

• myProject 폴더를 만드세요.

• 두 줄만 담긴 myProject.ipkg 파일을 추가하세요:

package myProject

pkgs = pruviloj, lightyear

• Atom에서 File 메뉴로 myProject 폴더를 여세요.

더 많은 정보 (More information)

사용 가능한 필드의 완전한 목록을 포함한 더 많은 세부 사항은 참조 매뉴얼의 Packages에서 찾을 수 있어요.

더 알아보기 (Learn more)

• Idris 참조 — 패키지