Skip to content
Logo

FAQ and troubleshooting

The framework catches many defects at compile time, but not all problems emit compiler errors. This page is grounded in actual failure modes encountered during development, with the source files you can read to understand the root cause and how the gates prevent regress.

I hit "undefined symbol" from the linker, but lake build <module> succeeds

Root cause: After a module gains or moves definitions, incremental builds can fail with a linker error that names a module but points nowhere in its source.

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

The module's source is fine. The issue is stale object files left by the incremental build system.

Solution: Run npm run build — build.mjs detects whether Lean reported an actual source error (file and line) or a phantom linker error. If it's phantom, it runs lake clean and retries. See /home/basque/dev/impl-super-encapp/build.mjs for the detection logic (it reads both stdout and stderr looking for \.lean:\d+:\d+:).

Why this happens: Lean's lake build system records module dependencies based on the definitions it sees at build time. When you add a definition to a module or move it, the .o files downstream can reference a symbol that no longer exists at the old address, even though lake build <that one module> recompiles it correctly. Running the full build (lake exe super) links against stale .o files from upstream modules.

Silently cleaning would hide real compile errors (making a typo take four minutes to see), so the build script prints real errors and exits non-zero, only cleaning on phantom linker errors.

My proof passes but the shipped app doesn't work — it's using old code

Root cause: There are two independent staleness holes:

  1. Adapter staleness: You edit adapter/enc-entry.mjs, run the test suite, and it all goes green. But the shipped HTML (dist/index-live.html) still <script src>s the old dist/adapter.bundle.js.

  2. Binding staleness: You edit Super/App.lean, run the probe tests, and they all pass. But they're asserting against the OLD declared binding read from a stale dist/index.html.

Both are file-timestamp-detectable.

Solution: Before running tests or probes, run:

npm run build        # regenerates index.html + adapter.bundle.js
node test/bundle-fresh-check.mjs  # fails if artifacts are stale relative to source

The check script is in /home/basque/dev/impl-super-encapp/test/bundle-fresh-check.mjs. It compares mtime of:

  • Super/App.lean vs dist/index.html
  • Every file in adapter/ vs dist/adapter.bundle.js

Why this exists: Probes and tests import adapter/enc-entry.mjs (the source), but the app loads the emitted bundle. A divergence between the two is invisible to the test suite because the suite exercises the source adapter directly. The replayers load the bundle, so they see the old code.

My workflow proof holds, but it fails when I replay it

Root cause: The proof tier and the execution tier are two different claims, both necessary but not identical:

  • Proof: Workflow.holds app w = true by native_decide — the Lean interpreter and the app logic agree on the post-conditions.
  • Execution: The same workflow replayed on real UI runtimes (happy-dom, headless Chromium, Electron) — the JS runtime and the Lean interpreter agree empirically.

The proof says nothing about whether the emitted JavaScript matches the Lean interpreter. That match is checked empirically, not proven.

What it means: If a proof passes but the replayer fails, the likely causes are:

  1. JS runtime divergence — the emitted code does something the Lean interpreter doesn't, or vice versa. See /home/basque/dev/impl-encapp/test/fuzz-parity.mjs for differential fuzzing across runtimes (seeded regression tests that each caught a distinct divergence class).

  2. Adapter gap — the adapter implements the store seam but is hand-written. If the adapter violates the HostBinding protocol (e.g., doesn't call onChange when the app mutates the store), the proof can pass while the replayer sees stale state. See Host bindings for how to move policy out of the adapter and into declared bindings.

  3. Multi-user or persistence gap — the proof tier is single-Doc logic (one app instance, no cross-user state, no reload). If your workflow requires two app instances or multi-enclave sync, the proof is out of scope. That story lives in the node layer. See What is proven for the honest boundary.

How to debug: Run the same workflow on all four replayers and see which ones fail:

npm run replay:dom   # happy-dom, fastest, no real browser
npm run replay:hl    # headless Chromium, real browser engine
npm run replay:rn    # React Native (native simulator if available)
npm run replay:e2e   # Electron, if in CI environment

If only the headless Chromium run fails, the bug is probably in the JS emitter or a browser-specific edge case. If the dom replayer passes but Electron fails, it's likely native code or a native binding issue.

The replayer crashes with "no such file" for webkit libraries

Root cause: Playwright (the replayer's browser driver) tries to launch Webkit (Safari's engine) but the system does not have the required host libraries installed.

Error: browser launch failed
... missing libgstreamer...

Solution: Use chromium or firefox instead:

npm run replay:hl -- --browser chromium    # works out of the box
npm run replay:hl -- --browser firefox     # also works, usually
# npm run replay:hl -- --browser webkit   # requires webkit development headers

The replayer defaults to chromium. See test/encapp-replay.mjs for the Playwright configuration.

Why this matters: Webkit (Safari's engine) requires system development libraries (libgstreamer-plugins-base, libgstreamer, libharfbuzz, etc.) that are not present on all CI runners. Chromium and Firefox ship as portable binaries and work out of the box. If you need Webkit coverage, you must provision those libraries on the runner or use a base image that includes them.

My axioms look wrong in the build output, or I see sorryAx

Root cause: lake build allows sorry in proofs (it's only a warning), so a keystone proof could rot to unsound and still build green. Keystones like Foundation.Layer.mono are the foundation of the whole framework, so rotting one is a showstopper.

Solution: The soundness gate runs first in the test suite:

node test/axiom-audit.mjs . Encapp.Core Foundation.Layer.mono ''

This fails immediately if:

  • The module contains sorryAx (an unsound axiom)
  • The module uses an axiom outside the accepted set (pinned per module)

It must run before any proof is trusted. See /home/basque/dev/impl-encapp/test/README.md under "Soundness gate" for the full inventory.

Why it's automated: The audit uses #print axioms to extract the exact axiom set at build time, so if a maintainer accidentally adds an axiom without updating the gate, the test fails. You cannot commit a gate-breaking change.

Foundation is in the parent directory, but lake can't find it

Root cause: The foundation library (Enc.Foundation or similar) must be a sibling checkout — at the same depth as impl-encapp, not nested inside it.

If your directory structure is:

my-project/
  impl-encapp/  ← you are here

Then foundation is not accessible.

Correct structure:

my-workspace/
  foundation/         ← must be here, sibling to impl-encapp
  impl-encapp/        ← you are here
  impl-super-encapp/  ← optional, also works as sibling

Solution: Check your lakefile.lean. It should declare the dependency with a relative path:

require foundation from "../foundation"

If foundation is not checked out as a sibling, clone it:

cd ../
git clone <foundation-repo>
cd impl-encapp
lake build  # should find ../foundation now

Why this matters: lake resolves relative paths from the workspace root. If you nest foundation inside impl-encapp or put it elsewhere, lake cannot find it and the build fails with a cryptic "package not found" error.

How do I run the whole verification suite?

Command:

npm run verify        # lint + smoke + units + web build + bundle-size budget

Equivalently, step by step:

npx eslint .          # lint (must pass with --max-warnings 25)
npm run test          # smoke + algebra + units (27 + 25 = 52 tests)
npm run build         # Vite production build
node test/bundle-fresh-check.mjs  # bundle artifacts vs sources (mtime check)

The most useful subset for rapid iteration:

npm run build         # ~1s, catches app.lean + adapter drift
npm run test:workflows # ~8s, proves + replays the whole corpus

If anything fails, stop and fix it before committing. The test invariants (27 algebra checks + 25 unit tests passing, both bundles compiling, no axiom rot) are gates on every commit.

Recap

  • Stale links: lake clean before retrying if a linker error disappears after clean.
  • Stale bundles: Run npm run build before testing; bundle-fresh-check.mjs catches divergence.
  • Proof vs runtime: Proofs are Lean theorems; runtime matching is empirical (four independent replayers).
  • Single-Doc boundary: Proofs do not cover multi-user, persistence, or cross-enclave logic.
  • Axiom rot: axiom-audit.mjs must pass; sorry is permitted but audited.
  • Foundation location: Must be a sibling checkout, not nested.
  • Webkit failures: Use chromium or firefox if webkit libraries are unavailable.

Next steps

  • Read What is proven for the formal boundary and the theorems you get.
  • See Host bindings if your adapter needs to expose store policy.
  • Check test/README.md for the full gate hierarchy (proof tier, coverage gates, axiom audit, native parity).