CLI Reference

The sema command is the entire toolchain. This page is the exhaustive per-command reference, verified against the binary. For a task-oriented tour see Toolchain; for the verification model behind assure see Verification.

Running sema with no arguments prints the command list:

usage: sema <tokens|parse|check|run|circuit|debug|infer|doc|assure|repl|dap|add|remove|list|lsp> <args>

Most commands take a project directory — the folder that contains src/. sema check, sema parse, and sema tokens also accept individual files.

No sema test or sema fmt

There is no separate test subcommand: authored test "…": blocks run through sema assure, which is the verification entry point. Source formatting (sema fmt) is planned but is not yet a standalone command; use sema parse --ast to inspect structure in the meantime.

Summary

Command	Synopsis	What it does
check	sema check <project | files…>	Static checks: parse, arity, struct fields, effect-row discipline, unrecognized-directive and policy-example warnings.
run	sema run <project>	Execute main(). Honors SEMA_STRICT=1 and SEMA_VM=1.
circuit	sema circuit <run|resume|list|show|cancel>	Durable runs: run executes like sema run; resume/list/show/cancel manage recorded runs under .sema/runs/.
debug	sema debug <serve|run|replay>	Localhost token-protected run-inspector web UI; replay verifies determinism against a recorded run.
assure	sema assure <project> [--grade bronze|silver|gold]	Verification engine: test blocks, fuzzed ensure properties, mutation testing at gold.
doc	sema doc <project> [--out DIR] [--skills] [--html]	Reflected documentation from signatures + docstrings.
parse	sema parse <files…> [--ast]	Parse; --ast dumps the parse tree.
tokens	sema tokens <files…> [--quiet]	Dump the lexer token stream.
repl	sema repl [project]	Interactive console (:doc, :trace, :q).
infer	sema infer --gguf … --tokenizer … [--prompt …]	Real local GGUF inference (needs the real-model build).
add / remove / list	sema add <pkg | path | git+url>	Package management (PyPI + native Sema packages).
lsp / dap	sema lsp · sema dap	Language server and debug adapter for editors.
--version	sema --version	Print the version.

sema check

sema check <project-dir | files...>

The fast, run-after-every-edit command. It parses the target and runs the static checks without executing anything: parse errors, function arity, struct fields, literal and return-type mismatches (both sides certain), the effect-row discipline, unrecognized-directive warnings (a directive in a def body that no runtime handler recognizes — the guard against silent no-ops), and policy-example verification (a policy whose examples: contradict its rules).

A directory is checked as a project; a non-directory argument is checked as a file, so you can point it at one module.

sema check myproject
sema check src/main.sema src/domain.sema

Warnings alone (for example, a bronze !{*} escape hatch) do not fail the check; any error returns a non-zero exit code. A clean run prints [sema] check: no problems found.

sema run

sema run <project-dir>

Executes the project’s main() on the tree-walking interpreter — the reference semantics — and writes a run journal (its path is printed on completion).

sema run myproject

Two environment variables change its behavior:

• SEMA_STRICT=1 turns recoverable degradations into hard, typed errors. With it off, the runtime self-heals a mis-estimate or a failed step, logs it to the journal and to stderr ([sema:warn] … (recovered; set SEMA_STRICT=1 to fail hard)), and keeps going. With it on, each such degradation aborts loudly — use it when verifying, in tests, and in CI.

  SEMA_STRICT=1 sema run myproject

• SEMA_VM=1 runs compilable function bodies on the opt-in bytecode VM instead of the tree-walker. The VM compiles a function only if every construct in its body is supported, and otherwise falls back transparently; value operations delegate to the same runtime helpers, so results are identical. It is a performance path, not a different language.

  SEMA_VM=1 sema run myproject

sema circuit

sema circuit <run|resume|list|show|cancel>

Durable, resumable runs. sema circuit run <project> executes the project like sema run while recording a durable run under .sema/runs/; resume picks a recorded run back up, and list / show / cancel manage the recorded runs.

sema circuit run myproject
sema circuit list myproject

sema debug

sema debug serve <run-dir | project-dir> [--latest] [--port N]
sema debug run <project-dir> [--port N]
sema debug replay <project-dir> --against <run-dir>

The run inspector — a localhost, token-protected web UI over a run’s journal. serve inspects an existing run directory (or a project’s runs, --latest for the most recent); run executes the project and serves the inspector for the fresh run; replay re-executes the project and verifies determinism against a previously recorded run.

sema debug serve myproject --latest
sema debug replay myproject --against myproject/.sema/runs/<run-id>

sema assure

sema assure <project-dir> [--grade bronze|silver|gold]

The verification engine. Verification is default-on in Sema — there is no opt-in testable keyword — and assure is where the grades run. --grade defaults to silver. It runs three things, gated by grade:

• Tests — every test "name": block runs; a block that finishes without a contract violation or error passes.
• Properties — every function with an ensure postcondition is fuzzed: inputs are generated from the parameter types and the function is called many times; a violated ensure is reported with a concrete counterexample.
• Mutation adequacy (grade gold only) — the program is systematically mutated and the tests and properties re-run against each mutant; the killed/total score is reported as a percentage.

Grades set the depth:

Grade	Runs	Notes
bronze	tests	effect-row inference allowed
silver	tests + fuzzed properties	requires an explicit effect row on every declared function
gold	+ mutation adequacy	the strongest gate

sema assure myproject                 # defaults to silver
sema assure myproject --grade gold

The output lists tests passed, properties held (with any falsifying counterexample), and, at gold, the mutation score; the exit code reflects the PASS/FAIL verdict, so assure slots straight into CI.

sema doc

sema doc <project> [--out DIR] [--skills] [--html]

Generates Markdown documentation by reflecting over the program and merging in the docstrings you write inline. A docstring is a triple-quoted string as the first statement of a module, def, struct, or enum — no per-line marker. Reflection contributes the always-accurate part (signatures, typed parameters, return types, effect rows, decorators, struct fields with their sem descriptors, enum variants); your docstring prose contributes Markdown, LaTeX ($…$ / $$…$$), GitHub admonitions, and sema code examples.

Flag	Effect
--out DIR	Write output to DIR (default: <project>/docs/api).
--html	Also render a self-contained HTML page per module (KaTeX + marked, no build step).
--skills	Emit each module’s doc with skill frontmatter, so generated docs load as model context via skills.load.

sema doc myproject                    # write Markdown to <project>/docs/api
sema doc myproject --out build/docs   # to a chosen directory
sema doc myproject --html             # also render standalone HTML
sema doc myproject --skills           # docs loadable as model context

A standard project keeps its modules in src/; if there is no src/, doc documents the directory itself (so it also works on an SDK’s flat sema/ folder).

sema parse / sema tokens

Low-level tools for understanding how Sema reads your source. Both accept one or more files.

sema parse <files...> [--ast]
sema tokens <files...> [--quiet]

sema parse reports parse success (OK (N decls)) or a located parse error; --ast prints the full parse tree instead. sema tokens dumps the lexer’s token stream, or with --quiet just the token count.

sema parse src/main.sema --ast
sema tokens src/main.sema --quiet

sema repl

sema repl [project]

An interactive console: expressions print their value, definitions persist across lines, and a line ending in : reads a block until a blank line. Passing a project directory loads its modules first, so its functions and types are in scope.

Meta-commands (prefixed with :):

Command	Effect
:doc NAME	Reflect a function’s signature + docstring.
:trace	Show the last error’s self-repair packet.
:help	List the meta-commands.
:q (:quit / :exit)	Quit (or press Ctrl-D).

sema repl                # a bare session
sema repl myproject      # with the project's definitions in scope

sema infer

sema infer --gguf <path> --tokenizer <path> --prompt "..." [--max N] [--temp T] [--seed N]

Runs a real local model directly — GGUF generation on GPU (Apple Metal) or CPU via the pure-Rust candle backend. It requires the real-model build; a default build prints how to enable it:

cargo build --release -p sema-cli --features real-model
sema infer --gguf model.gguf --tokenizer tokenizer.json --prompt "Hello" --max 64

--max bounds the generated tokens (default 64), --temp sets sampling temperature (default 0.0, i.e. greedy), and --seed fixes the RNG (default 42).

Package commands

sema add <pypi-name | path | git+url>
sema remove <name>
sema list

sema add installs both PyPI packages (into the project-local .sema/venv, usable immediately via python.import) and native Sema packages (from a local path or git+<url>, installed into .sema/packages/ and resolved by the import loader). sema remove uninstalls; sema list shows what is installed.

sema add numpy
sema add ./greetings
sema add git+https://example.com/some/sema-pkg
sema list
sema remove numpy

Editor integration

sema lsp      # the language server (LSP)
sema dap      # the debug adapter (semad) over stdio

sema lsp runs the language server that editors talk to for diagnostics, hovers, and completion. sema dap runs the debug adapter so any DAP-speaking editor can drive a Sema debug session (breakpoints, stepping, call stack, per-frame locals), sharing the same evaluator as run — inspected equals executed.

The everyday loop

sema check myproject                    # milliseconds; run after every edit
SEMA_STRICT=1 sema run myproject        # prove it does not quietly degrade
sema assure myproject --grade silver    # grade the contracts and properties

See also

• Toolchain — the task-oriented walkthrough.
• Verification — the full model behind assure.
• Effects catalog — the capability rows the checker enforces.