effx lift

effx lift --group <id> [--module <file>] [--form verbose|dense|both] [--check] [--emit-patch] [--write <file>] [--json]

From the monorepo root: bun run effx lift --project <tsconfig> --group profile --module src/profile.effx.ts.

Source: scripts/effx.ts, liftCommand and prepareLift in packages/cli/src/lift-command.ts, packages/cli/src/lift.ts, packages/cli/src/lift-check.ts, docs/specs/0019-lift.md. The native child lives in scripts/lift-execution.ts under exception EX-0034 (docs/research/0019-implementation-design.md, "S6 native child custody and EX-0034").

The command reads pure Effect source (HttpApiEndpoint, HttpApiGroup, HttpApi values) and prints an effx declaration that is meant to generate an equivalent group. It never rewrites a user file. By default it runs no application code at all.

FlagsCopy Anchor Link

lift takes the shared project flags (--project, --config, --target, --strict-access) and resolves them with resolveProject. See the CLI overview.

With neither --module nor a configured output module the command exits 1 with error: --module is required: the config declares no lift output module.

Project configCopy Anchor Link

The lift inputs are inert data in effx.config.ts. The CLI never imports or executes anything they name.

import { defineConfig } from "@effx/cli/config";

export default defineConfig({
  lift: {
    rules: [],
    names: {},
    output: { module: "../../src/profile.effx" },
    projections: [],
  },
});

The registry is the selected extension list: Extensions.builtin unless the config adds or replaces extensions. There is no other default registry. The same list drives lift, the printer's recognition rules and the check's compile.

What it printsCopy Anchor Link

Every surface prints the same bytes from one printer. A suggestion in the report, in --json and in a --write file is byte-identical.

Explicit source statuses are preserved, including status: 200; an omitted status stays omitted (spec 0019 section 0.7).

--write accepts one form: --form both with --write is a usage error and creates nothing. The target is refused before any analysis when it exists, and the final write is an exclusive create, so an existing file is never changed.

--checkCopy Anchor Link

The check is the one place lift executes application modules. It runs, per requested form:

overlay → COLLECT → compile → generate (contract) → one witness child → compare

1. A scoped overlay is a throwaway directory holding a copy of the project that owns the group, the verified refactor results (in memory, never the files on disk) and the printed suggestion. node_modules directories on the project's ancestor chain are shared by read-only symlink. Dotenv files, bunfig.toml, .npmrc, .netrc and .git are never copied. Nothing outside the overlay is written.
2. The printed text is collected by the real frontend, compiled with the selected extensions and generated as a contract. The check never reads the in-memory lift.
3. One generated static witness imports the unmodified original group and the generated contract group, mounts each alone on a fresh root that reuses the original root's identity, and reflects both with HttpApi.reflect and OpenApi.fromApi. Registered projections run on both sides.
4. The two reflections are decoded strictly and compared. Only the three deltas of spec 0019 section 2.2 are tolerated: ref-suffix, explicit-default-identifier and endpoint-order. Path, method, schemas, status, headers, media type, security, operation id, summary, description, tags, middleware and access projections must be equal.

The original application root is never replaced or evaluated as part of the comparison. Its middleware, metadata, prefixes and errors stay unverified (spec 0019 section 0.8).

The binding gate is independent evidence. It compares the original model's complete endpoint key set for the group with the generated group's, then typechecks a generated handler skeleton against the actual original root. PASSED needs an actual key proof and an executed zero-exit typecheck receipt; without evidence the binding is MISSING, never accepted.

Check inability is data, never a pass. An application module that throws, prints noise or hangs is reported by stage and error name only: messages, stack frames and values from the application never leave the child.

Execution bounds and environmentCopy Anchor Link

The witness and the binding typecheck run as native Bun children owned by the process root. Each has explicit arguments and working directory, an empty reviewed environment (extendEnv: false: no variable of the invoking shell reaches the child), a 16 MiB capture bound per output pipe, and a forced-stop deadline: 120 seconds for the witness and 600 seconds for the typecheck. The check is not a sandbox. Application imports can perform IO, so run it only on code you would run anyway.

Exit codeCopy Anchor Link

A required source refactor (EFFX3002 to EFFX3004) is an error diagnostic of the lift. With --check both forms and the binding gate can pass and the exit code is still 1: the printed suggestion is not adoptable until the patch (--emit-patch) is applied to the source.

The report is printed before the exit code is raised, through the process's standard output stream, so a report larger than a pipe buffer reaches a slow reader complete. --json prints exactly one line on stdout; diagnostics of a failed analysis go to stderr.