Toolchain

The sema command is the whole toolchain: static checking, execution, verification, documentation, inspection, package management, and editor integration. This page is a reference to every command, with an example invocation for each.

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 containing src/). check also accepts individual files.

Summary

Command	What it does
sema check <project>	Static checks: parse, arity, struct fields, effect discipline, unrecognized-directive and policy-example warnings. Run after every edit.
sema run <project>	Execute main(). SEMA_STRICT=1 fails hard on degradations; SEMA_VM=1 runs the bytecode VM.
sema circuit <run|resume|list|show|cancel>	Durable runs: run executes like sema run; the rest manage recorded runs under .sema/runs/.
sema debug <serve|run|replay>	Localhost token-protected run-inspector web UI; replay verifies determinism against a recorded run.
sema assure <project> [--grade bronze|silver|gold]	The verification engine: runs test blocks, fuzzes ensure properties for counterexamples, and (at gold) mutation-tests.
sema doc <project> [--out DIR] [--html] [--skills]	Reflected documentation from signatures + docstrings.
sema repl [project]	Interactive console.
sema parse <files…> [--ast]	Parse and inspect the parse tree.
sema tokens <files…>	Dump the lexer’s token stream.
sema infer …	Run a real local model (requires the real-model build).
sema add / remove / list	Package management (PyPI and native Sema packages).
sema lsp / sema dap	The language server and debug adapter for editors.

Tests and formatting

There is no separate sema test command — authored tests run through sema assure, which executes every test "…": block as part of the verification engine (see below). Source formatting (sema fmt) is planned but not yet a standalone command; use sema parse --ast to inspect structure in the meantime.

sema check — static checks

The fast, run-after-every-edit command. It parses the project and runs the static checks: parse errors, function arity, struct fields, the effect-row discipline, unrecognized-directive warnings (the guard against silent no-ops — a directive in a def body that no runtime handler recognizes is flagged, so a typo or a misplaced clause surfaces here rather than doing nothing at runtime), and policy-example verification (a policy whose declared examples: contradict its rules is an error). It does not execute your program.

sema check myproject
sema check src/main.sema src/domain.sema   # or individual files

A clean run reports no diagnostics.

sema run — execute

Runs the project’s main() on the tree-walking interpreter, the reference semantics.

sema run myproject

Two environment variables change its behavior:

• SEMA_STRICT=1 turns recoverable degradations into hard, typed errors. Off, the runtime self-heals a mis-estimate or a failed step, logs it to the journal and to stderr ([sema:warn] …), and keeps going. 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 to the tree-walker, and every value operation delegates 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 assure — verification

The verification engine. Verification is default-on in Sema — there is no opt-in testable keyword — and assure is where the grades run. It executes 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). The program is systematically mutated and the tests and properties are re-run against each mutant; a mutant that still passes exposes a gap. The killed/total score is gated at ≥50% for a green verdict.

Grades set the depth, selected with --grade (default silver):

• bronze — tests must pass.
• silver — tests plus fuzzed properties; requires explicit effect rows.
• gold — adds the mutation-adequacy threshold.

sema assure myproject --grade silver
sema assure myproject --grade gold

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

sema doc — reflected documentation

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 ($…$), and sema code examples.

sema doc myproject                 # print reflected Markdown
sema doc myproject --out docs/     # write to a directory
sema doc myproject --html          # also render a self-contained HTML page
sema doc myproject --skills        # emit with skill frontmatter (loadable as model context)

--html produces a standalone page (rendered Markdown + KaTeX, no build step). --skills writes each module’s doc with skill frontmatter, so generated docs load as model context via skills.load — code that documents itself to humans and to the models that read it.

sema repl — interactive console

An interactive session for evaluating expressions and inspecting definitions. Passing a project directory loads its modules first.

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

sema parse and sema tokens — inspection

Low-level tools for understanding how Sema reads your source. sema parse --ast prints the parse tree; without --ast it reports parse success or errors. sema tokens dumps the lexer’s token stream.

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

sema infer — real model inference

Runs a real local model directly (GGUF generation on GPU/CPU). It requires the real-model build (cargo build --release --features real-model); a default build prints how to enable it.

sema infer --gguf model.gguf --tokenizer tokenizer.json --prompt "Hello" --max 64

Package commands

sema add installs both PyPI packages (into .sema/venv) and native Sema packages (from a path or git+<url>), sema remove uninstalls, and sema list shows what is installed. See Project Layout for details.

sema add numpy
sema add ./greetings
sema list
sema remove numpy

Editor integration

• sema lsp runs the language server (LSP) that editors talk to for diagnostics, hovers, and completion.
• sema dap runs the debug adapter over stdio, so any DAP-speaking editor can drive a Sema debug session.

sema lsp
sema dap

The verification loop

For everyday work the loop is edit → sema check → SEMA_STRICT=1 sema run → sema assure. check catches static mistakes in milliseconds, strict run proves the program does not quietly degrade, and assure grades the contracts and properties.

Next

• Verification — the full model behind assure: contracts, properties, mutation adequacy, and the guarantee lattice.
• CLI reference — the generated, exhaustive command reference.