# CLI Reference > The complete, verified reference for the sema command — check, run, assure, doc, parse, tokens, repl, infer, packages, and the editor servers — with the exact flags and an example for each. 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](/start/toolchain/); for the verification model behind `assure` see [Verification](/neurosymbolic/verification/). Running `sema` with no arguments prints the command list: ``` usage: sema ``` Most commands take a **project directory** — the folder that contains `src/`. `sema check`, `sema parse`, and `sema tokens` also accept individual files. :::note[No `sema test` or `sema fmt`] There is **no separate `test` subcommand**: authored `test "…":` blocks run through [`sema assure`](#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`](#sema-parse--sema-tokens) to inspect structure in the meantime. ::: ## Summary | Command | Synopsis | What it does | |---|---|---| | `check` | `sema check ` | Static checks: parse, arity, struct fields, effect-row discipline, unrecognized-directive and policy-example warnings. | | `run` | `sema run ` | Execute `main()`. Honors `SEMA_STRICT=1` and `SEMA_VM=1`. | | `assure` | `sema assure [--grade bronze\|silver\|gold]` | Verification engine: `test` blocks, fuzzed `ensure` properties, mutation testing at `gold`. | | `doc` | `sema doc [--out DIR] [--skills] [--html]` | Reflected documentation from signatures + docstrings. | | `parse` | `sema parse [--ast]` | Parse; `--ast` dumps the parse tree. | | `tokens` | `sema tokens [--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 ` | 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 ``` 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. ```bash 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 ``` Executes the project's `main()` on the tree-walking interpreter — the reference semantics — and writes a run journal (its path is printed on completion). ```bash 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. ```bash 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. ```bash SEMA_VM=1 sema run myproject ``` ## `sema assure` ``` sema assure [--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 | ```bash 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 [--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: `/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`. | ```bash sema doc myproject # write Markdown to /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 [--ast] sema tokens [--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. ```bash 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). | ```bash sema repl # a bare session sema repl myproject # with the project's definitions in scope ``` ## `sema infer` ``` sema infer --gguf --tokenizer --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: ```bash 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 sema remove 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+`, installed into `.sema/packages/` and resolved by the import loader). `sema remove` uninstalls; `sema list` shows what is installed. ```bash 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 ```bash 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](/start/toolchain/) — the task-oriented walkthrough. - [Verification](/neurosymbolic/verification/) — the full model behind `assure`. - [Effects catalog](/reference/effects-catalog/) — the capability rows the checker enforces.