컴파일, 로깅, 리포트

컴파일, 로깅, 리포트 (Compilation, Logging, and Reporting)

이 섹션은 Idris 컴파일 과정에 대한 정보를 제공하고, 로깅을 통해 그 과정을 따라가는 방법에 대한 세부 사항을 제공해요.

출처: 문서

본문

컴파일 과정 (Compilation Process)

Idris는 다음 컴파일 과정을 따르고 있어요.

  • 파싱 (Parsing)
  • 타입 체킹 (Type Checking)
  • 정교화 (Elaboration)
  • 커버리지 (Coverage)
  • 통일 (Unification)
  • 전체성 검사 (Totality Checking)
  • 소거 (Erasure)
  • 코드 생성 (Code Generation)
  • 역함수화 (Defunctionalisation)
  • 인라인 (Inlining)
  • 변수 해석 (Resolving variables)
  • 코드 생성 (Code Generation)

타입 체킹만 하기 (Type Checking Only)

Idris를 사용하면 타입 체킹이 완료된 후에 컴파일 과정을 종료하도록 요청할 수 있어요. 이것은 다음 중 하나를 통해 달성해요.

  • 파일을 위한 --check 커맨드라인 옵션
  • 패키지를 위한 --checkpkg
  • REPL 명령: :check

이 옵션을 사용해도 Idris 바이너리 .ibc 파일의 생성은 여전히 일어나며, 지원되는 백엔드 중 하나에서 코드를 생성하고 싶지 않을 때 적합해요.

컴파일 과정 리포트 (Reporting Compilation Process)

컴파일 중, Idris의 진행 상황 보고는 장황도(verbosity) 수준을 설정해 제어할 수 있어요.

  • -V, 또는 동등하게 --verbose와 --V0는 Idris가 현재 어떤 파일을 타입 체킹하고 있는지 보고해요.
  • --V1은 추가로 보고해요: 파싱, IBC 생성, 코드 생성.
  • --V2는 추가로 보고해요: 전체성 검사, 유니버스 검사, 그리고 코드 생성 전의 개별 단계들.

기본적으로 Idris의 진행 보고는 조용히 설정돼요: -q, 또는 --quiet.

내부 동작 로깅 (Logging Internal Operation)

Idris 컴파일러를 개발하는 사람들을 위해, Idris의 내부 동작은 카테고리 기반 로거로 캡처돼요. 현재 로깅 인프라는 다음 카테고리를 지원해요:

  • 파서 (parser)
  • 정교화기 (elab)
  • 코드 생성 (codegen)
  • 소거 (erasure)
  • 커버리지 검사 (coverage)
  • IBC 생성 (ibc)

이 카테고리들은 커맨드라인 옵션 --logging-categories CATS로 지정돼요. 여기서 CATS는 보고 싶은 카테고리의 콜론으로 구분된 따옴표 문자열이에요. 기본적으로 이 옵션이 지정되지 않으면 모든 카테고리가 허용돼요. 하위-카테고리(sub-categories)는 아직 정의되지 않았지만, 미래에 — 특히 정교화기를 위해 — 정의될 거예요.

또한 로깅의 장황도는 커맨드라인 옵션 --log <level>로 1에서 10 사이의 로깅 수준을 지정해 제어할 수 있어요.

  • 수준 0: 로깅 출력을 보여주지 않아요. 기본 수준이에요.
  • 수준 1: 컴파일 과정의 높은 수준 세부 사항.
  • 수준 2: 커버리지 검사에 대한 세부 사항, 그리고 정교화 과정의 세부 사항 — 특히, 인터페이스, 절(clauses), 데이터, 용어, 타입.
  • 수준 3: IRTS의 컴파일, 소거, 파싱, case 분할에 대한 세부 사항, 그리고 정교화의 추가 세부 사항: 구현, 프로바이더, 값.
  • 수준 4: 소거, 커버리지 검사, case 분할, 절의 정교화에 대한 추가 세부 사항.
  • 수준 5: 증명기(prover)에 대한 세부 사항, 그리고 정교화(선언 추가)와 IRTS 컴파일의 추가 세부 사항.
  • 수준 6: 정교화와 커버리지 검사의 추가 세부 사항.
  • 수준 7:
  • 수준 8:
  • 수준 9:
  • 수준 10: 정교화의 추가 세부 사항.

환경 변수 (Environment Variables)

Idris 컴파일러 내에서 기본으로 설정된 여러 경로는 환경 변수를 통해 재정의될 수 있어요. 제공되는 변수는:

  • IDRIS_CC — C 백엔드가 사용하는 C 컴파일러를 변경해요.
  • IDRIS_CFLAGS — C 컴파일러에 전달되는 C 플래그를 변경해요.
  • TARGET — 대상 디렉터리, 즉 Cabal/Stack을 사용해 설치할 때 Idris가 파일을 설치하는 데이터 디렉터리를 변경해요.
  • IDRIS_LIBRARY_PATH — 설치된 패키지가 발견/설치되는 위치를 변경해요.
  • IDRIS_DOC_PATH — 패키지에 대해 생성된 idrisdoc이 설치되는 위치를 변경해요.

주의: 0.12.3 이전의 Idris 버전에서는 환경 변수 IDRIS_LIBRARY_PATH와 TARGET 둘 다 단일 패키지의 설치에 영향을 주고 Idris가 데이터를 설치하는 위치를 지시하는 데 사용됐어요. 이 변수들의 의미는 변경되었으며, 개별 패키지가 설치되는 위치를 바꿀 때에는 커맨드라인 옵션이 선호돼요.

--ibcsubdir CLI 옵션은 생성된 IBC 파일이 놓일 위치를 지시하는 데 사용할 수 있어요. 그러나 이것은 Idris가 나머지 설치된 패키지들과 분리된 비-표준 위치에 파일을 설치한다는 뜻이에요. --idrispath <dir> CLI 옵션은 라이브러리 탐색 경로에 디렉터리를 추가하게 해줘요; 이 옵션은 여러 번 사용할 수 있고 -i <dir>로 줄일 수 있어요. 마찬가지로 --sourcepath <dir> 옵션은 소스 탐색 경로에 디렉터리를 추가하는 데 사용할 수 있어요. -s는 예약된 플래그이므로 이 옵션에 대한 축약 버전은 없어요.

또한 Idris는 사용되는 경로를 보강하고 코드 생성기 백엔드에 옵션을 전달하는 옵션도 지원해요. --cg-opt <ARG> 옵션은 코드 생성기에 옵션을 전달하는 데 사용할 수 있어요. <ARG>의 형식은 선택된 백엔드에 따라 달라요.

더 알아보기 (Learn more)