Getting started

For a quicker start, see quick-start. For detailed toolchain setup, see installation.

Prerequisites

Encapp resolves foundation by path, so the two repositories must sit side by side:

dev/
├── impl-encapp/
└── impl-foundation/

1. Build the framework

cd impl-encapp
~/.elan/bin/lake build

This does more than compile. Every theorem in the repository is checked here — the refinement proof, the replay laws, the bridge to Foundation.Layer.mono, and every workflow's native_decide. A red build is a failed proof, not just a failed compile.

2. Emit an app

The hello example compiles to all three targets in one command:

~/.elan/bin/lake exe helloapp

Output:

dist/index.html            the web SPA, self-contained (no build step, no framework dependency)
dist/native/app.cjs        the React Native module
dist/desktop/main.cjs      the Electron main process
dist/desktop/preload.cjs   the Electron preload bridge
dist/desktop/package.json  the Electron package manifest

Open dist/index.html in a browser — it needs no server, no bundler and no node_modules.

There are four executables declared in lakefile.lean:

3. Run the gates

node test/hello-matrix.mjs

This is the framework's own end-to-end gate, and it is deliberately broad:

1. lake build Encapp.Examples.HelloWorkflow — the proofs must be current before they are audited.
2. Axiom audit — lake build only warns on sorry, so a keystone could rot to unsound and still build green. axiom-audit.mjs pins each keystone's axiom set with #print axioms and fails on sorryAx or any axiom outside the accepted set. Foundation.Layer.mono is pinned to exactly zero axioms.
3. Coverage gates — page-coverage.mjs, handler-coverage.mjs, nav-integrity.mjs. These are app-generic: the same tools drive the flagship app.
4. lake exe helloapp — emit the artifacts under test.
5. Native parity — core-identity (one step engine, web ≡ native), locatability, input-sync, and seeded differential fuzzing.
6. Replay — the emitted corpus is executed on the happy-dom and headless-Chromium tiers.

See Testing and coverage gates for what each gate catches and why it exists.

4. Write your own app

The shortest complete example is Encapp/Examples/Hello.lean — 177 lines covering three routes, an identity handshake, a composer and two tables. Start by copying its shape:

import Encapp
 
open Encapp Encapp.ViewDsl
 
def myApp : ReflApp Unit where
  init     := { scalars := [("path", .str "/home")], tables := [] }
  pages    := [("/home", box "padding:24px" [ txt "font-size:20px" "Hello" ])]
  handlers := [ ⟨"nav", [ .setInput "path" ]⟩ ]

Then add a main that calls AppGen.emit, and register it in lakefile.lean as a lean_exe. The full walkthrough is in The app model.

Where things live

Recap

• Encapp requires Lean 4.15.0, Lake, Node.js v20+, and impl-foundation as a sibling directory
• lake build proves all theorems and audits axioms; a red build means a failed proof
• One command (lake exe helloapp) emits to three platforms without per-platform build steps
• Test gates validate proofs, coverage, replay across web/native/desktop tiers, and native parity
• Apps start from the hello example (177 lines), extended through AppGen.emit and a main function

Next steps

• The app model — How ReflApp, pages, handlers, and tables fit together
• Testing and coverage gates — What each gate catches and why it exists