网络科技网站有哪些方面,网站更改公司需要重新备案吗,网络营销课程设置,一条龙网页唠唠闲话
Lean 是一个交互式定理证明器#xff08;Interactive Theorem Prover, ITP#xff09;#xff0c;也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器#xff0c;数学家可以把数学定理转换成代码#xff0c;再输入到 Lean 中#xff0…
唠唠闲话
Lean 是一个交互式定理证明器Interactive Theorem Prover, ITP也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器数学家可以把数学定理转换成代码再输入到 Lean 中让程序来验证定理是否正确。用于定理证明的编程语言还有很多比如 CoqisabelleHOL Light 等。很多数学家选择使用 Lean 的标准库 mathlib 作为基础这个仓库也被称为未来的数学图书馆。
Lean 4 的官方文档(Get started)提供了不同平台的安装方式包括 Windows、MacOS 和 Ubuntu 系统且都提供了一行脚本运行的方式。但在国内因为网络问题通常要借助镜像站或手动安装。
当前教程针对 Ubuntu 系统Windows 可以参考 子鱼的博客Mac 系统可以按官网教程使用 homebrew 来快速配置。
安装教程
如果没有网络问题用一行命令安装
wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh bash install_debian.sh ; rm -f install_debian.sh source ~/.profile该命令执行了一个脚本install_debian.sh脚本安装了 VsCodeLEAN 插件以及 elan。
如果下载不了 GitHub 资源在安装了 VsCode 和 LEAN 4 拓展后脚本里只有 elan 是需要手动安装的。
安装 elan
elan 是一个用于管理 LEAN 环境的工具。它的功能类似于 Rust 的 rustup 或 Node.js 的 nvm用于安装、管理和切换不同版本的 Lean。
在 GitHub release 页面根据系统版本下载新版 elan比如 linux-x86_64 系统的 elan 安装器地址为
https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz如果不确定系统架构执行 uname -s 和 uname -m 查看
❯ uname -s
Linux
❯ uname -m
x86_64下载文件并解压
# 如果网络不行就本地下载再上传
curl https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tar.gz
tar xf elan.tar.gz解压得到 elan-init 文件赋予可执行权限并执行
chmod x elan-init
./elan-init完成后在 .bashrc 或 .zshrc 中修改环境变量
export PATH$HOME/.elan/bin:$PATH重启终端检查 elan 版本和默认安装的 Lean 版本
❯ elan -V
elan 3.1.1 (71ddc6633 2024-02-22)
❯ elan show
stable (default)
Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)elan 的管理目录为 $HOME/.elan内容形如
❯ tree .elan -L 2
.elan
├── bin
│ ├── elan
│ ├── lake
│ ├── lean
│ ├── leanc
│ ├── leanchecker
│ ├── leanmake
│ └── leanpkg
├── env
├── settings.toml
├── tmp
├── toolchains
│ └── stable
└── update-hashes└── stable下载的 LEAN 版本在 toolchains 目录下settings.toml 是 elan 的配置文件。
elan 的二进制文件中lake 经常会用到。
Lake 管理器
lake 全称 Lean Make是 LEAN4 的包管理器已合并到 LEAN4 仓库作为源码的一部分。
下边用一个简单的例子演示 lake 的基本用法。
创建项目目录为 hello
# 创建包
lake new hello
## 或者
mkdir hello cd hello lake init hello
# 构建包
lake build
# 运行
lake exec hello # Hello, world!
# 清理构建文件
lake clean
# 更新依赖
lake update
# 运行 lakefile.lean 的脚本
lake run script以上遇到问题欢迎评论讨论~
