请求添加 Lean4 相关镜像 #425
Description
先决条件 (Prerequisites)
-
我已确认这个镜像源从未在 其他 issues 中讨论过。
I have checked that this repository has not been discussed in other issues. -
我已仔细阅读 请求新镜像前必读。
I have CAREFULLY read the mirroring rules.
项目介绍 (Project introduction)
Lean 是微软研究院在 2013 年推出的计算机定理证明器.Lean4 于 2021 年发布，为 Lean 定理证明器的重新实现，能够生成 C 代码后进行编译，以便开发高效的特定领域自动化。Lean 作为一门独特的语言，兼具数学和编程两方面的特性。作为交互式定理证明器，Lean 提供了严格的逻辑框架，数学家可以将数学定理转换成代码，并严格验证这些定理的正确性。作为通用函数式编程语言，它具有依赖类型的严格的纯函数式语言性质。这些特性让 Lean 在数学和计算机科学研究中非常有用，它可以帮助研究人员发现并纠正概念上的错误，同时加深他们对研究对象的理解。
将数学及其他学科的各种定理（逻辑系统）进行形式化历来都是理论计算机科学的重要课题，在近几年，随着大模型等技术的发展，Lean4 更是在 ai4math 领域体现出了独特的重要性。从 AlphaProof 到最新的 Seed-Prover, 主流的 ai4math 路径仍是将大模型及其他机器学习技术结合 Lean4 的反馈。而 Lean4 活跃的社区更是始终在推动着科学、教育等各种领域的发展。
上游地址与镜像方法 (Upstream & mirroring method)
对于当前 Lean4 的主要应用场景而言，需要镜像的环节分为三个部分
1. 构建后 github release 中的 elan 与 lean (toolchain) 二进制文件
https://github.com/leanprover/elan/releases
https://github.com/leanprover/lean4/releases
其中 lean4 toolchain 文件本身每次 release 总文件大小约在 5G 左右（单文件 0.5G)。
鉴于 Lean4 本身版本迭代快速的特性，可以选择保留最新几个版本和特殊版本以减少存储占用
2. Reservoir 中记录的 git 仓库
Lean4 的包管理工具 lake 在解析配置文件时，会从 Reservoir 网站获取实际的 github 仓库地址.
其依赖的注册表文件定时更新在 https://github.com/leanprover/reservoir-index.
通过类似 https://github.com/EricTianC/reservoir-mirror 中的方法
自行实现对应的 reservoir server api 服务对目标 gitUrl 进行修改，配合 lake 读取的环境变量 “RESERVOIR_API_URL” 即可实现镜像站的切换。
reservoir-index 只自动收录 github 上所有 star 大于 2 的 Lean4 项目并建立索引。由于现有的 Lean4 应用场景仍集中于数学、计算机等领域的形式化验证，绝大多数的仓库体积很小。仅数个具有较高官方性质的项目具有较大体积。同时若只需涉及定理证明，也可将镜像内容限定为其中的几个仓库。不过，就目前以及数月内的实际情况而言，所需镜像的 github repo 总体积应在 20G 以内.
3. Mathlib 的 cache 脚本中生成并发布的 cache
该部分文件目前以 s3 形式存储，暂时硬编码于 Mathlib 对应的 Cache 逻辑中
https://a09a7664adc082e00f294ac190827820.r2.cloudflarestorage.com/mathlib4
其每版文件大小与 1 相近，发版频率显著高于 1
镜像大小 (Mirror size)
暂无现有的镜像同步脚本，就目前所需而言，100 G 以内的镜像内容应该可以显著改善创建 Lean4 定理证明项目时的体验
备注 (Note)
国内已有 stju 的 Lean4 相关镜像。但是其仅在环节 1 部分做到了最低的可用性。
在建立定理证明项目时，必要的步骤是拉取 Mathlib4 及相关依赖，以及对应的构建缓存
对环节 3 而言，stju mirror 中没有相应镜像
对环节 2 而言，stju mirror 中只建立了 Mathlib4 依赖的仓库的镜像，且与 lake 本身配置文件脱钩，需要使用 stju 自行编写的 glean 脚本进行使用。
同时，查看 https://mirrors.sjtug.sjtu.edu.cn/ 可以发现， stju 中的相关仓库长时间（高频率）处于同步失败状态，且同步失败时无法正常使用