安装lean4

突然又想玩lean4了，但是打开vscode之后不知道什么原因，我之前的lean4的环境又不能用了，vscode的自动安装又经常连不上，所以重新安装一次，顺便记录一下。

简介

lean4是一个很神奇的语言，是基于类型论的纯函数语言，用它编写函数需要严格的证明，而且写起来很数学且优雅美观（Unicode显示的符号好评），既能用于正常的编程，又能用于定理证明（或者说正常的编程过程中就需要证明，也算是对于编程者的一种提醒吧）。

好像听说需要安装git，我之前就装有git，不知道没有git能不能使用。

还需要万能的vscode

听说用glean安装可以使用上交大的源来下载，所以下载一个glean

里面选择版本看自己的系统来选，下载完之后解压，应该是有一个README.md和一个可执行文件，如果有点基础的就直接看README.md安装。

首先安装elan，这个是个包管理器。可以在这里看看elan的版本，链接

然后用下面的命令安装elan

1	glean -install elan -version v4.1.2

glean就是之前解压出来那个可执行文件，版本号换成自己需要的，我这里是v4.1.2，注意不要漏了v

接下来是安装lean，这个是编译器还有构建工具，LSP之类的东西，过程同上，先看版本，链接

然后用下面的命令安装lean

1	glean -install lean --version 4.23.0

同理版本号换成自己需要的，这里不需要v。这个文件比较大，可能要等比较久。

首先先使用elan把我们刚刚下载的lean设置为默认版本

1	elan default leanprover/lean4:v4.23.0

可以通过下面的命令查看安装的lean版本以及默认版本

elan show

设置完lean之后我们可以来创建一个lean项目来看看，我们可以使用lake命令来创建和管理项目或许是lean make的缩写呢

可以使用下面的命令创建项目

1	lake new 你的项目名字

然后用vscode打开，它应该已经提示你装lean的插件了，如果没有就自己搜索一下，这个插件

装完之后打开Main.lean，右边应该有一个界面，像这样

然后来简单的查看一下输出，在下面加上一行

1	#eval main

#是指令的开头，eval是求值的意思，在你输入完的时候应该就能在旁边看见输出了，所见即所得，实时反馈，这也是为什么我要在自己电脑上安装，而不是使用网页版的主要原因，网页版太卡了。

然后注意看vscode中的插件的图标这里，点了有一些选项，大家可以自己熟悉一下

作为安装教程，知道这些应该已经够用了，剩下的大家去看看中文文档，文档写得已经很好了，下一篇文章我就写一个简单的使用。