Concepts

Compilation pipeline

Syntax is only an entry tree, not domain semantics: Parse → Preflight → Decode → Typed → Semantic → Resolve → Materialize. Any failure fails closed.

Data flow

Author / CI
  │  Lean source + explicit --target / profiles
  ▼
proof-forge-next
  ├─ Lean Parser + portable decoder (+ Syntax preflight)
  │       → Source.Program
  ├─ name / type / effect check
  │       → Typed.Program
  ├─ target-neutral normalization
  │       → Semantic.Program + ProgramRequirements
  ├─ Support resolver (exact SupportClaim, fail closed)
  │       → ResolvedProgram target
  ├─ target Materializer
  │       → target Plan → TargetIR
  └─ emitter
          → OutputSet + provenance (atomic write)
                  │
                  ├─ official packager / validator / local runtime
                  └─ deploy / prove / verify  ← explicit only

Rules

The CLI only parses allowed portable commands; it never elaborates or executes arbitrary Lean commands from user files.
Front-end uses Lean 4 Syntax directly but does not treat the Lean AST as domain semantics.
No best-effort downgrade, no legacy fallback path. Diagnostics are stable.

Pipeline details on GitHub →

Was this page helpful?

Open issue ↗Submit PR ↗Discuss ↗