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|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.
Summary
Section titled “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. |
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
Section titled “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 myprojectsema check src/main.sema src/domain.semaWarnings 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
Section titled “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 myprojectTwo environment variables change its behavior:
-
SEMA_STRICT=1turns 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.Terminal window SEMA_STRICT=1 sema run myproject -
SEMA_VM=1runs 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.Terminal window SEMA_VM=1 sema run myproject
sema assure
Section titled “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
ensurepostcondition is fuzzed: inputs are generated from the parameter types and the function is called many times; a violatedensureis reported with a concrete counterexample. - Mutation adequacy (grade
goldonly) — 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 silversema assure myproject --grade goldThe 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
Section titled “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/apisema doc myproject --out build/docs # to a chosen directorysema doc myproject --html # also render standalone HTMLsema doc myproject --skills # docs loadable as model contextA 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
Section titled “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 --astsema tokens src/main.sema --quietsema repl
Section titled “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 sessionsema repl myproject # with the project's definitions in scopesema infer
Section titled “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-modelsema 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
Section titled “Package commands”sema add <pypi-name | path | git+url>sema remove <name>sema listsema 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 numpysema add ./greetingssema add git+https://example.com/some/sema-pkgsema listsema remove numpyEditor integration
Section titled “Editor integration”sema lsp # the language server (LSP)sema dap # the debug adapter (semad) over stdiosema 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
Section titled “The everyday loop”sema check myproject # milliseconds; run after every editSEMA_STRICT=1 sema run myproject # prove it does not quietly degradesema assure myproject --grade silver # grade the contracts and propertiesSee also
Section titled “See also”- Toolchain — the task-oriented walkthrough.
- Verification — the full model behind
assure. - Effects catalog — the capability rows the checker enforces.