官网的各种文档很丰富!
首先是安装 elan: Lean version manager, 熟悉 Rust 的自然了然于胸, 类似于 rustup. elan 是 Rust 编写的 (嗯, 会不会未来 Lean 的 C++ 也会切换到 Rust? 哈哈)
# source $HOME/.elan/env
elan self update
elan default leanprover/lean4:stable
然后, lake 类比于 Cargo
lake new lean-snippet
cd lean-snippet
lake build
./.lake/build/bin/lean-snippet
顺便提一下本人的第一个 Lean4 PR 5789, 哈哈~