ATS는 타입 시스템에 내장된 증명 기능을 제공하는 프로그래밍 언어로, 증명은 일급 값으로 다루어지며 컴파일 시 제거되어 런타임 오버헤드가 없습니다.

ATS1과 ATS2 빌드 과정은 GitHub 소스에서 직접 수행할 수 있으나, ATS1 저장소의 깨진 autotools 심볼릭 링크와 macOS의 컴파일러 경고 문제 등으로 인해 여러 수동 수정이 필요합니다.

GMP 라이브러리는 ATS2의 타입 검사 시 정수 제약 조건 해결에 필수이며, macOS에서는 Homebrew를 통해 설치 후 경로 설정이 반드시 요구됩니다.

빌드 완료 후에는 ATS2 컴파일러인 patsopt와 patscc를 사용해 ATS 코드를 C로 변환하고, gcc로 최종 실행 파일을 생성할 수 있습니다.

또한, 사전 생성된 C 소스가 포함된 릴리스 타르볼을 만들어 ATS1 없이도 컴파일 가능하며, 이 방식은 C 컴파일러만 있으면 설치와 사용이 간편합니다.