Build targets and CLI

Lake targets

Declared in lakefile.lean:

@[default_target]
lean_lib «Encapp» where
  globs := #[.andSubmodules `Encapp]
 
lean_exe «encapp»     where root := `Main
lean_exe «hellocheck» where root := `HelloCheck
lean_exe «helloapp»   where root := `HelloApp
lean_exe «emulator»   where root := `EmuGenMain

Command	Produces
`lake build`	compiles the library and checks every theorem
`lake build Encapp.Examples.HelloWorkflow`	just the workflow module and its proofs
`lake exe helloapp`	`dist/index.html`, `dist/native/app.cjs`, `dist/desktop/*`
`lake exe emulator`	the ENC emulator SPA
`lake exe encapp`	the counter SPA via `Codegen.emit`
`lake exe hellocheck`	hello's final state as JSON on stdout

Lake lives at ~/.elan/bin/lake in a standard elan install; the test harnesses use that path.

A red lake build is a failed proof, not merely a failed compile.

Running Lean scripts

The emit scripts under test/ are Lean programs run through lake env:

~/.elan/bin/lake env lean --run test/emit-hello-corpus.lean > /tmp/corpus.json
~/.elan/bin/lake env lean --run test/emit-pages-nav.lean
~/.elan/bin/lake env lean --run test/emit-handlers.lean
~/.elan/bin/lake env lean --run test/emit-core.lean

These are how the app-generic tools read a specific app's reflected data: each app supplies its own emit script, and the tool takes the script path as an argument.

Test entry points

Everything

node test/hello-matrix.mjs

Proof build → axiom audit → coverage gates → emit → native parity → fuzz → replay.

Soundness

node test/axiom-audit.mjs <repo> <module> <decls> <extra-allowed-axioms>

Fails on sorryAx or any axiom outside the accepted set. lake build only warns on sorry, so without this a keystone could rot to unsound and still build green.

Coverage

node test/page-coverage.mjs    <appDir> <emit-pages-nav> <emit-corpus>
node test/handler-coverage.mjs <appDir> <emit-handlers>  <emit-corpus>
node test/nav-integrity.mjs    <appDir> <emit-pages-nav>

App-generic — the same tools drive hello and the flagship app.

Replay

node test/encapp-replay-dom.mjs      <distDir> <corpus.json>   # happy-dom
node test/encapp-replay.mjs          <distDir> <corpus.json>   # headless chromium
node test/encapp-replay-rnweb.mjs    <distDir> <corpus.json>   # react-native-web
node test/encapp-replay-electron.mjs <distDir> <corpus.json>   # real electron

Native parity

node test/native-core-identity.mjs
node test/native-locators-hello.mjs
node test/native-input-sync.mjs
node test/fuzz-parity.mjs 314159,1,42,303,424242,16180

Desktop

node test/electron-smoke.mjs

Emitted layout

dist/
├── index.html              the web SPA (self-contained)
├── native/
│   ├── app.cjs             the React Native module
│   ├── boot.web.js         the RN-web boot shim
│   ├── bundle.web.js       the RN-web bundle
│   └── index.rnweb.html    the RN-web harness page
└── desktop/
    ├── main.cjs            the Electron main process
    ├── preload.cjs         the preload bridge
    └── package.json        the package manifest

dist/ is emitted output. Everything in it is reproducible from lake exe.

Repository layout

Path	What
`Encapp/`	the framework
`Encapp/Examples/`	Counter, Hello, HelloWorkflow
`test/`	replayers, gates, audit, fuzz harness
`compat/`	the oracle diff against the reference implementation
`docs/`	this site
`docs-internal/`	earlier long-form notes and platform progress logs
`dist/`	emitted artifacts

Prerequisites recap

Lean leanprover/lean4:v4.15.0 via elan (pinned in lean-toolchain)
Node.js v20+
impl-foundation checked out as a sibling directory — lakefile.lean requires it by path