> ## Documentation Index
> Fetch the complete documentation index at: https://gradiences.mintlify.site/llms.txt
> Use this file to discover all available pages before exploring further.

# 快速开始

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

## 前置条件

先安装这些工具：

* **`elan`** — Lean 工具链管理器（使用仓库里 `lean-toolchain` 锁定的版本）。
* **`just`** — 命令运行器，来自 [casey/just](https://github.com/casey/just)。
* **`solc`**（0.8.30）和 **Foundry**（`forge`/`cast`/`anvil`）— 只有 EVM
  target 需要。

## 构建

```sh theme={null}
git clone https://github.com/DaviRain-Su/proof_forge.git
cd proof_forge
elan toolchain install "$(cat lean-toolchain)"
lake build
```

根目录 `justfile` 是面向开发者的命令目录和 CI 入口：

```sh theme={null}
just --list        # 所有 recipe
just build         # lake build
just check         # 快速静态门禁（Lean + EVM + Psy）
just evm-all       # 完整 EVM 门禁：示例编译、Foundry 冒烟、Anvil 部署
just ci            # 本地跑完整 CI 序列
```

## 编译合约

把 EVM Counter 示例编译为运行时 bytecode：

```sh theme={null}
lake env proof-forge --evm-bytecode --root . --module contract \
  -o build/evm/Counter.bin Examples/Evm/Contracts/Counter.lean
```

从内置的 portable IR fixture 产出其他目标的制品：

```sh theme={null}
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
```

<Tip>
  Lean 命令必须通过 `lake env ...` 运行，这样工具链环境才会被正确设置。
</Tip>

## 下一步

<CardGroup cols={2}>
  <Card title="入职指南" icon="door-open" href="/zh/onboarding">
    完整本地环境、编辑器配置和最小验证循环。
  </Card>

  <Card title="架构" icon="sitemap" href="/zh/architecture">
    编译器如何把 Lean 源码降级为链原生制品。
  </Card>

  <Card title="后端状态" icon="circle-check" href="/zh/backend-status">
    哪些 target 是成熟、实验或研究阶段。
  </Card>

  <Card title="验证门禁" icon="shield-halved" href="/zh/reference/validation-gates">
    每个 target 的可运行门禁和工具前置条件。
  </Card>
</CardGroup>