Concepts

Architecture

One portable program source, target-neutral semantics and exact-support resolution, then per-target Plan / IR and artifacts. External packagers, runtimes and networks live outside the compiler boundary.

Layers

Syntax — Lean 4 Syntax as an entry tree only. Not domain semantics.
Source → Typed → Semantic — target-neutral. Must not branch on TargetId.
Resolve — exact SupportClaim resolver, fail closed.
Materialize — target-owned Plan → TargetIR → emitter → OutputSet with provenance.

Repository layout

.
├── ProofForgeV2/    # compiler: Core · Language · Targets · CLI
├── Examples/        # compilable example programs
├── Tests/           # unit / materialization tests
├── docs/            # PRD · architecture · specs · ADR · diagrams
├── scripts/         # CI · clean-room · toolchain · doc checks
├── justfile         # local & CI gate entry
├── active/          # archived v1 tree (research only)
└── AGENTS.md        # control plane for agents / contributors

Boundaries

The compiler is a code-generation and semantic-check tool. It is not an on-chain VM, a key custodian, or a default network executor. build performs no network or key IO.

Full architecture spec on GitHub →

Was this page helpful?

Open issue ↗Submit PR ↗Discuss ↗