elan 和 lake 基本用法

发表于 更新于 阅读次数： 字数： 1.3k 时间 ≈ 5 分钟
Lake 基本用法。

Lean 除了交互的特性，其本身也可以作为编写真实程序的语言。

前边介绍了 Lean 函数式编程的基础知识，本章将解释如何开始一个编程项目、编译它并运行出结果。

问题导向，注意，博客不是为了写给别人，而是为了让自己的知识更容易形成体系！

先来个 TODO 吧，有个 Ending，以及可持续性。

目前，非常困扰我的有几个点，一是 Lean 包的结构。

总的来说，我想知道这几个事情：

1. lake, elan, lean 分别可以做什么？当然，我只需要给几个例子就可以了。

  1. lean 包的结构是怎样的。

好，既然你摊牌了，不装了，那以后，咱有话就直接在这里说吧。

来吧，别废话了。

我想强烈提醒你一点，避免做 general 的 work，理解吗？就是像，论文综述，工具概述，等等。我不是说学这些东西不合适，而是批判这种，打算一退到底，然后一口气全部吃下来的无知。你可能压根不理解自己到底几斤几两。

好嘞。了解了，那，我不从 shell 脚本的角度来学习了，直接从使用角度好吧！

是的！二八法则！只学那么常用的 20%。

有一个对应，你应该理解

常见用法

elan 是 lean 的版本控制器。

查看已安装版本：

1
2
3
4
5
6
7
8
❯ elan show                                              
installed toolchains
--------------------

stable (default)
leanprover/lean4:stable
leanprover/lean4:v4.10.0
leanprover/lean4:v4.11.0

安装或更新：

1
2
3
elan install leanprover/lean4:v4.11.0
elan install v4.11.0
elan update stable

下载路径：$HOME/.elan/tool-chains 以及 $HOME/.elan/update-hashes。

以某个 toolchain 版本运行 lake 命令：

1
2
elan run v4.11.0 lake new hello
cat hello/lean-toolchain # v4.11.0

lake 是包管理器。

创建包：

1
2
3
4
5
6
7
lake new hello
# 或者
cd xxx && lake init .
# 初始化带 mathlib 仓库的项目
lake new myproject math
# 设置依赖文件，支持 toml 和 lean
lake new myproj math.lean

关于可执行文件

这点，我相当迷糊了？

可以参考几个包结构例子。

以及，import 机制，

首先：

1
2
3
4
5
elan run leanprover/lean4:v4.12.0 lake new demoproject math.lean
# elan run leanprover/lean4:v4.12.0 lake new demoproject2 math.toml
cd demoproject
lake update
lake build

配置文件是仓库的基础，比如 toml 格式：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
name = "demoproject2"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["Demoproject2"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[lean_lib]]
name = "Demoproject2"

这里 lean_lib 指定了包的入口文件。

放一个模块，用于可执行程序：

1
2
3
[[lean_exe]]
name = "hi"
root = "Hi"

然后在 Hi.lean 中，编写相应的 main 函数：

1
2
3
def your_name : String := "rex"
def main : IO Unit :=
  IO.println s!"Hi, {your_name}!"

或者 lean 配置文件：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
import Lake
open Lake DSL

package "demoproject" where
  version := v!"0.1.0"
  keywords := #["math"]
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
  ]

require "leanprover-community" / "mathlib"

@[default_target]
lean_lib «Demoproject» where
  -- add any library configuration options here

类似加一段：

1
2
3
@[default_target]
lean_exe "hello" where
  root := `Main

目标（target） 是 Lake 构建的基本单元。一个包可以定义任意数量的目标。每个目标都有一个名称，用于指示 Lake 去构建该目标，比如加一个：

1
2
@[default_target]
lean_lib «Test» where

在 Test.lean 中编写相关代码。

相关依赖：

1
2
3
require "leanprover-community" / "mathlib"
require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ s!"{Lean.versionString}"

运行程序

我们从最简单的 “Hello World” 程序开始：

1
def main : IO Unit := IO.println "Hello, world!"

使用以下命令运行：

1
lean --run Hello.lean

关键概念：

  • main 的类型是 IO Unit，表示一个不返回有意义值的 I/O 操作
  • Unit 是最简单的类型，可以理解为"空值"，只有一个 unit 构造子
  • IO α 为程序类型，可能产生副作用，要么抛出异常要么返回类型 α 的程序
  • IO.println 从字符串到 IO 活动的函数，将给定的字符串写入标准输出

函数式编程与副作用

Lean 的计算模型基于数学表达式的求值，再次求值相同的表达式会始终产生相同的结果。而另一方面，由于程序必须与世界交互，这些文件的内容可能随时间而改变，那么，要如何编写可以从磁盘读取文件的程序呢？

简单说， Lean 通过分离关注点来处理副作用:

  • Lean 语言本身保持纯函数式，专注于计算逻辑
  • 将 I/O 等副作用操作交给运行时系统 (RTS) 处理
  • 用 IO 类型在两者之间传递信息

理论上，可以把副作用看成接收整个世界状态并返回新世界的纯函数，从标准输入读取一行文本是一个 纯（Pure）函数，因为每次都提供了一个不同的世界作为参数。

当程序启动时，它会提供一个世界标识，比如 do-记法的子语言，它能够将这些原语 IO 活动安全地组合成一个更大、更有用的程序。这种设计既保持了语言的纯度,又能与现实世界交互。

这个更复杂的例子展示了如何与用户交互：

1
2
3
4
5
6
7
8
9
10
def main : IO Unit := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  -- IO.FS.Stream
  stdout.putStrLn "How would you like to be addressed?"
  -- IO.FS.Stream → String → IO Unit
  let input ← stdin.getLine
  -- IO.FS.Stream → IO String
  let name := input.dropRightWhile Char.isWhitespace
  stdout.putStrLn s!"Hello, {name}!"

这里 IO.getStdin 和 IO.getStdout 用来获取标准输入输出句柄，input.dropRightWhile Char.isWhitespace 类似 strip 的操作。

do 语法的特点：

  • 使用 ← 执行 I/O 活动并绑定结果
  • 使用 := 进行普通变量绑定