한줄평
“Lean을 쓴다면 툴체인 관리를 사실상 자동화해 주는 필수에 가까운 도구입니다. 다만 Lean 생태계 밖에서는 쓸 일이 없습니다.”
이런 분께 Lean 정리 증명기로 작업하는 연구자·개발자께
좋은 점
- 프로젝트별 Lean 버전을 자동으로 맞춰 충돌을 막습니다
- rustup처럼 익숙한 방식으로 툴체인을 관리합니다
아쉬운 점
- Lean 전용이라 그 생태계 밖에서는 쓰임이 없습니다
일란 소개
Lean 정리 증명기(theorem prover)의 여러 버전을 설치하고 전환해 주는 명령줄 도구입니다. Rust의 rustup에 해당하는 역할로, 프로젝트마다 요구하는 Lean 툴체인을 자동으로 맞춰 주어 버전 충돌을 막습니다. GUI가 아니라 터미널에서 도는 관리 도구이며, Lean으로 수학·형식 검증을 하는 이들이 씁니다.
