跳转到主要内容

​
前置条件

先安装这些工具：
  • elan — Lean 工具链管理器（使用仓库里 lean-toolchain 锁定的版本）。
  • just — 命令运行器，来自 casey/just。
  • solc（0.8.30）和 Foundry（forge/cast/anvil）— 只有 EVM target 需要。

​
构建

git clone https://github.com/DaviRain-Su/proof_forge.git
cd proof_forge
elan toolchain install "$(cat lean-toolchain)"
lake build
根目录 justfile 是面向开发者的命令目录和 CI 入口： 
just --list        # 所有 recipe
just build         # lake build
just check         # 快速静态门禁（Lean + EVM + Psy）
just evm-all       # 完整 EVM 门禁：示例编译、Foundry 冒烟、Anvil 部署
just ci            # 本地跑完整 CI 序列

​
编译合约

把 EVM Counter 示例编译为运行时 bytecode： 
lake env proof-forge --evm-bytecode --root . --module contract \
  -o build/evm/Counter.bin Examples/Evm/Contracts/Counter.lean
从内置的 portable IR fixture 产出其他目标的制品： 
lake env proof-forge --emit-counter-emitwat -o build/wasm-near   # NEAR Wasm
lake env proof-forge --solana-elf -o build/solana/counter.so     # Solana ELF
lake env proof-forge --emit-counter-ir-psy -o build/psy/Counter.psy
lake env proof-forge --emit-counter-ir-leo -o build/aleo         # Aleo Leo
lake env proof-forge --emit-counter-ir-ts -o build/ts/Counter.ts # CF Workers
Lean 命令必须通过 lake env ... 运行，这样工具链环境才会被正确设置。

​
下一步

入职指南

完整本地环境、编辑器配置和最小验证循环。

架构

编译器如何把 Lean 源码降级为链原生制品。

后端状态

哪些 target 是成熟、实验或研究阶段。

验证门禁

每个 target 的可运行门禁和工具前置条件。