lean4与lean4game的使用记录

Posted on | In

lean4与lean4game的使用记录

lean4我至少去年就听说过.事实上,我高二在某个网站上玩过Lean4Game中的自然数关卡(然而存档丢了).现在高中毕业了,某个qq群的讨论使我重新想起了这个东西.并且被推荐了另一个游戏.于是我终于开始尝试下载它了.昨天在Ubuntu上装了一天没成功,今天在Windows上搞定了.其中最大的折磨是网络--我暂时没有梯子.

注:本人不对任何按照我列举步骤操作但是没成功(在某一步卡住)的事负责.因为归根到底我也就是个初学者.我只描述我是怎么安装的.

Lean4的安装(Windows)

  1. 根据大部分的指南,安装过程中需要先行装好VSCode和Git,这两个我都有了.

  2. 在VSCode中打开extensions,安装Lean4.

  3. 打开github,下载elan(windows用户要下载的是那个elan-x86_64-pc-windows-msvc.zip)

  4. 解压,有一个elan-init.exe.不要直接双击.在当前文件夹打开终端,输入.\elan-init.弹出来"Welcome to Lean!"以及一大串其他东西,此时回车,界面会卡住一段时间,不用害怕.等待就行了.直到看到"Elan is installed now, Great!"什么的,说明这一步成功了.保险起见再elan --version一下也行.

  5. 下一步和其他攻略中有点区别.因为我的目的是玩lean4game,而我想玩的游戏只支持lean4 v4.7.0,这个版本有点太早了,镜像站没有.但是我的网络状况不支持我从github上直接下载这个版本,所以我用了代理加速网站.从github上下载了一份lean--windows.zip.

  6. 接下来是一串奇异搞笑的操作:本来我应该用glean下载lean和elan,但是都没成功,elan show卡住了,估计是在尝试下载lean.于是我决定直接伪造结果:我在~\.elan中新建了文件夹toolchains,并把我刚才下载的lean--windows.zip解压到里面.然后把文件夹名字改成了leanprover--lean4---v4.7.0(前面两个-,后面三个-).注意,现在的文件结构应该类似于这样: 

    ~\.ELAN
    ├─bin
    └─toolchains
        └─leanprover--lean4---<你的版本号>
            ├─bin
            ├─include
            ├─lib
            │  └─...
            ├─share
            │  └─...
            └─src
               └─...

如果和这个不一样自己对着修改.主要是bin -> toolchains -> leanprover--lean4---<...>不能错.

  1. 此时还不能直接elan show.要把刚才装的leanprover指定为默认版本. 在终端输入命令elan default leanprover/lean4:<你安装的版本>.

  2. 接下来应该已经成功了.你可以用lean --version和lake --version验证一下.