快速开始

安装工具链并把第一个 ProofForge 合约编译为 EVM bytecode

​

前置条件

先安装这些工具：

• 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 的可运行门禁和工具前置条件。