spectec/doc/Usage.md

# SpecTec Usage

SpecTec can be run in various modes.
Here we document the most relevant ones.
Use the `--help` option to get a list of additional options.


### Checking Mode

```
spectec [option] file ...
```
This invocation takes a list of SpecTec sources,
concatenates them,
and checks them as a script.

If no error occurs,
i.e., the script is well-formed in the SpecTec [language](Language.md),
this command will simply return silently.

The following general options are available:

* `-v` — print SpecTec version
* `-l` — log processing steps to stdout
* `--help` — print all available options


### AST Mode

```
spectec [option] file ... --ast [-o file]
```
This performs checking and then outputs the abstract syntax true of the [intermediate language](IL.md),
either into the given file, or to stdout.

The following general options are available:

* `--ast-width` - set the line width for pretty-printing the output (default is 80)


### Splicing Mode

```
spectec [option] file ... --splice-sphinx -p file ... [-i | -o file ...]
spectec [option] file ... --splice-latex -p file ... [-i | -o file ...]
```
This performs checking and [*splicing*](Splicing.md).
Splicing processes a list of inputs containing *splice anchors*
and replaces those with output generated by SpecTec.
The output format depends on the splice format chosen:

* `--splice-sphinx` generates output suitable for Sphinx documents,
  including inline math using `:math:` and `math::` mark-up.

* `--splice-latex` generates output suitable for Latex documents
  (currently, prose generation does not work with this).

As before, the first list of files enumerates the SpecTec sources.

The second file list enumerates the input files to be run through splicing,
while the third list names the corresponding output files.

* If the third list is omitted,
  and the `-i` option is given,
  then splicing is applied in place,
  mutating the original input files.

* If the third list is omitted,
  and the `-i` option is *not* given,
  then the output is written to stdout.

* If the third list consists of a single directory path,
  then the output files are written to that directory,
  using their original names.

* Otherwise, the third list must consist of exactly as many file names as the second,
  and names the corresponding output files in order.

If both input and output lists are empty,
then SpecTec will merely check the SpecTec definitions.

See the documentation of [splicing](Splicing.md) for details about the format and function of spice anchors.

The following additional options are available:

* `-d` — dry run: suppress producing output
* `-w` — warn about definitions that have not been spliced or being spliced multiple times
  (individual definitions can be ignored explicitly by using `ignore` splices)
* `--warn-math` — same as `-w`, but only for splices producing formal rules
* `--warn-prose` — same as `-w`, but only for splices producing prose rules
* `--latex-macros` — for math, generate macro invocations for all variables and atoms
  instead of literal math
  (requires the user to define these macros separately)


### Interpreter Mode

```
spectec [option] file ... --interpreter file ...
```
This invokes the meta-interpreter built into SpecTec.

As before, the first list of files enumerates the SpecTec sources.

The other file list enumerates `.wast` files to execute.

**Note:** This mode is highly specific to Wasm
and makes various assumptions about the SpecTec source files and what they define.
It is not expected to work for any other specification,
and may break and require implementation changes when the current Wasm specification is changed in significant ways.

The following additional options are available:

* `-ll` — log interpreter execution steps to stdout
* `--test-version i` — adjust internal assumptions to Wasm version (i = 1, 2, 3, default is 3)
* `--debug` — use debug interpreter

See the documentation for the [Interpreter backend](Interpreter.md) for more details.