Installation

The Encapp framework compiles to verified proofs and emits static SPAs that need no runtime framework dependency. Each step is deliberately designed to catch failures early — the build enforces theorems, and the gates check coverage, parity, and replay fidelity.

Prerequisites

Directory structure

Encapp resolves the foundation dependency by relative path, so both repositories must sit side by side:

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

If impl-foundation is elsewhere, lake build will fail with an unresolved import.

Install elan and Lean

Download and install elan, then let it install the pinned toolchain:

curl -sSf https://elan-lang.org/elan-init.sh | sh
cd impl-encapp
~/.elan/bin/lake build

The lean-toolchain file specifies leanprover/lean4:v4.15.0. Elan reads it and downloads the exact toolchain the framework was tested against.

The four lake executables

Every executable is declared in lakefile.lean and rooted at a different module. They emit different things from the same framework:

Build and emit

Build the framework (all theorems must check):

~/.elan/bin/lake build

A red build is a failed proof, not just a failed compile. The framework is not statically typed in the traditional sense — it is formally verified. If the build succeeds, every theorem holds.

Emit the hello app to all three platforms:

~/.elan/bin/lake exe helloapp

Output:

dist/index.html            Web SPA (self-contained, no bundler, no server needed)
dist/native/app.cjs        React Native module
dist/desktop/main.cjs      Electron main process
dist/desktop/preload.cjs   Electron preload bridge
dist/desktop/package.json  Electron manifest

Open dist/index.html in any browser — it is a fully functional static file.

Run the gates

The framework's end-to-end verification:

node test/hello-matrix.mjs

This one command runs:

1. Proof check — lake build ensures all theorems hold.
2. Axiom audit — verifies keystones carry no sorry and no rogue axioms (see Axiom hygiene below).
3. Coverage gates — ensures every page, handler, and nav target is tested by a workflow.
4. Artifact emit — lake exe helloapp builds the SPA.
5. Native parity — core-identity (web ≡ native), locatability, and input-sync.
6. Replay — executes the corpus on happy-dom, headless Chromium, React-Native, and Electron.

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

Troubleshooting

Stale-link linker errors

After moving or adding definitions in a module, lake exe helloapp can fail with a linker error even though lake build succeeded:

ld.lld: error: undefined symbol: l_Super_App_app
Some required builds logged failures: - Super.Screens:c.o

This happens because Lake's incremental build cache references stale object files. The fix is to clean and retry:

~/.elan/bin/lake clean
~/.elan/bin/lake exe helloapp

If the error persists, check the module name in the error message — it may indicate a genuine source error masked by the stale link.

Axiom hygiene

lake build accepts proofs containing sorry (it only warns), so a keystone could rot to unsound and still build green. The gates catch this with an axiom audit:

node test/axiom-audit.mjs . Encapp.Examples.hello_reflected_matches Lean.ofReduceBool

This runs #print axioms on each keystone and fails if it sees sorryAx or any unexpected axiom. The framework allows:

• Lean.ofReduceBool — legitimately introduced by native_decide proofs
• propext, Classical.choice, Quot.sound — standard propositional axioms
• Nothing else

Any other axiom in a keystone is a regression — the proof has drifted.

Recap

• Install elan, which reads lean-toolchain and installs the exact Lean version the framework was tested against.
• Place impl-foundation as a sibling directory — it is a compile-time dependency, not a runtime one.
• lake build compiles the framework and checks all theorems; a red build is a failed proof.
• lake exe helloapp emits a self-contained SPA to dist/index.html.
• node test/hello-matrix.mjs runs the full verification suite: proofs, coverage, parity, and replay.
• If lake exe fails with a linker error after moving definitions, run lake clean and retry.
• If a keystone gains sorry, the axiom audit will catch it and fail.

Next steps

• Read The app model to understand how to write your own Encapp app.
• Explore Workflows and proofs to see how a single definition becomes both a theorem and a cross-platform test.
• Check What is proven (and what is not) to understand the boundary between verified and empirical guarantees.