安装Lean

(updates in 2023.09.17)

本教程演示在Windows系统下如何安装Lean 4正式版。Linux和MacOS版本请参考Lean Manual。

如果你身在中国,在运行安装程序前需要做如下准备:

在系统目录C:\Windows\System32\drivers\etc文件夹下找到hosts文件。对于其它系统用户也都是找到各自系统的hosts文件。

这个文件需要管理员权限来修改,有一个简便方法是,把它复制到别的地方修改,然后再粘贴回去,并选择使用管理员身份继续。

用记事本打开这个文件,在最后一行写入185.199.108.133 raw.githubusercontent.com

重启电脑,然后开启科学上网。(注意,你需要让终端也处在梯子的作用域中,例如你使用clash类梯子需要打开全局模式。)

(经过这个步骤之后你也可以使用官网提供的方法来安装了。)

如果你遇到"SSL connect error", "Timeout was reached","Failed to connect to github.com port 443"...等错误,就是说明你的网络环境有问题。重启电脑或者检查你的梯子。

基本安装

所有受支持平台的发布版本都可以在https://github.com/leanprover/lean4/releases中找到。

  1. 使用Lean版本管理器elan代替下载文件和手动设置路径。

    在elan的Github仓库中下载最新release(对于windows,请下载elan-x86_64-pc-windows-msvc.zip),解压运行elan-init.exe,按照指示安装。

    默认安装位置是用户文件目录下的.elan文件夹,添加环境变量你的用户文件目录\.elan\bin

    可能出现以下报错无法加载文件……因为在此系统上禁止运行此脚本”。解决方案是

    1.用管理员身份运行Powershell;

    2.输入命令set-Executionpolicy Remotesigned,选择Y

    然后就可以正常使用了。考虑到系统安全性,建议安装完成后将该选项改回默认值N

    效果如下图

    setuplean

    由于本网站无法提供讨论区,欢迎向译者提供新的报错和解决方案,以丰富本页面。可邮件至subfishzhou@gmail.com

  2. 安装git。安装 VS Code,并安装lean4扩展。

    installing the vscode-lean4 extension

  3. 在终端中运行

    $ elan self update  # 以防你下载的不是最新版elan
    # 下载及应用最新的Lean4版本 (https://github.com/leanprover/lean4/releases)
    $ elan default leanprover/lean4:stable
    # 也可选择,只在当前目录下使用Lean4
    $ elan override set leanprover/lean4:stable
    
  4. 创建一个以 .lean 为扩展名的新文件,并写入以下代码:

    #eval Lean.versionString
    

    你会看到语法高亮。当你把光标放在最后一行时,在右边有一个“Lean信息视图”,显示已经安装的Lean版本。

    successful setup

创建新Lean项目

用VS code打开一个新文件夹,你可以用两种方式创建新工程。

  1. 在终端中运行(<your_project_name>替换为你自己起的名字)

    lake init <your_project_name>
    

    以创建一个名为your_project_name的空白新工程。如果你想把你的Lean程序编译成可执行文件,在终端中运行lake build命令。

    如果你想在这个现有的工程中引用Mathlib4,你需要在lakefile.lean文件中加入

    require mathlib from git
        "https://github.com/leanprover-community/mathlib4"
    

    然后在终端中运行

    curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
    
  2. 如果你想直接创建一个引用Mathlib4的新工程,在终端中运行

    lake +leanprover-community/mathlib4:lean-toolchain new <your_project_name> math
    

    以创建一个名为your_project_name的新工程。

使用Mathlib

更多内容请参考Mathlib Wiki

在你的项目文件夹下打开VS code,使用终端运行

lake update
lake exe cache get

如果你看到终端中显示了类似如下的提示:

Decompressing 1234 file(s)
unpacked in 12345 ms

同时你的项目文件夹中出现了lake-packages文件夹,那么证明你安装Mathlib成功了,重启系统即可使用。注意:你要在lake-packages所在的目录中运行VScode,才能让Lean使用Mathlib。

这里提供一个实例来测试你的安装:

import Mathlib.Data.Real.Basic
example (a b : ℝ) : a * b = b * a := by
  rw [mul_comm a b]

如果你的Lean infoview没有任何报错,并且光标放在文件最后一行时会提示“No goals”,证明你的Mathlib已经正确安装了。

如果你想更新Mathlib,在终端中运行

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update
lake exe cache get