【亲测免费】 Lean版本管理器（elan）下载及安装教程

1. 项目介绍

elan 是一个用于管理 Lean 定理证明器安装的小工具。它将 lean 和 lake 二进制文件放置在您的 PATH 中，这些二进制文件会自动选择并（如果必要）下载项目 lean-toolchain 文件中描述的 Lean 版本。您还可以使用 elan 命令手动安装、选择、运行和卸载 Lean 版本。

2. 项目下载位置

您可以从以下 GitHub 仓库下载 elan 项目：

GitHub - leanprover/elan

3. 项目安装环境配置

3.1 环境要求

• 操作系统：Linux、macOS、Cygwin、MSYS2、Git Bash
• 依赖：Git（用于通过 lake 下载依赖项）

3.2 环境配置示例

以下是配置环境变量的示例：

# 设置环境变量
export PATH=$HOME/.elan/bin:$PATH

图片示例：

4. 项目安装方式

4.1 Linux/macOS/Cygwin/MSYS2/Git Bash

在终端中运行以下命令：

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

4.2 Windows

在终端（命令提示符或 PowerShell ≥ 7.4.1）中运行以下命令：

curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

4.3 手动安装

您也可以手动下载最新版本的 elan，解压缩并运行安装程序。安装程序会告诉您 elan 将被安装到哪里（默认是 ~/elan），并询问您是否要编辑 shell 配置以扩展 PATH。

5. 项目处理脚本

5.1 安装脚本

以下是 elan 的安装脚本示例：

#!/bin/bash

# 下载并安装 elan
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# 设置环境变量
export PATH=$HOME/.elan/bin:$PATH

# 验证安装
elan --version

5.2 卸载脚本

以下是 elan 的卸载脚本示例：

#!/bin/bash

# 卸载 elan
elan self uninstall

# 清理环境变量
sed -i '/elan\/bin/d' ~/.bashrc

# 验证卸载
elan --version

通过以上步骤，您可以成功下载并安装 elan，并管理 Lean 定理证明器的版本。