Skip to content

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.

CommandSynopsisWhat it does
checksema check <project | files…>Static checks: parse, arity, struct fields, effect-row discipline, unrecognized-directive and policy-example warnings.
runsema run <project>Execute main(). Honors SEMA_STRICT=1 and SEMA_VM=1.
assuresema assure <project> [--grade bronze|silver|gold]Verification engine: test blocks, fuzzed ensure properties, mutation testing at gold.
docsema doc <project> [--out DIR] [--skills] [--html]Reflected documentation from signatures + docstrings.
parsesema parse <files…> [--ast]Parse; --ast dumps the parse tree.
tokenssema tokens <files…> [--quiet]Dump the lexer token stream.
replsema repl [project]Interactive console (:doc, :trace, :q).
infersema infer --gguf … --tokenizer … [--prompt …]Real local GGUF inference (needs the real-model build).
add / remove / listsema add <pkg | path | git+url>Package management (PyPI + native Sema packages).
lsp / dapsema lsp · sema dapLanguage server and debug adapter for editors.
--versionsema --versionPrint the version.
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.

Terminal window
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 <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).

Terminal window
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.

    Terminal window
    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.

    Terminal window
    SEMA_VM=1 sema run myproject
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:

GradeRunsNotes
bronzetestseffect-row inference allowed
silvertests + fuzzed propertiesrequires an explicit effect row on every declared function
gold+ mutation adequacythe strongest gate
Terminal window
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 <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.

FlagEffect
--out DIRWrite output to DIR (default: <project>/docs/api).
--htmlAlso render a self-contained HTML page per module (KaTeX + marked, no build step).
--skillsEmit each module’s doc with skill frontmatter, so generated docs load as model context via skills.load.
Terminal window
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).

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.

Terminal window
sema parse src/main.sema --ast
sema tokens src/main.sema --quiet
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 :):

CommandEffect
:doc NAMEReflect a function’s signature + docstring.
:traceShow the last error’s self-repair packet.
:helpList the meta-commands.
:q (:quit / :exit)Quit (or press Ctrl-D).
Terminal window
sema repl # a bare session
sema repl myproject # with the project's definitions in scope
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:

Terminal window
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).

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.

Terminal window
sema add numpy
sema add ./greetings
sema add git+https://example.com/some/sema-pkg
sema list
sema remove numpy
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.

Terminal window
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