LeanPort v0.1.1은 Lean 4로 작성하고 증명한 모듈을 C 정적 라이브러리와 Go/cgo 패키지로 변환하는 명령줄 도구다. LeanPort 제작자에 따르면 애플리케이션을 빌드하는 사람은 Lean을 설치할 필요 없이 Go, cgo, C 컴파일러만 있으면 된다.
LeanPort는 스칼라형, 문자열, 바이트 배열을 생성할 수 있다. 스칼라형만 쓰면 Lean 런타임이 포함되지 않는 런타임 프리 아카이브를 만들고, String이나 ByteArray를 쓰면 Lean 런타임을 포함하는 런타임 링크 아카이브를 만든다. 제작자가 제시한 크기는 각각 12~28KB와 약 29MB다. 레코드, 배열, Option, Except는 ABI 매핑을 검증하지만 아직 생성 기능은 지원하지 않는다.
Lean 코드를 바꾸는 유지보수자는 leanport check로 증명을 확인하고 leanport build로 네이티브 코드와 Go 바인딩을 다시 생성해야 한다. 일반적인 Go 빌드는 이미 생성된 패키지만 컴파일하므로 Lean 변경 사항을 반영하지 않는다. cgo가 필수라 CGO_ENABLED=0인 순수 Go 빌드에서는 사용할 수 없으며, v0.1.1은 호스트 대상용 아카이브를 만든다. 여러 런타임 프리 패키지는 함께 쓸 수 있지만 런타임 링크 패키지는 v0.1.1에서 하나만 지원한다. 검증 경계 밖에 있는 인증·데이터베이스 일관성 같은 애플리케이션 규칙까지 LeanPort가 증명하는 것은 아니다.
Go로 설치하려면 다음 명령을 사용한다.
go install github.com/shrsv/LeanPort/cmd/leanport@v0.1.1
전체 사용 예제는 튜토리얼, 지원 범위와 제약은 제한 사항 문서에서 확인할 수 있다. 제작자는 파이프라인을 종단 간 테스트했으며, 테스트에는 증명 검사와 Go 테스트, 의도적으로 실패하는 sorry 사례가 포함됐다고 밝혔다. 저장소
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요